Fix bug#2080: error message on Ltac name clash with primitive tactics

2 files changed, 10 insertions, 1 deletions

diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml
index 8446539f96..9bd3128546 100644
--- a/tactics/tacenv.ml
+++ b/tactics/tacenv.ml
@@ -102,9 +102,17 @@ let _ =
 
 let interp_atomic_ltac id = Id.Map.find id !atomic_mactab
 
+let is_primitive_ltac_ident id =
+  try
+    match Pcoq.parse_string Pcoq.Tactic.tactic id with
+     | Tacexpr.TacArg _ -> false
+     | _ -> true (* most probably TacAtom, i.e. a primitive tactic ident *)
+  with e when Errors.noncritical e -> true (* prim tactics with args, e.g. "apply" *)
+
 let is_atomic_kn kn =
   let (_,_,l) = repr_kn kn in
-  Id.Map.mem (Label.to_id l) !atomic_mactab
+  (Id.Map.mem (Label.to_id l) !atomic_mactab)
+  || (is_primitive_ltac_ident (Label.to_string l))
 
 (***************************************************************************)
 (* Tactic registration *)
diff --git a/test-suite/bugs/closed/2080.v b/test-suite/bugs/closed/2080.v
new file mode 100644
index 0000000000..62c42c8c31
--- /dev/null
+++ b/test-suite/bugs/closed/2080.v
@@ -0,0 +1 @@
+Fail Ltac clear h := inversion h; clear h.