From 6d89e7a4d322a5b341704c490c4460b3353d9888 Mon Sep 17 00:00:00 2001 From: herbelin Date: Mon, 16 Oct 2000 21:19:44 +0000 Subject: 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 --- parsing/astterm.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'parsing/astterm.ml') 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) -- cgit v1.2.3