diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-10-16 21:19:44 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-10-16 21:19:44 +0000 |
| commit | 6d89e7a4d322a5b341704c490c4460b3353d9888 (patch) | |
| tree | e46f518a0f3e3802e4f7e455afc2422f2e430093 /parsing/astterm.ml | |
| 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
Diffstat (limited to 'parsing/astterm.ml')
| -rw-r--r-- | parsing/astterm.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/parsing/astterm.ml b/parsing/astterm.ml index bdd818b6a..5182ed29d 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) |