Renommage command en constr

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@267 85f007b7-540e-0410-9357-904b9bb8a0f7

14 files changed, 122 insertions, 114 deletions

diff --git a/.depend.camlp4 b/.depend.camlp4
index 68d5393d34..3ac01960b4 100644
--- a/.depend.camlp4
+++ b/.depend.camlp4
@@ -2,16 +2,22 @@ parsing/extend.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/lexer.cmi \
     parsing/pcoq.cmi lib/pp.cmi lib/util.cmi parsing/extend.cmi 
 parsing/extend.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/lexer.cmx \
     parsing/pcoq.cmx lib/pp.cmx lib/util.cmx parsing/extend.cmi 
-parsing/g_basevernac.cmo: parsing/ast.cmi toplevel/command.cmi \
-    parsing/coqast.cmi parsing/pcoq.cmi toplevel/vernac.cmi 
-parsing/g_basevernac.cmx: parsing/ast.cmx toplevel/command.cmx \
-    parsing/coqast.cmx parsing/pcoq.cmx toplevel/vernac.cmx 
-parsing/g_cases.cmo: toplevel/command.cmi parsing/coqast.cmi parsing/pcoq.cmi 
-parsing/g_cases.cmx: toplevel/command.cmx parsing/coqast.cmx parsing/pcoq.cmx 
+parsing/g_basevernac.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi \
+    toplevel/vernac.cmi 
+parsing/g_basevernac.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/pcoq.cmx \
+    toplevel/vernac.cmx 
+parsing/g_cases.cmo: parsing/coqast.cmi parsing/pcoq.cmi 
+parsing/g_cases.cmx: parsing/coqast.cmx parsing/pcoq.cmx 
 parsing/g_command.cmo: parsing/ast.cmi toplevel/command.cmi \
     parsing/coqast.cmi parsing/pcoq.cmi 
 parsing/g_command.cmx: parsing/ast.cmx toplevel/command.cmx \
     parsing/coqast.cmx parsing/pcoq.cmx 
+parsing/g_constr.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi 
+parsing/g_constr.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/pcoq.cmx 
+parsing/g_corevernac.cmo: parsing/coqast.cmi parsing/pcoq.cmi \
+    toplevel/vernac.cmi 
+parsing/g_corevernac.cmx: parsing/coqast.cmx parsing/pcoq.cmx \
+    toplevel/vernac.cmx 
 parsing/g_minicoq.cmo: kernel/generic.cmi parsing/lexer.cmi kernel/names.cmi \
     lib/pp.cmi kernel/sign.cmi kernel/term.cmi kernel/univ.cmi lib/util.cmi \
     parsing/g_minicoq.cmi 
@@ -20,20 +26,20 @@ parsing/g_minicoq.cmx: kernel/generic.cmx parsing/lexer.cmx kernel/names.cmx \
     parsing/g_minicoq.cmi 
 parsing/g_prim.cmo: parsing/coqast.cmi parsing/pcoq.cmi 
 parsing/g_prim.cmx: parsing/coqast.cmx parsing/pcoq.cmx 
-parsing/g_tactic.cmo: parsing/ast.cmi toplevel/command.cmi parsing/coqast.cmi \
-    parsing/pcoq.cmi lib/pp.cmi lib/util.cmi 
-parsing/g_tactic.cmx: parsing/ast.cmx toplevel/command.cmx parsing/coqast.cmx \
-    parsing/pcoq.cmx lib/pp.cmx lib/util.cmx 
-parsing/g_vernac.cmo: toplevel/command.cmi parsing/coqast.cmi \
-    parsing/pcoq.cmi toplevel/vernac.cmi 
-parsing/g_vernac.cmx: toplevel/command.cmx parsing/coqast.cmx \
-    parsing/pcoq.cmx toplevel/vernac.cmx 
+parsing/g_tactic.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi \
+    lib/pp.cmi lib/util.cmi 
+parsing/g_tactic.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/pcoq.cmx \
+    lib/pp.cmx lib/util.cmx 
+parsing/g_vernac.cmo: parsing/coqast.cmi parsing/pcoq.cmi toplevel/vernac.cmi 
+parsing/g_vernac.cmx: parsing/coqast.cmx parsing/pcoq.cmx toplevel/vernac.cmx 
 parsing/pcoq.cmo: parsing/coqast.cmi parsing/lexer.cmi lib/pp.cmi \
     lib/util.cmi parsing/pcoq.cmi 
 parsing/pcoq.cmx: parsing/coqast.cmx parsing/lexer.cmx lib/pp.cmx \
     lib/util.cmx parsing/pcoq.cmi 
 parsing/q_coqast.cmo: parsing/coqast.cmi parsing/pcoq.cmi 
 parsing/q_coqast.cmx: parsing/coqast.cmx parsing/pcoq.cmi 
+scripts/coqc.cmo: config/coq_config.cmi toplevel/usage.cmi 
+scripts/coqc.cmx: config/coq_config.cmx toplevel/usage.cmx 
 toplevel/mltop.cmo: library/lib.cmi library/libobject.cmi library/library.cmi \
     lib/pp.cmi library/summary.cmi lib/system.cmi lib/util.cmi \
     toplevel/vernacinterp.cmi toplevel/mltop.cmi 
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index 2c8cb53dc3..3064492d33 100644
--- a/parsing/g_basevernac.ml4
+++ b/parsing/g_basevernac.ml4
@@ -34,10 +34,10 @@ GEXTEND Gram
     [ [ s = Prim.string -> s ] ]
   ;
   comarg:
-    [ [ c = Command.command -> <:ast< (COMMAND $c) >> ] ]
+    [ [ c = Constr.constr -> <:ast< (CONSTR $c) >> ] ]
   ;
   lcomarg:
-    [ [ c = Command.lcommand -> <:ast< (COMMAND $c) >> ] ]
+    [ [ c = Constr.lconstr -> <:ast< (CONSTR $c) >> ] ]
   ;
   lvernac:
     [ [ v = vernac; l = lvernac -> v::l
@@ -54,9 +54,11 @@ GEXTEND Gram
     [ [ IDENT "Pwd"; "." -> <:ast< (PWD) >>
       | IDENT "Cd"; "." -> <:ast< (CD) >>
       | IDENT "Cd"; dir = stringarg; "." -> <:ast< (CD $dir) >>
-      | "Quit"; "." -> <:ast< (QUIT) >>
+
       | IDENT "Drop"; "." -> <:ast< (DROP) >>
-      | IDENT "ProtectedLoop"; "." -> <:ast< (PROTECTEDLOOP) >>
+      | IDENT "ProtectedLoop"; "." -> <:ast< (PROTECTEDLOOP)>>
+      | "Quit"; "." -> <:ast< (QUIT) >>
+
       | IDENT "Print"; IDENT "All"; "." -> <:ast< (PrintAll) >>
       | IDENT "Print"; "." -> <:ast< (PRINT) >>
       | IDENT "Print"; IDENT "Hint"; "*"; "." 
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index 8bdecdf8fc..ffb88d104c 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -227,10 +227,10 @@ let ctxt_access sigma sp =
 
 
 let pf_lookup_name_as_renamed hyps ccl s =
-  Termast.lookup_name_as_renamed (gLOB hyps) ccl s
+  Detyping.lookup_name_as_renamed (gLOB hyps) ccl s
 
 let pf_lookup_index_as_renamed ccl n =
-  Termast.lookup_index_as_renamed ccl n
+  Detyping.lookup_index_as_renamed ccl n
 
 (*********************************************************************)
 (*                  Pretty printing functions                        *)
@@ -239,31 +239,31 @@ let pf_lookup_index_as_renamed ccl n =
 open Pp
 open Printer
 
-(* Il faudrait parametrer toutes les pr_term, term0, etc. par la
+(* Il faudrait parametrer toutes les pr_term, term_env, etc. par la
   strategie de renommage choisie pour Termast (en particulier, il
   faudrait pouvoir etre sur que lookup_as_renamed qui est utilisé par
   Intros Until fonctionne exactement comme on affiche le but avec
-  term0 *)
+  term_env *)
 
 let pf_lookup_name_as_renamed hyps ccl s =
-  Termast.lookup_name_as_renamed (gLOB hyps) ccl s
+  Detyping.lookup_name_as_renamed (gLOB hyps) ccl s
 
 let pf_lookup_index_as_renamed ccl n =
-  Termast.lookup_index_as_renamed ccl n
+  Detyping.lookup_index_as_renamed ccl n
 
 let pr_idl idl = prlist_with_sep pr_spc print_id idl
 
 let pr_goal g =
   let sign = context g.evar_env in
   let penv = pr_env_opt sign in
-  let pc = term0_at_top sign g.evar_concl in
+  let pc = prterm_env_at_top sign g.evar_concl in
   [< 'sTR"  "; hV 0 [< penv; 'fNL;
 		       'sTR (emacs_str (String.make 1 (Char.chr 253))) ;
                        'sTR "============================"; 'fNL ;
                        'sTR" " ; pc>]; 'fNL>]
 
 let pr_concl n g =
-  let pc = term0_at_top (context g.evar_env) g.evar_concl in
+  let pc = prterm_env_at_top (context g.evar_env) g.evar_concl in
   [< 'sTR (emacs_str (String.make 1 (Char.chr 253))) ;
      'sTR "subgoal ";'iNT n;'sTR " is:";'cUT;'sTR" " ; pc >]
 
@@ -321,7 +321,7 @@ let pr_seq evd =
       (fun (id,ty) -> hOV 0 [< print_id id; 'sTR" : ";prterm ty.body >])
       sign 
   in
-  let pcl = term0_at_top (gLOB hyps) cl in
+  let pcl = prterm_env_at_top (gLOB hyps) cl in
   hOV 0 [< pc; pdcl ; 'sPC ; hOV 0 [< 'sTR"|- " ; pcl >] >]
 
 let prgl gl =
diff --git a/syntax/MakeBare.v b/syntax/MakeBare.v
index 8740d5a04d..bb12e70585 100644
--- a/syntax/MakeBare.v
+++ b/syntax/MakeBare.v
@@ -1,3 +1,3 @@
-Load PPCommand.
-Load PPTactic.
+Load PPConstr.
 Load PPCases.
+Load PPTactic.
diff --git a/syntax/PPTactic.v b/syntax/PPTactic.v
index 62c3319a0c..e9a5f11b54 100644
--- a/syntax/PPTactic.v
+++ b/syntax/PPTactic.v
@@ -312,4 +312,4 @@ Syntax tactic
   ;
 
   level 8:
-  command [(COMMAND $c)] -> [ (PPUNI$COMMAND $c):E ].
+  tactic_to_constr [(COMMAND $c)] -> [ $c:"constr":9 ].
diff --git a/tactics/auto.ml b/tactics/auto.ml
index e1c4caad77..02d76010cc 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -330,7 +330,7 @@ let _ =
   vinterp_add
     "HintResolve"
     (function 
-       | [VARG_IDENTIFIER hintname; VARG_VARGLIST l; VARG_COMMAND c] ->
+       | [VARG_IDENTIFIER hintname; VARG_VARGLIST l; VARG_CONSTR c] ->
 	   let c1 = Astterm.constr_of_com Evd.empty (Global.env()) c in
 	   let dbnames = if l = [] then ["core"] else 
 	     List.map (function VARG_IDENTIFIER i -> string_of_id i
@@ -342,7 +342,7 @@ let _ =
   vinterp_add
     "HintImmediate"
     (function 
-       | [VARG_IDENTIFIER hintname; VARG_VARGLIST l; VARG_COMMAND c] ->
+       | [VARG_IDENTIFIER hintname; VARG_VARGLIST l; VARG_CONSTR c] ->
 	   let c1 = Astterm.constr_of_com Evd.empty (Global.env()) c in
 	   let dbnames = if l = [] then ["core"] else 
 	     List.map (function VARG_IDENTIFIER i -> string_of_id i
@@ -377,7 +377,7 @@ let _ =
     "HintExtern"
     (function 
        | [VARG_IDENTIFIER hintname; VARG_VARGLIST l;
-	  VARG_NUMBER pri; VARG_COMMAND patcom; VARG_TACTIC tacexp] ->
+	  VARG_NUMBER pri; VARG_CONSTR patcom; VARG_TACTIC tacexp] ->
            let pat = Pattern.raw_sopattern_of_compattern 
 		       (Global.env()) patcom in
 	   let dbnames = if l = [] then ["core"] else 
diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml
index 6efa9c686f..1b47b7c1e4 100644
--- a/tactics/dhyp.ml
+++ b/tactics/dhyp.ml
@@ -206,7 +206,7 @@ let add_destructor_hint na pat pri code =
 let _ = 
   vinterp_add "HintDestruct"
     (function
-       | [VARG_IDENTIFIER na; VARG_AST location; VARG_COMMAND patcom;
+       | [VARG_IDENTIFIER na; VARG_AST location; VARG_CONSTR patcom;
           VARG_NUMBER pri; VARG_AST tacexp] ->
 	   let loc = match location with
              | Node(_,"CONCL",[]) -> Concl()
diff --git a/tactics/pattern.ml b/tactics/pattern.ml
index fc5b6a4466..3038933e9a 100644
--- a/tactics/pattern.ml
+++ b/tactics/pattern.ml
@@ -35,7 +35,7 @@ let raw_sopattern_of_compattern env com =
 let parse_pattern s =
   let com =
     try 
-      Pcoq.parse_string Pcoq.Command.command_eoi s 
+      Pcoq.parse_string Pcoq.Constr.constr_eoi s 
     with Stdpp.Exc_located (_ , (Stream.Failure | Stream.Error _)) ->
       error "Malformed pattern" 
   in
diff --git a/theories/Init/DatatypesSyntax.v b/theories/Init/DatatypesSyntax.v
index 2841c2150a..520c988d24 100644
--- a/theories/Init/DatatypesSyntax.v
+++ b/theories/Init/DatatypesSyntax.v
@@ -5,20 +5,20 @@ Require Export Datatypes.
 
 (* Parsing of things in Datatypes.v *)
 
-Grammar command command1 :=
-  pair_expl [ "<" lcommand($l1) "," lcommand($c2) ">" "(" lcommand($c3) ","
-    lcommand($c4) ")" ] -> [<<(pair $l1 $c2 $c3 $c4)>>]
-| fst_expl [ "<" lcommand($l1) "," lcommand($c2) ">" "Fst" "("
-    lcommand($l) ")" ] -> [<<(fst $l1 $c2 $l)>>]
-| snd_expl [ "<" lcommand($l1) "," lcommand($c2) ">" "Snd" "("
-    lcommand($l) ")" ] -> [<<(snd $l1 $c2 $l)>>]
-
-with command0 :=
-  pair [ "(" lcommand($lc1) "," lcommand($lc2) ")" ] ->
+Grammar constr constr1 :=
+  pair_expl [ "<" lconstr($l1) "," lconstr($c2) ">" "(" lconstr($c3) ","
+    lconstr($c4) ")" ] -> [<<(pair $l1 $c2 $c3 $c4)>>]
+| fst_expl [ "<" lconstr($l1) "," lconstr($c2) ">" "Fst" "("
+    lconstr($l) ")" ] -> [<<(fst $l1 $c2 $l)>>]
+| snd_expl [ "<" lconstr($l1) "," lconstr($c2) ">" "Snd" "("
+    lconstr($l) ")" ] -> [<<(snd $l1 $c2 $l)>>]
+
+with constr0 :=
+  pair [ "(" lconstr($lc1) "," lconstr($lc2) ")" ] ->
          [<<(pair ? ? $lc1 $lc2)>>]
 
-with command3 :=
-  prod [ command2($c1) "*" command3($c2) ] -> [<<(prod $c1 $c2)>>].
+with constr3 :=
+  prod [ constr2($c1) "*" constr3($c2) ] -> [<<(prod $c1 $c2)>>].
 
 (* Pretty-printing of things in Datatypes.v *)
 
diff --git a/theories/Init/LogicSyntax.v b/theories/Init/LogicSyntax.v
index fdcc7624cc..b0e8bd5ba4 100644
--- a/theories/Init/LogicSyntax.v
+++ b/theories/Init/LogicSyntax.v
@@ -5,46 +5,46 @@ Require Export Logic.
 
 (* Parsing of things in Logic.v *)
 
-Grammar command command1 :=
-  conj [ "<" lcommand($l1) "," lcommand($c2) ">" "{" command($c3) ","
-        command($c4) "}" ] -> [<<(conj $l1 $c2 $c3 $c4)>>]
-| proj1 [ "<" lcommand($l1) "," lcommand($c2) ">" "Fst" "{"
-        lcommand($l) "}" ] -> [<<(proj1 $l1 $c2 $l)>>]
-| proj2 [ "<" lcommand($l1) "," lcommand($c2) ">" "Snd" "{"
-        lcommand($l) "}" ] -> [<<(proj2 $l1 $c2 $l)>>]
-| IF [ "either" command($c) "and_then" command($t) "or_else" command($e) ] ->
+Grammar constr constr1 :=
+  conj [ "<" lconstr($l1) "," lconstr($c2) ">" "{" constr($c3) ","
+        constr($c4) "}" ] -> [<<(conj $l1 $c2 $c3 $c4)>>]
+| proj1 [ "<" lconstr($l1) "," lconstr($c2) ">" "Fst" "{"
+        lconstr($l) "}" ] -> [<<(proj1 $l1 $c2 $l)>>]
+| proj2 [ "<" lconstr($l1) "," lconstr($c2) ">" "Snd" "{"
+        lconstr($l) "}" ] -> [<<(proj2 $l1 $c2 $l)>>]
+| IF [ "either" constr($c) "and_then" constr($t) "or_else" constr($e) ] ->
        [<<(IF $c $t $e)>>]
-| all [ "<" lcommand($l1) ">" "All" "(" lcommand($l2) ")" ] ->
+| all [ "<" lconstr($l1) ">" "All" "(" lconstr($l2) ")" ] ->
        [<<(all $l1 $l2)>>]
-| eq_expl [ "<" lcommand($l1) ">" command0($c1) "=" command0($c2) ] ->
+| eq_expl [ "<" lconstr($l1) ">" constr0($c1) "=" constr0($c2) ] ->
             [<<(eq $l1 $c1 $c2)>>]
-| eq_impl [ command0($c) "=" command0($c2) ] -> [<<(eq ? $c $c2)>>]
+| eq_impl [ constr0($c) "=" constr0($c2) ] -> [<<(eq ? $c $c2)>>]
 
-with command2 :=
-  not [ "~" command2($c) ] -> [<<(not $c)>>]
+with constr2 :=
+  not [ "~" constr2($c) ] -> [<<(not $c)>>]
 
-with command6 :=
-  and [ command5($c1) "/\\" command6($c2) ] -> [<<(and $c1 $c2)>>]
+with constr6 :=
+  and [ constr5($c1) "/\\" constr6($c2) ] -> [<<(and $c1 $c2)>>]
 
-with command7 :=
-  or [ command6($c1) "\\/" command7($c2) ] -> [<<(or $c1 $c2)>>]
+with constr7 :=
+  or [ constr6($c1) "\\/" constr7($c2) ] -> [<<(or $c1 $c2)>>]
 
-with command8 :=
-  iff [ command7($c1) "<->" command8($c2) ] -> [<<(iff $c1 $c2)>>]
+with constr8 :=
+  iff [ constr7($c1) "<->" constr8($c2) ] -> [<<(iff $c1 $c2)>>]
 
-with command10 :=
-  allexplicit [ "ALL" ident($x) ":" command($t) "|" command($p) ]
+with constr10 :=
+  allexplicit [ "ALL" ident($x) ":" constr($t) "|" constr($p) ]
                           -> [<<(all $t [$x : $t]$p)>>]
-| allimplicit [ "ALL" ident($x) "|" command($p) ]
+| allimplicit [ "ALL" ident($x) "|" constr($p) ]
                           -> [<<(all ? [$x]$p)>>]
-| exexplicit [ "EX" ident($v) ":" command($t) "|" command($c1) ]
+| exexplicit [ "EX" ident($v) ":" constr($t) "|" constr($c1) ]
                           -> [<<(ex $t [$v : $t]$c1)>>]
-| eximplicit [ "EX" ident($v) "|" command($c1) ] 
+| eximplicit [ "EX" ident($v) "|" constr($c1) ] 
                           -> [<<(ex ? [$v]$c1)>>]
-| ex2explicit [ "EX" ident($v) ":" command($t) "|" command($c1) "&"
-           command($c2) ] -> [<<(ex2 $t [$v : $t]$c1 [$v : t]$c2)>>]
-| ex2implicit [ "EX" ident($v) "|" command($c1) "&" 
-           command($c2) ] -> [<<(ex2 ? [$v]$c1 [$v]$c2)>>].
+| ex2explicit [ "EX" ident($v) ":" constr($t) "|" constr($c1) "&"
+           constr($c2) ] -> [<<(ex2 $t [$v : $t]$c1 [$v : t]$c2)>>]
+| ex2implicit [ "EX" ident($v) "|" constr($c1) "&" 
+           constr($c2) ] -> [<<(ex2 ? [$v]$c1 [$v]$c2)>>].
 
 
 (* Pretty-printing of things in Logic.v *)
diff --git a/theories/Init/SpecifSyntax.v b/theories/Init/SpecifSyntax.v
index 0c8700ceb1..c399a74eb3 100644
--- a/theories/Init/SpecifSyntax.v
+++ b/theories/Init/SpecifSyntax.v
@@ -6,26 +6,26 @@ Require Export Specif.
 
 (* Parsing of things in Specif.v *)
 
-Grammar command command1 :=
-  sig [ "{" lcommand($lc) ":" lcommand($c1) "|" lcommand($c2) "}" ]
+Grammar constr constr1 :=
+  sig [ "{" lconstr($lc) ":" lconstr($c1) "|" lconstr($c2) "}" ]
        -> [<<(sig $c1 [$lc : $c1]$c2)>>]
 
-| sig2 [ "{" lcommand($lc) ":" lcommand($c1)
-           "|" lcommand($c2) "&" lcommand($c3) "}" ]
+| sig2 [ "{" lconstr($lc) ":" lconstr($c1)
+           "|" lconstr($c2) "&" lconstr($c3) "}" ]
        -> [<<(sig2 $c1 [$lc : $c1]$c2 [$lc : $c1]$c3)>>]
 
-| sigS [ "{" lcommand($lc) ":" lcommand($c1) "&" lcommand($c2) "}" ]
+| sigS [ "{" lconstr($lc) ":" lconstr($c1) "&" lconstr($c2) "}" ]
        -> [<<(sigS $c1 [$lc : $c1]$c2)>>]
 
-| sigS2 [ "{" lcommand($lc) ":" lcommand($c1)
-             "&" lcommand($c2) "&" lcommand($c3) "}" ]
+| sigS2 [ "{" lconstr($lc) ":" lconstr($c1)
+             "&" lconstr($c2) "&" lconstr($c3) "}" ]
        -> [<<(sigS2 $c1 [$lc : $c1]$c2 [$lc : $c1]$c3)>>]
 
-| squash [ "{" lcommand($lc) "}" ] -> [(SQUASH $lc)].
+| squash [ "{" lconstr($lc) "}" ] -> [(SQUASH $lc)].
 
-Grammar command lassoc_command4 :=
+Grammar constr lassoc_constr4 :=
   squash_sum
-  [ lassoc_command4($c1) "+" lassoc_command4($c2) ] ->
+  [ lassoc_constr4($c1) "+" lassoc_constr4($c2) ] ->
       case [$c2] of
         (SQUASH $T2) ->
             case [$c1] of
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 765f3e9f6e..4dad9e2bc1 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -339,7 +339,7 @@ let _ =
 let _ =
   add "GOAL"
     (function 
-       | [VARG_COMMAND com] ->
+       | [VARG_CONSTR com] ->
 	   (fun () ->
               if not (refining()) then begin
               	start_proof "Unnamed_thm" NeverDischarge com;
@@ -659,7 +659,7 @@ let _ =
 let _ =
   add "StartProof"
     (function 
-       | [VARG_STRING kind;VARG_IDENTIFIER s;VARG_COMMAND c] ->
+       | [VARG_STRING kind;VARG_IDENTIFIER s;VARG_CONSTR c] ->
 	   let stre = match kind with
 	     | "THEOREM" -> NeverDischarge
              | "LEMMA" -> NeverDischarge
@@ -681,7 +681,7 @@ let _ =
   add "TheoremProof"
     (function 
        | [VARG_STRING kind; VARG_IDENTIFIER s; 
-	  VARG_COMMAND c; VARG_VARGLIST coml] ->
+	  VARG_CONSTR c; VARG_VARGLIST coml] ->
 	   let calls = List.map
 			 (function 
 			    | (VCALL(na,l)) -> (na,l)
@@ -724,7 +724,7 @@ let _ =
 let _ =
   add "DEFINITION"
     (function 
-       | (VARG_STRING kind :: VARG_IDENTIFIER id :: VARG_COMMAND c ::optred) ->
+       | (VARG_STRING kind :: VARG_IDENTIFIER id :: VARG_CONSTR c ::optred) ->
 	   let red_option = match optred with 
 	     | [] -> None
 	     | [VARG_TACTIC_ARG (Redexp(r1,r2))] -> 
@@ -806,7 +806,7 @@ let _ =
 let _ =
   add "Eval"
     (function
-       | VARG_TACTIC_ARG (Redexp (rn,unf)) :: VARG_COMMAND c :: g ->
+       | VARG_TACTIC_ARG (Redexp (rn,unf)) :: VARG_CONSTR c :: g ->
            let (evmap,sign) = get_evmap_sign (goal_of_args g) in
            let redexp = redexp_of_ast evmap sign (rn,unf) in 
            let redfun = print_eval (reduction_of_redexp redexp) sign in 
@@ -816,7 +816,7 @@ let _ =
 let _ =
   add "Check"
     (function 
-       | VARG_STRING kind :: VARG_COMMAND c :: g ->
+       | VARG_STRING kind :: VARG_CONSTR c :: g ->
 	   let (evmap, sign) = get_evmap_sign (goal_of_args g) in
 	   let prfun = match kind with
 	     | "CHECK" -> print_val
@@ -881,7 +881,7 @@ let _ =
     (function 
        | [ VARG_STRING f;
            VARG_IDENTIFIER s;
-           VARG_COMMAND c;
+           VARG_CONSTR c;
            VARG_BINDERLIST binders;
            VARG_BINDERLIST constructors ] ->
            let la = join_binders binders in
@@ -921,7 +921,7 @@ let _ =
           	(function 
 		   | (VARG_VARGLIST 
 			[VARG_IDENTIFIER arid;
-			 VARG_COMMAND arc;
+			 VARG_CONSTR arc;
 			 VARG_BINDERLIST binders; 
 			 VARG_BINDERLIST lconstr])
 		     ->
@@ -948,7 +948,7 @@ let _ =
            	(function 
 		   | (VARG_VARGLIST 
 			[VARG_IDENTIFIER arid;
-			 VARG_COMMAND arc;
+			 VARG_CONSTR arc;
 			 VARG_BINDERLIST lconstr])
 		     -> (arid,
 			 arc,
@@ -969,7 +969,7 @@ let _ =
        | [VARG_STRING coe;
           VARG_IDENTIFIER struc; 
           VARG_BINDERLIST binders; 
-          VARG_COMMAND s; 
+          VARG_CONSTR s; 
           VARG_VARGLIST namec; 
           VARG_VARGLIST cfs] -> 
            let ps = join_binders binders in
@@ -977,7 +977,7 @@ let _ =
                        (function 
 			  | (VARG_VARGLIST 
                                [VARG_STRING str;VARG_IDENTIFIER id;
-                                VARG_COMMAND c]) ->
+                                VARG_CONSTR c]) ->
 			      (str = "COERCION",(id,c))
 			  | _ -> bad_vernac_args "RECORD")
                        cfs 
@@ -1001,8 +1001,8 @@ let _ =
 		   | (VARG_VARGLIST 
 			[VARG_IDENTIFIER fid;
 			 VARG_BINDERLIST farg; 
-			 VARG_COMMAND arf;
-			 VARG_COMMAND ardef])
+			 VARG_CONSTR arf;
+			 VARG_CONSTR ardef])
 		     -> (fid,join_binders farg,arf,ardef)
 		   | _ -> bad_vernac_args "MUTUALRECURSIVE") lmi
 	    in 
@@ -1018,8 +1018,8 @@ let _ =
                (function 
 		  | (VARG_VARGLIST 
 		       [VARG_IDENTIFIER fid; 
-			VARG_COMMAND arf;
-			VARG_COMMAND ardef])
+			VARG_CONSTR arf;
+			VARG_CONSTR ardef])
 		    -> (fid,arf,ardef)
 		  | _ -> bad_vernac_args "MUTUALCORECURSIVE") lmi
 	   in 
@@ -1037,7 +1037,7 @@ let _ =
 		       [VARG_IDENTIFIER fid;
 			VARG_STRING depstr;
 			VARG_IDENTIFIER indid;
-			VARG_COMMAND sort]) ->
+			VARG_CONSTR sort]) ->
 		      let dep = match depstr with 
 			| "DEP" -> true
                         | "NODEP" -> false
@@ -1052,9 +1052,9 @@ let _ =
 let _ =
   add "SyntaxMacro"
     (function 
-       | [VARG_IDENTIFIER id;VARG_COMMAND com] ->
+       | [VARG_IDENTIFIER id;VARG_CONSTR com] ->
 	   (fun () -> syntax_definition id com)
-       | [VARG_IDENTIFIER id;VARG_COMMAND com; VARG_NUMBER n] ->
+       | [VARG_IDENTIFIER id;VARG_CONSTR com; VARG_NUMBER n] ->
            (fun () ->
               let rec aux t = function
                 | 0 -> t
@@ -1067,7 +1067,7 @@ let _ =
 let _ =
   add "ABSTRACTION"
     (function 
-       | (VARG_IDENTIFIER id) :: (VARG_COMMAND com) :: l ->
+       | (VARG_IDENTIFIER id) :: (VARG_CONSTR com) :: l ->
 	   (fun () ->
               let arity = 
 		Array.of_list
@@ -1246,7 +1246,7 @@ let _ =
 let _ =
   add "Searchisos"
   (function
-     | [VARG_COMMAND com] -> 
+     | [VARG_CONSTR com] -> 
 	 (fun () ->
 	    let env = Global.env() in
 	    let c = constr_of_com Evd.empty env com in
@@ -1409,7 +1409,7 @@ open Pfedit
 let _ = 
   vinterp_add "EXISTENTIAL"
     (function 
-       | [VARG_NUMBER n; VARG_COMMAND c] -> 
+       | [VARG_NUMBER n; VARG_CONSTR c] -> 
            (fun () -> mutate (instantiate_pf_com n c))
        |  _  -> assert false)
 
@@ -1419,7 +1419,7 @@ let _ =
 let _ = 
   vinterp_add "PROOF"
     (function 
-       | [VARG_COMMAND c] ->
+       | [VARG_CONSTR c] ->
            (fun () -> (* by (tactic_com exact c) *)
               (* on experimente la synthese d'ise dans exact *)
               by (dyn_exact [Command c]); 
@@ -1460,7 +1460,7 @@ let _ =
 let _ =
   add "PrintConstr"
     (function
-       | [VARG_COMMAND c] -> 
+       | [VARG_CONSTR c] -> 
 	   (fun () ->
 	      Term.constr_display (constr_of_com empty_evd (initial_sign()) c))
        | _ -> bad_vernac_args "PrintConstr")
diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml
index 412575a03b..3329beff53 100644
--- a/toplevel/vernacinterp.ml
+++ b/toplevel/vernacinterp.ml
@@ -25,8 +25,8 @@ type vernac_arg =
   | VARG_NUMBERLIST of int list
   | VARG_IDENTIFIER of identifier
   | VCALL of string * vernac_arg list
-  | VARG_COMMAND of Coqast.t
-  | VARG_COMMANDLIST of Coqast.t list
+  | VARG_CONSTR of Coqast.t
+  | VARG_CONSTRLIST of Coqast.t list
   | VARG_TACTIC of Coqast.t
   | VARG_TACTIC_ARG of tactic_arg
   | VARG_BINDER of identifier list * Coqast.t
@@ -80,8 +80,8 @@ let rec cvt_varg ast =
     | Str(_,s) -> VARG_STRING s
     | Num(_,n) -> VARG_NUMBER n
     | Node(_,"NONE",[]) -> VARG_UNIT
-    | Node(_,"COMMAND",[c]) -> VARG_COMMAND c
-    | Node(_,"COMMANDLIST",l) -> VARG_COMMANDLIST l
+    | Node(_,"CONSTR",[c]) -> VARG_CONSTR c
+    | Node(_,"CONSTRLIST",l) -> VARG_CONSTRLIST l
     | Node(_,"TACTIC",[c]) -> VARG_TACTIC c
     | Node(_,"BINDER",c::idl) ->
         VARG_BINDER(List.map (compose id_of_string nvar_of_ast) idl, c)
diff --git a/toplevel/vernacinterp.mli b/toplevel/vernacinterp.mli
index 98ccd4e357..8f10f8004c 100644
--- a/toplevel/vernacinterp.mli
+++ b/toplevel/vernacinterp.mli
@@ -21,8 +21,8 @@ type vernac_arg =
   | VARG_NUMBERLIST of int list
   | VARG_IDENTIFIER of identifier
   | VCALL of string * vernac_arg list
-  | VARG_COMMAND of Coqast.t
-  | VARG_COMMANDLIST of Coqast.t list
+  | VARG_CONSTR of Coqast.t
+  | VARG_CONSTRLIST of Coqast.t list
   | VARG_TACTIC of Coqast.t
   | VARG_TACTIC_ARG of tactic_arg
   | VARG_BINDER of identifier list * Coqast.t