Les réduction dans les hypothèses s'appliquent maintenant au corps de la définition en cas de LetIn (l'horrible syntaxe 'Unfold toto in (Type of hyp)' permet de forcer la réduction dans le type

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

3 files changed, 24 insertions, 11 deletions

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 70aaba18d..c374f5955 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -54,6 +54,9 @@ GEXTEND Gram
     [ [ id = Constr.ident -> id
       | "?"; n = Prim.number -> <:ast< (COMMAND (META $n)) >> ] ]
   ;
+  idmetahyp:
+    [ [ id = idmeta_arg -> <:ast< (INHYP $id) >> ] ]
+  ;
   qualidarg:
     [ [ l = Constr.qualid -> <:ast< (QUALIDARG ($LIST l)) >>
       | "?"; n = Prim.number -> <:ast< (QUALIDMETA $n) >> ] ]
@@ -94,8 +97,8 @@ GEXTEND Gram
   ne_identarg_list:
     [ [ l = LIST1 identarg -> l ] ]
   ;
-  ne_idmeta_arg_list:
-    [ [ l = LIST1 idmeta_arg -> l ] ]
+  ne_idmetahyp_list:
+    [ [ l = LIST1 idmetahyp -> l ] ]
   ;
   ne_qualidarg_list:
     [ [ l = LIST1 qualidarg -> l ] ]
@@ -211,8 +214,15 @@ GEXTEND Gram
       | IDENT "Pattern"; pl = ne_pattern_list ->
           <:ast< (Pattern ($LIST $pl)) >> ] ]
   ;
+  hypident:
+    [ [ id = identarg -> <:ast< (INHYP $id) >>
+      | "("; "Type"; "of"; id = identarg; ")" -> <:ast< (INHYPTYPE $id) >> ] ]
+  ;
+  ne_hyp_list:
+    [ [ l = LIST1 hypident -> l ] ]
+  ;
   clausearg:
-    [ [ "in"; idl = ne_identarg_list -> <:ast< (CLAUSE ($LIST idl)) >>
+    [ [ "in"; idl = ne_hyp_list -> <:ast< (CLAUSE ($LIST idl)) >>
       | -> <:ast< (CLAUSE) >> ] ]
   ;
   fixdecl:
@@ -225,9 +235,6 @@ GEXTEND Gram
           <:ast< (COFIXEXP $id $c) >> :: fd
       | -> [] ] ]
   ;
- END
-
-GEXTEND Gram
   simple_tactic:
     [ [ IDENT "Fix"; n = pure_numarg -> <:ast< (Fix $n) >>
       | IDENT "Fix"; id = identarg; n = pure_numarg -> <:ast< (Fix $id $n) >>
@@ -300,8 +307,8 @@ GEXTEND Gram
              <:ast< (DecomposeAnd $c) >>
       | IDENT "Decompose"; IDENT "Sum"; c = constrarg -> 
              <:ast< (DecomposeOr $c) >>
-      | IDENT "Decompose"; "["; l = ne_identarg_list; "]"; c = constrarg ->
-          <:ast< (DecomposeThese (CLAUSE ($LIST $l)) $c) >>
+      | IDENT "Decompose"; "["; l = ne_qualidarg_list; "]"; c = constrarg ->
+          <:ast< (DecomposeThese $c ($LIST $l)) >>
       | IDENT "Cut"; c = constrarg -> <:ast< (Cut $c) >>
       | IDENT "Specialize"; n = pure_numarg; lcb = constrarg_binding_list ->
           <:ast< (Specialize $n ($LIST $lcb))>>
@@ -314,7 +321,7 @@ GEXTEND Gram
       | IDENT "LetTac"; s = identarg; ":="; c = constrarg; p = clause_pattern->
 	  <:ast< (LetTac $s $c $p) >>
       | IDENT "LApply"; c = constrarg -> <:ast< (CutAndApply $c) >>
-      | IDENT "Clear"; l = ne_idmeta_arg_list -> 
+      | IDENT "Clear"; l = ne_idmetahyp_list -> 
                 <:ast< (Clear (CLAUSE ($LIST $l))) >>
       | IDENT "Move"; id1 = identarg; IDENT "after"; id2 = identarg -> 
                 <:ast< (MoveDep $id1 $id2) >>
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index ff103ae2c..849d2639c 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -292,7 +292,9 @@ module Tactic =
     let constrarg_list = gec_list "constrarg_list"
     let ident_or_constrarg = gec "ident_or_constrarg"
     let identarg = gec "identarg"
+    let hypident = gec "hypident"
     let idmeta_arg = gec "idmeta_arg"
+    let idmetahyp = gec "idmetahyp"
     let qualidarg = gec "qualidarg"
     let qualidconstarg = gec "qualidconstarg"
     let input_fun = gec "input_fun"
@@ -307,7 +309,8 @@ module Tactic =
     let match_rule = gec "match_rule"
     let match_list = gec_list "match_list"
     let ne_identarg_list = gec_list "ne_identarg_list"
-    let ne_idmeta_arg_list = gec_list "ne_idmeta_arg_list"
+    let ne_hyp_list = gec_list "ne_hyp_list"
+    let ne_idmetahyp_list = gec_list "ne_idmetahyp_list"
     let ne_qualidarg_list = gec_list "ne_qualidarg_list"
     let ne_qualidconstarg_list = gec_list "ne_qualidconstarg_list"
     let ne_pattern_list = gec_list "ne_pattern_list"
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 30773eaa6..b9c77509e 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -116,7 +116,9 @@ module Tactic :
     val fixdecl : Coqast.t list Gram.Entry.e
     val ident_or_constrarg : Coqast.t Gram.Entry.e
     val identarg : Coqast.t Gram.Entry.e
+    val hypident : Coqast.t Gram.Entry.e
     val idmeta_arg : Coqast.t Gram.Entry.e
+    val idmetahyp : Coqast.t Gram.Entry.e
     val qualidarg : Coqast.t Gram.Entry.e
     val qualidconstarg : Coqast.t Gram.Entry.e
     val input_fun : Coqast.t Gram.Entry.e
@@ -132,7 +134,8 @@ module Tactic :
     val match_rule : Coqast.t Gram.Entry.e
     val match_list : Coqast.t list Gram.Entry.e
     val ne_identarg_list : Coqast.t list Gram.Entry.e
-    val ne_idmeta_arg_list : Coqast.t list Gram.Entry.e
+    val ne_hyp_list : Coqast.t list Gram.Entry.e
+    val ne_idmetahyp_list : Coqast.t list Gram.Entry.e
     val ne_qualidarg_list : Coqast.t list Gram.Entry.e
     val ne_qualidconstarg_list : Coqast.t list Gram.Entry.e
     val ne_intropattern : Coqast.t Gram.Entry.e