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.
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.
The following coercions were declared by default in Specif.v.
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.