Library Coq.Compat.Coq84


Compatibility file for making Coq act similar to Coq v8.4 See https://coq.inria.fr/bugs/show_bug.cgi?id=4319 for updates This is required in Coq 8.5 to use the omega tactic; in Coq 8.4, it's automatically available. But ZArith_base puts infix ~ at level 7, and we don't want that, so we don't Import it.
Require Coq.omega.Omega.
Ltac omega := Coq.omega.Omega.omega.

The number of arguments given in match statements has changed from 8.4 to 8.5.

The automatic elimination schemes for records were dropped by default in 8.5. This restores the default behavior of Coq 8.4.

See bug 3545

In 8.4, constructor (tac) allowed backtracking across the use of constructor; it has been subsumed by constructor; tac.
Ltac constructor_84_n n := constructor n.
Ltac constructor_84_tac tac := once (constructor; tac).

Tactic Notation "constructor" := Coq.Init.Notations.constructor.
Tactic Notation "constructor" int_or_var(n) := constructor_84_n n.
Tactic Notation "constructor" "(" tactic(tac) ")" := constructor_84_tac tac.

In 8.4, econstructor (tac) allowed backtracking across the use of econstructor; it has been subsumed by econstructor; tac.
Ltac econstructor_84_n n := econstructor n.
Ltac econstructor_84_tac tac := once (econstructor; tac).

Tactic Notation "econstructor" := Coq.Init.Notations.econstructor.
Tactic Notation "econstructor" int_or_var(n) := econstructor_84_n n.
Tactic Notation "econstructor" "(" tactic(tac) ")" := econstructor_84_tac tac.

Some tactic notations do not factor well with tactics; we add global parsing entries for some tactics that would otherwise be overwritten by custom variants. See https://coq.inria.fr/bugs/show_bug.cgi?id=4392.
Tactic Notation "reflexivity" := reflexivity.
Tactic Notation "assumption" := assumption.
Tactic Notation "etransitivity" := etransitivity.
Tactic Notation "cut" constr(c) := cut c.
Tactic Notation "exact_no_check" constr(c) := exact_no_check c.
Tactic Notation "vm_cast_no_check" constr(c) := vm_cast_no_check c.
Tactic Notation "casetype" constr(c) := casetype c.
Tactic Notation "elimtype" constr(c) := elimtype c.
Tactic Notation "lapply" constr(c) := lapply c.
Tactic Notation "transitivity" constr(c) := transitivity c.
Tactic Notation "left" := left.
Tactic Notation "eleft" := eleft.
Tactic Notation "right" := right.
Tactic Notation "eright" := eright.
Tactic Notation "symmetry" := symmetry.
Tactic Notation "split" := split.
Tactic Notation "esplit" := esplit.

Many things now import PeanoNat rather than NPeano, so we require it so that the old absolute names in NPeano.Nat are available.
Require Coq.Numbers.Natural.Peano.NPeano.

The following coercions were declared by default in Specif.v.
Coercion sig_of_sig2 : sig2 >-> sig.
Coercion sigT_of_sigT2 : sigT2 >-> sigT.
Coercion sigT_of_sig : sig >-> sigT.
Coercion sig_of_sigT : sigT >-> sig.
Coercion sigT2_of_sig2 : sig2 >-> sigT2.
Coercion sig2_of_sigT2 : sigT2 >-> sig2.

As per bug 4733 (https://coq.inria.fr/bugs/show_bug.cgi?id=4733), we want the user to be able to create custom list-like notatoins that work in both 8.4 and 8.5. This is necessary. These should become compat 8.4 notations in the relevant files, but these modify the parser (bug 4798), so this cannot happen until that bug is fixed.
Require Coq.Lists.List.
Require Coq.Vectors.VectorDef.
Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) : list_scope.
Notation " [ x ; .. ; y ] " := (VectorDef.cons _ x _ .. (VectorDef.cons _ y _ (nil _)) ..) : vector_scope.