diff options
| author | herbelin | 2009-09-11 17:53:30 +0000 |
|---|---|---|
| committer | herbelin | 2009-09-11 17:53:30 +0000 |
| commit | ea85f46dc0cc34db149c24bb2da8f3130e191fc1 (patch) | |
| tree | 3b8fa67f3f1dc5bb2815b38c1040a3ea192c88fe /tactics/auto.ml | |
| parent | 7131609a82198080421b15e2c7a0d8f3b6cbd3de (diff) | |
Generalized the possibility to refer to a global name by a notation
string in most commands expecting a global name (e.g. 'Print "+"' for
an infix notation or 'Print "{ _ } + { _ }"' for a misfix notation,
possibly surrounded by a scope delimiter). Support for such smart
globals in VERNAC EXTEND to do.
Added a file smartlocate.ml for high-level globalization functions.
Mini-nettoyage metasyntax.ml.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12323 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/auto.ml')
| -rw-r--r-- | tactics/auto.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index c62824d4b6..394626f247 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -34,6 +34,7 @@ open Clenv open Hiddentac open Libnames open Nametab +open Smartlocate open Libobject open Library open Printer @@ -533,7 +534,7 @@ type hints_entry = let interp_hints h = let f = Constrintern.interp_constr Evd.empty (Global.env()) in let fr r = - let gr = Syntax_def.global_with_alias r in + let gr = global_with_alias r in let r' = evaluable_of_global_reference (Global.env()) gr in Dumpglob.add_glob (loc_of_reference r) gr; r' in @@ -1118,7 +1119,7 @@ let superauto n to_add argl = tclTRY (tclCOMPLETE (search_superauto n to_add argl)) let interp_to_add gl r = - let r = Syntax_def.locate_global_with_alias (qualid_of_reference r) in + let r = locate_global_with_alias (qualid_of_reference r) in let id = basename_of_global r in (next_ident_away id (pf_ids_of_hyps gl), constr_of_global r) |