From 5f8f9e5b8eb22a413090229bc317fc2f36c053ac Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Fri, 30 Oct 2015 13:32:42 -0400
Subject: Update compatibility file for some of bug #4392

Now doing
```coq
Tactic Notation "left" "~" := left.
Tactic Notation "left" "*" := left.
```
will no longer break the `left` tactic in Coq 8.4.

List obtained via
```
grep -o '^  \[[^]]*\]' tactics/coretactics.ml4  | sed s'/^  \[ \(.*\) \]/Tactic Notation \1 := \1./g' | sed s'/\(:=.*\)"/\1/g' | sed s'/\(:=.*\)"/\1/g' | sed s'/\(:=.*\)"/\1/g' | sed s'/\(:=.*\)"/\1/g' | sed s'/\(:=.*\) \(constr\|bindings\|constr_with_bindings\|quantified_hypothesis\|ne_hyp_list\)(\([^)]*\))/\1 \3/g'
```---
 theories/Compat/Coq84.v | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)

diff --git a/theories/Compat/Coq84.v b/theories/Compat/Coq84.v
index 83016976e8..b04d5168f2 100644
--- a/theories/Compat/Coq84.v
+++ b/theories/Compat/Coq84.v
@@ -34,6 +34,27 @@ Tactic Notation "constructor" := constructor_84.
 Tactic Notation "constructor" int_or_var(n) := constructor_84_n 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. *)
+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 "constructor" := constructor.
+Tactic Notation "econstructor" := econstructor.
+Tactic Notation "symmetry" := symmetry.
+Tactic Notation "split" := split.
+Tactic Notation "esplit" := esplit.
+
 Global Set Regular Subst Tactic.
 
 (** Some names have changed in the standard library, so we add aliases. *)
-- 
cgit v1.2.3