Fin du changement comarg -> constrarg

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

4 files changed, 71 insertions, 71 deletions

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 3814af4f26..f19e373733 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -21,10 +21,10 @@ GEXTEND Gram
       | "-"; n = Prim.number -> Coqast.Num (Ast.loc n, ( - Ast.num_of_ast n))
       ] ]
   ;
-  comarg:
+  constrarg:
     [ [ c = Constr.constr -> <:ast< (COMMAND $c) >> ] ]
   ;
-  lcomarg:
+  lconstrarg:
     [ [ c = Constr.lconstr -> <:ast< (COMMAND $c) >> ] ]
   ;
   ne_identarg_list:
@@ -34,8 +34,8 @@ GEXTEND Gram
     [ [ n = numarg; l = ne_num_list -> n :: l | n = numarg -> [n] ] ]
   ;
   pattern_occ:
-    [ [ nl = ne_num_list; c = comarg -> <:ast< (PATTERN $c ($LIST $nl)) >>
-      | c = comarg -> <:ast< (PATTERN $c) >> ] ]
+    [ [ nl = ne_num_list; c = constrarg -> <:ast< (PATTERN $c ($LIST $nl)) >>
+      | c = constrarg -> <:ast< (PATTERN $c) >> ] ]
   ;
   ne_pattern_list:
     [ [ l = LIST1 pattern_occ -> l ] ]
@@ -70,39 +70,39 @@ GEXTEND Gram
          | -> <:ast< (LISTPATTERN) >> ]]
   ;
   simple_binding:
-    [ [ id = identarg; ":="; c = comarg -> <:ast< (BINDING $id $c) >>
-      | n = numarg; ":="; c = comarg -> <:ast< (BINDING $n $c) >> ] ]
+    [ [ id = identarg; ":="; c = constrarg -> <:ast< (BINDING $id $c) >>
+      | n = numarg; ":="; c = constrarg -> <:ast< (BINDING $n $c) >> ] ]
   ;
   simple_binding_list:
     [ [ b = simple_binding; l = simple_binding_list -> b :: l | -> [] ] ]
   ;
   com_binding_list:
-    [ [ c = comarg; bl = com_binding_list -> <:ast< (BINDING $c) >> :: bl
+    [ [ c = constrarg; bl = com_binding_list -> <:ast< (BINDING $c) >> :: bl
       | -> [] ] ]
   ;
   binding_list:
-    [ [ c1 = comarg; ":="; c2 = comarg; bl = simple_binding_list ->
+    [ [ c1 = constrarg; ":="; c2 = constrarg; bl = simple_binding_list ->
           let id = match c1 with 
             | Coqast.Node(_,"COMMAND",[c]) -> coerce_to_var "c1" c
             | _ -> assert false
           in <:ast<(BINDINGS (BINDING ($VAR $id) $c2) ($LIST $bl))>>
-      | n = numarg; ":="; c = comarg; bl = simple_binding_list ->
+      | n = numarg; ":="; c = constrarg; bl = simple_binding_list ->
           <:ast<(BINDINGS (BINDING $n $c) ($LIST $bl))>>
-      | c1 = comarg; bl = com_binding_list ->
+      | c1 = constrarg; bl = com_binding_list ->
           <:ast<(BINDINGS (BINDING $c1) ($LIST $bl))>>
       | -> <:ast<(BINDINGS)>> ] ]
   ;
   with_binding_list:
     [ [ "with"; l = binding_list -> l | -> <:ast<(BINDINGS)>> ] ]
   ;
-  comarg_binding_list:
-    [ [ c = comarg; l = with_binding_list -> [c; l] ] ]
+  constrarg_binding_list:
+    [ [ c = constrarg; l = with_binding_list -> [c; l] ] ]
   ;
   numarg_binding_list:
     [ [ n = numarg; l = with_binding_list -> [n; l] ] ]
   ;
-  comarg_list:
-    [ [ c = comarg; l = comarg_list -> c :: l | -> [] ] ]
+  constrarg_list:
+    [ [ c = constrarg; l = constrarg_list -> c :: l | -> [] ] ]
   ;
   unfold_occ:
     [ [ nl = ne_num_list; c = identarg -> <:ast< (UNFOLD $c ($LIST $nl)) >>
@@ -129,7 +129,7 @@ GEXTEND Gram
       | IDENT "Compute" -> <:ast< (Cbv (Beta) (Delta) (Iota)) >>
       | IDENT "Unfold"; ul = ne_unfold_occ_list ->
           <:ast< (Unfold ($LIST ul)) >>
-      | IDENT "Fold"; cl = comarg_list -> <:ast< (Fold ($LIST cl)) >>
+      | IDENT "Fold"; cl = constrarg_list -> <:ast< (Fold ($LIST cl)) >>
       | IDENT "Pattern"; pl = ne_pattern_list ->
           <:ast< (Pattern ($LIST $pl)) >> ] ]
   ;
@@ -155,12 +155,12 @@ GEXTEND Gram
       | -> Coqast.Str(loc,"NoAutoArg")  ] ]
   ;
   fixdecl:
-    [ [ id = identarg; n = numarg; ":"; c = comarg; fd = fixdecl ->
+    [ [ id = identarg; n = numarg; ":"; c = constrarg; fd = fixdecl ->
           <:ast< (FIXEXP $id $n $c) >> :: fd
       | -> [] ] ]
   ;
   cofixdecl:
-    [ [ id = identarg; ":"; c = comarg; fd = cofixdecl ->
+    [ [ id = identarg; ":"; c = constrarg; fd = cofixdecl ->
           <:ast< (COFIXEXP $id $c) >> :: fd
       | -> [] ] ]
   ;
@@ -241,46 +241,46 @@ GEXTEND Gram
 	  IDENT "after"; id2 = identarg -> <:ast< (IntroMove $id2) >>
       | IDENT "Intro"; id = identarg -> <:ast< (Intro $id) >>
       | IDENT "Intro" -> <:ast< (Intro) >>
-      | IDENT "Apply"; cl = comarg_binding_list ->
+      | IDENT "Apply"; cl = constrarg_binding_list ->
           <:ast< (Apply ($LIST $cl)) >>
-      | IDENT "Elim"; cl = comarg_binding_list; "using";
-        el = comarg_binding_list ->
+      | IDENT "Elim"; cl = constrarg_binding_list; "using";
+        el = constrarg_binding_list ->
           <:ast< (Elim ($LIST $cl) ($LIST $el)) >>
-      | IDENT "Elim"; cl = comarg_binding_list ->
+      | IDENT "Elim"; cl = constrarg_binding_list ->
           <:ast< (Elim ($LIST $cl)) >>
       | IDENT "Assumption" -> <:ast< (Assumption) >>
       | IDENT "Contradiction" -> <:ast< (Contradiction) >>
-      | IDENT "Exact"; c = comarg -> <:ast< (Exact $c) >>
-      | IDENT "OldElim"; c = comarg -> <:ast< (OldElim $c) >>
-      | IDENT "ElimType"; c = comarg -> <:ast< (ElimType $c) >>
-      | IDENT "Case"; cl = comarg_binding_list ->
+      | IDENT "Exact"; c = constrarg -> <:ast< (Exact $c) >>
+      | IDENT "OldElim"; c = constrarg -> <:ast< (OldElim $c) >>
+      | IDENT "ElimType"; c = constrarg -> <:ast< (ElimType $c) >>
+      | IDENT "Case"; cl = constrarg_binding_list ->
           <:ast< (Case ($LIST $cl)) >>
-      | IDENT "CaseType"; c = comarg -> <:ast< (CaseType $c) >>
+      | IDENT "CaseType"; c = constrarg -> <:ast< (CaseType $c) >>
       | IDENT "Destruct"; s = identarg -> <:ast< (Destruct $s) >>
       | IDENT "Destruct"; n = numarg -> <:ast< (Destruct $n) >>
-      | IDENT "Decompose"; IDENT "Record" ; c = comarg -> 
+      | IDENT "Decompose"; IDENT "Record" ; c = constrarg -> 
              <:ast< (DecomposeAnd $c) >>
-      | IDENT "Decompose"; IDENT "Sum"; c = comarg -> 
+      | IDENT "Decompose"; IDENT "Sum"; c = constrarg -> 
              <:ast< (DecomposeOr $c) >>
-      | IDENT "Decompose"; "["; l = ne_identarg_list; "]"; c = comarg ->
+      | IDENT "Decompose"; "["; l = ne_identarg_list; "]"; c = constrarg ->
           <:ast< (DecomposeThese (CLAUSE ($LIST $l)) $c) >>
       |	IDENT "First" ; "["; l = LIST0 tactic_com_list SEP "|"; "]" ->
           <:ast<(FIRST ($LIST $l))>>
       |	IDENT "Solve" ; "["; l = LIST0 tactic_com_list SEP "|"; "]" ->
           <:ast<(TCLSOLVE ($LIST $l))>>
-      | IDENT "Cut"; c = comarg -> <:ast< (Cut $c) >>
-      | IDENT "Specialize"; n = numarg; lcb = comarg_binding_list ->
+      | IDENT "Cut"; c = constrarg -> <:ast< (Cut $c) >>
+      | IDENT "Specialize"; n = numarg; lcb = constrarg_binding_list ->
           <:ast< (Specialize $n ($LIST $lcb))>>
-      | IDENT "Specialize"; lcb = comarg_binding_list ->
+      | IDENT "Specialize"; lcb = constrarg_binding_list ->
           <:ast< (Specialize ($LIST $lcb)) >>
-      | IDENT "Generalize"; lc = comarg_list ->
+      | IDENT "Generalize"; lc = constrarg_list ->
           <:ast< (Generalize ($LIST $lc)) >>
-      | IDENT "Generalize"; IDENT "Dependent"; c = comarg ->
+      | IDENT "Generalize"; IDENT "Dependent"; c = constrarg ->
           <:ast< (GeneralizeDep $c) >>
-      | IDENT "Let"; s = identarg; ":="; c = comarg; "in";
+      | IDENT "Let"; s = identarg; ":="; c = constrarg; "in";
 	  l = ne_pattern_hyp_list -> 
 	    <:ast< (LetTac $s $c (LETPATTERNS ($LIST $l))) >>
-      | IDENT "LApply"; c = comarg -> <:ast< (CutAndApply $c) >>
+      | IDENT "LApply"; c = constrarg -> <:ast< (CutAndApply $c) >>
       | IDENT "Clear"; l = ne_identarg_list -> 
                 <:ast< (Clear (CLAUSE ($LIST $l))) >>
       | IDENT "Move"; id1 = identarg; IDENT "after"; id2 = identarg -> 
@@ -301,18 +301,18 @@ GEXTEND Gram
       | IDENT "Constructor" -> <:ast<(Constructor) >>
       | IDENT "Reflexivity" -> <:ast< (Reflexivity) >>
       | IDENT "Symmetry" -> <:ast< (Symmetry) >>
-      | IDENT "Transitivity"; c = comarg -> <:ast< (Transitivity $c) >>
-      | IDENT "Absurd"; c = comarg -> <:ast< (Absurd $c) >>
+      | IDENT "Transitivity"; c = constrarg -> <:ast< (Transitivity $c) >>
+      | IDENT "Absurd"; c = constrarg -> <:ast< (Absurd $c) >>
       | IDENT "Idtac" -> <:ast< (Idtac) >>
       | IDENT "Fail" -> <:ast< (Fail) >>
       | "("; tcl = tactic_com_list; ")" -> tcl
       | r = red_tactic; cl = clausearg -> <:ast< (Reduce (REDEXP $r) $cl) >>
       (* Change ne doit pas s'appliquer dans un Definition t := Eval ... *)
-      | IDENT "Change"; c = comarg; cl = clausearg ->
+      | IDENT "Change"; c = constrarg; cl = clausearg ->
 	  <:ast< (Change $c $cl) >> 
       | IDENT "ML"; s = Prim.string -> <:ast< (MLTACTIC $s) >> ]
 
-    | [ id = identarg; l = comarg_list ->
+    | [ id = identarg; l = constrarg_list ->
           match (isMeta (nvar_of_ast id), l) with
             | (true, []) -> id
             | (false, _) -> <:ast< (CALL $id ($LIST $l)) >>
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index a27fa3cd98..418188be5f 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -273,13 +273,13 @@ module Tactic =
     
     let binding_list = gec "binding_list"
     let com_binding_list = gec_list "com_binding_list"
-    let comarg = gec "comarg"
-    let comarg_binding_list = gec_list "comarg_binding_list"
+    let constrarg = gec "constrarg"
+    let constrarg_binding_list = gec_list "constrarg_binding_list"
     let numarg_binding_list = gec_list "numarg_binding_list"
-    let lcomarg_binding_list = gec_list "lcomarg_binding_list"
-    let comarg_list = gec_list "comarg_list"
+    let lconstrarg_binding_list = gec_list "lconstrarg_binding_list"
+    let constrarg_list = gec_list "constrarg_list"
     let identarg = gec "identarg"
-    let lcomarg = gec "lcomarg"
+    let lconstrarg = gec "lconstrarg"
     let clausearg = gec "clausearg"
     let ne_identarg_list = gec_list "ne_identarg_list"
     let ne_num_list = gec_list "ne_num_list"
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index e271a5bd07..d7313e296c 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -94,14 +94,14 @@ module Tactic :
     val clausearg : Coqast.t Gram.Entry.e
     val cofixdecl : Coqast.t list Gram.Entry.e
     val com_binding_list : Coqast.t list Gram.Entry.e
-    val comarg : Coqast.t Gram.Entry.e
-    val comarg_binding_list : Coqast.t list Gram.Entry.e
-    val comarg_list : Coqast.t list Gram.Entry.e
+    val constrarg : Coqast.t Gram.Entry.e
+    val constrarg_binding_list : Coqast.t list Gram.Entry.e
+    val constrarg_list : Coqast.t list Gram.Entry.e
     val fixdecl : Coqast.t list Gram.Entry.e
     val identarg : Coqast.t Gram.Entry.e
     val intropattern : Coqast.t Gram.Entry.e
-    val lcomarg : Coqast.t Gram.Entry.e
-    val lcomarg_binding_list : Coqast.t list Gram.Entry.e
+    val lconstrarg : Coqast.t Gram.Entry.e
+    val lconstrarg_binding_list : Coqast.t list Gram.Entry.e
     val ne_identarg_list : Coqast.t list Gram.Entry.e
     val ne_intropattern : Coqast.t Gram.Entry.e
     val ne_num_list : Coqast.t list Gram.Entry.e
diff --git a/tactics/Equality.v b/tactics/Equality.v
index 9d6d343708..66f5252a99 100644
--- a/tactics/Equality.v
+++ b/tactics/Equality.v
@@ -58,10 +58,10 @@ with hintbase_list: List :=
        [(REDEXP (Explicit ($LIST $b))) ($LIST $tail) ]
 
 with hintbase: List := 
-  onehint_lr [ comarg($c) "LR" ] -> [(REDEXP (LR $c))]
-| onehint_rl  [ comarg($c) "RL" ] -> [(REDEXP (RL $c))]
-| conshint_lr [ comarg($c) "LR" hintbase($tail)] -> [(REDEXP (LR $c)) ($LIST $tail)]
-| conshint_rl [ comarg($c) "RL" hintbase($tail)] -> [(REDEXP (RL $c)) ($LIST $tail)]
+  onehint_lr [ constrarg($c) "LR" ] -> [(REDEXP (LR $c))]
+| onehint_rl  [ constrarg($c) "RL" ] -> [(REDEXP (RL $c))]
+| conshint_lr [ constrarg($c) "LR" hintbase($tail)] -> [(REDEXP (LR $c)) ($LIST $tail)]
+| conshint_rl [ constrarg($c) "RL" hintbase($tail)] -> [(REDEXP (RL $c)) ($LIST $tail)]
 
 with simple_tactic := 
  AutoRewrite [ "AutoRewrite" "[" hintbase_list($lbase) "]"
@@ -69,7 +69,7 @@ with simple_tactic :=
   [(AutoRewrite (REDEXP (BaseList ($LIST $lbase))) ($LIST $laa))].
 
 Grammar tactic simple_tactic :=
-  replace [ "Replace" comarg($c1) "with" comarg($c2) ] -> [(Replace $c1 $c2)]
+  replace [ "Replace" constrarg($c1) "with" constrarg($c2) ] -> [(Replace $c1 $c2)]
 
 | deqhyp   [ "Simplify_eq" identarg($id) ] -> [(DEqHyp $id)]
 | deqconcl [ "Simplify_eq" ] -> [(DEqConcl)]
@@ -80,31 +80,31 @@ Grammar tactic simple_tactic :=
 | inj    [ "Injection" ] -> [(Inj)]
 | inj_id [ "Injection" identarg($id) ] -> [(InjHyp $id)]
 
-| rewriteLR [ "Rewrite" "->" comarg_binding_list($cl) ] -> [(RewriteLR ($LIST $cl))]
-| rewriteRL [ "Rewrite" "<-" comarg_binding_list($cl) ] -> [(RewriteRL ($LIST $cl))]
-| rewrite [ "Rewrite" comarg_binding_list($cl) ] -> [(RewriteLR ($LIST $cl))]
+| rewriteLR [ "Rewrite" "->" constrarg_binding_list($cl) ] -> [(RewriteLR ($LIST $cl))]
+| rewriteRL [ "Rewrite" "<-" constrarg_binding_list($cl) ] -> [(RewriteRL ($LIST $cl))]
+| rewrite [ "Rewrite" constrarg_binding_list($cl) ] -> [(RewriteLR ($LIST $cl))]
 
-| condrewriteLR [ "Conditional" tactic_com($tac) "Rewrite" "->" comarg_binding_list($cl) ] -> [(CondRewriteLR (TACTIC $tac) ($LIST $cl))]
-| condrewriteRL [ "Conditional" tactic_com($tac) "Rewrite" "<-" comarg_binding_list($cl) ] -> [(CondRewriteRL (TACTIC $tac) ($LIST $cl))]
-| condrewrite [ "Conditional" tactic_com($tac) "Rewrite" comarg_binding_list($cl) ] -> [(CondRewriteLR (TACTIC $tac) ($LIST $cl))]
+| condrewriteLR [ "Conditional" tactic_com($tac) "Rewrite" "->" constrarg_binding_list($cl) ] -> [(CondRewriteLR (TACTIC $tac) ($LIST $cl))]
+| condrewriteRL [ "Conditional" tactic_com($tac) "Rewrite" "<-" constrarg_binding_list($cl) ] -> [(CondRewriteRL (TACTIC $tac) ($LIST $cl))]
+| condrewrite [ "Conditional" tactic_com($tac) "Rewrite" constrarg_binding_list($cl) ] -> [(CondRewriteLR (TACTIC $tac) ($LIST $cl))]
 
-| rewrite_in [ "Rewrite" comarg_binding_list($cl) "in" identarg($h) ]
+| rewrite_in [ "Rewrite" constrarg_binding_list($cl) "in" identarg($h) ]
        -> [(RewriteLRin $h ($LIST $cl))]
-| rewriteRL_in [ "Rewrite" "->" comarg_binding_list($cl) "in" identarg($h) ]
+| rewriteRL_in [ "Rewrite" "->" constrarg_binding_list($cl) "in" identarg($h) ]
        -> [(RewriteLRin $h ($LIST $cl))]
-| rewriteLR_in [ "Rewrite" "<-" comarg_binding_list($cl) "in" identarg($h) ]
+| rewriteLR_in [ "Rewrite" "<-" constrarg_binding_list($cl) "in" identarg($h) ]
        -> [(RewriteRLin $h ($LIST $cl))]
 
 | condrewriteLRin 
-  [ "Conditional" tactic_com($tac) "Rewrite" "->" comarg_binding_list($cl) 
+  [ "Conditional" tactic_com($tac) "Rewrite" "->" constrarg_binding_list($cl) 
 	"in" identarg($h) ] ->
 	   [(CondRewriteLRin (TACTIC $tac) $h ($LIST $cl))]
 | condrewriteRLin 
-  [ "Conditional" tactic_com($tac) "Rewrite" "<-" comarg_binding_list($cl) 
+  [ "Conditional" tactic_com($tac) "Rewrite" "<-" constrarg_binding_list($cl) 
 	"in" identarg($h)] ->
   	   [(CondRewriteRLin (TACTIC $tac) $h ($LIST $cl))]
 | condrewritein 
-  [ "Conditional" tactic_com($tac) "Rewrite" comarg_binding_list($cl) "in" identarg($h) ] 
+  [ "Conditional" tactic_com($tac) "Rewrite" constrarg_binding_list($cl) "in" identarg($h) ] 
         -> [(CondRewriteLRin (TACTIC $tac) $h ($LIST $cl))]
 
 | DRewriteLR [ "Dependent" "Rewrite" "->" identarg($id) ]
@@ -112,11 +112,11 @@ Grammar tactic simple_tactic :=
 | DRewriteRL [ "Dependent" "Rewrite" "<-" identarg($id) ]
        -> [(SubstHypInConcl_RL $id)]
 
-| cutrewriteLR [ "CutRewrite" "->" comarg($eqn) ] -> [(SubstConcl_LR $eqn)]
-| cutrewriteLRin [ "CutRewrite" "->" comarg($eqn) "in" identarg($id) ]
+| cutrewriteLR [ "CutRewrite" "->" constrarg($eqn) ] -> [(SubstConcl_LR $eqn)]
+| cutrewriteLRin [ "CutRewrite" "->" constrarg($eqn) "in" identarg($id) ]
       -> [(SubstHyp_LR $eqn $id)]
-| cutrewriteRL [ "CutRewrite" "<-" comarg($eqn) ] -> [(SubstConcl_RL $eqn)]
-| cutrewriteRLin [ "CutRewrite" "<-" comarg($eqn) "in" identarg($id) ]
+| cutrewriteRL [ "CutRewrite" "<-" constrarg($eqn) ] -> [(SubstConcl_RL $eqn)]
+| cutrewriteRLin [ "CutRewrite" "<-" constrarg($eqn) "in" identarg($id) ]
       -> [(SubstHyp_RL $eqn $id)].
 
 Syntax tactic level 0: