diff options
author | 2014-01-10 17:26:12 +0100 | |
---|---|---|
committer | 2014-01-10 17:26:12 +0100 | |
commit | a6ca35c30199f3ccf0ebb7d9b200190e345c4d50 (patch) | |
tree | 3d0cb0bbfda831ea9b820d0ea684db09104038f4 /tactics/tacenv.ml | |
parent | b9ee515a3685a606a0d33f1b06669bf7c4f617e7 (diff) |
Fix bug#2080: error message on Ltac name clash with primitive tactics
Diffstat (limited to 'tactics/tacenv.ml')
-rw-r--r-- | tactics/tacenv.ml | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml index 8446539f9..9bd312854 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 *) |