diff options
| author | herbelin | 2000-10-16 21:19:44 +0000 |
|---|---|---|
| committer | herbelin | 2000-10-16 21:19:44 +0000 |
| commit | 6d89e7a4d322a5b341704c490c4460b3353d9888 (patch) | |
| tree | e46f518a0f3e3802e4f7e455afc2422f2e430093 | |
| parent | a4da3fbec91ee28596c34414b6c58eb1e19b4f78 (diff) | |
Changement "command" en "constr" et globalize_command en globalize_constr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@711 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | parsing/astterm.ml | 8 | ||||
| -rw-r--r-- | parsing/astterm.mli | 2 |
2 files changed, 5 insertions, 5 deletions
diff --git a/parsing/astterm.ml b/parsing/astterm.ml index bdd818b6a9..5182ed29df 100644 --- a/parsing/astterm.ml +++ b/parsing/astterm.ml @@ -486,7 +486,7 @@ let ast_adjust_consts sigma = (* locations are kept *) in dbrec -let globalize_command ast = +let globalize_constr ast = let sign = Global.var_context () in ast_adjust_consts Evd.empty (from_list (ids_of_var_context sign)) ast @@ -509,10 +509,10 @@ let globalize_ast ast = glob_ast Evd.empty (from_list (ids_of_var_context sign)) ast -(* Installation of the AST quotations. "command" is used by default. *) +(* Installation of the AST quotations. "constr" is used by default. *) let _ = - Pcoq.define_quotation true "command" - (Pcoq.map_entry globalize_command Pcoq.Constr.constr) + Pcoq.define_quotation true "constr" + (Pcoq.map_entry globalize_constr Pcoq.Constr.constr) let _ = Pcoq.define_quotation false "tactic" (Pcoq.map_entry globalize_ast Pcoq.Tactic.tactic) diff --git a/parsing/astterm.mli b/parsing/astterm.mli index fdb930c999..0521b05951 100644 --- a/parsing/astterm.mli +++ b/parsing/astterm.mli @@ -78,7 +78,7 @@ val raw_constr_of_compattern : 'c evar_map -> 'a assumptions -> Coqast.t -> rawconstr *) -val globalize_command : Coqast.t -> Coqast.t +val globalize_constr : Coqast.t -> Coqast.t (* val globalize_ast : Coqast.t -> Coqast.t |