diff options
| author |  Jason Gross <jasongross9@gmail.com> | 2015-12-29 13:21:17 -0500 |
|---|---|---|
| committer |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-04-04 17:08:04 +0200 |
| commit | 4c078b0362542908eb2fe1d63f0d867b339953fd (patch) | |
| tree | 7081179cef1270f35cc5ce8008336761a2a74050 /theories/Compat | |
| parent | 59cb5ca9b6c0e29fe65e9ae99dfd6cabafc52be6 (diff) | |
Update Coq84.v
We no longer need to redefine `refine` (it now shelves by default). Also clean up `constructor` a bit.
Diffstat (limited to 'theories/Compat')
| -rw-r--r-- | theories/Compat/Coq84.v | 9 |
1 files changed, 2 insertions, 7 deletions
diff --git a/theories/Compat/Coq84.v b/theories/Compat/Coq84.v index d695ef1d8..5036b9bc8 100644 --- a/theories/Compat/Coq84.v +++ b/theories/Compat/Coq84.v @@ -21,16 +21,11 @@ Global Set Nonrecursive Elimination Schemes. (** See bug 3545 *) Global Set Universal Lemma Under Conjunction. -(** In 8.5, [refine] leaves over dependent subgoals. *) -Tactic Notation "refine" uconstr(term) := refine term; shelve_unifiable. - (** In 8.4, [constructor (tac)] allowed backtracking across the use of [constructor]; it has been subsumed by [constructor; tac]. *) -Ltac constructor_84 := constructor. -Ltac constructor_84_n n := constructor n. Ltac constructor_84_tac tac := once (constructor; tac). -Tactic Notation "constructor" := constructor_84. -Tactic Notation "constructor" int_or_var(n) := constructor_84_n n. +Tactic Notation "constructor" := Coq.Init.Notations.constructor. +Tactic Notation "constructor" int_or_var(n) := Coq.Init.Notations.constructor n. Tactic Notation "constructor" "(" tactic(tac) ")" := constructor_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. *) |