Ajout d'une entrée hyp de type HypArgType pour parser et interpréter les noms d'hypothèses

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

7 files changed, 40 insertions, 18 deletions

diff --git a/interp/genarg.ml b/interp/genarg.ml
index 4ef21df45..d4df7de86 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -26,6 +26,7 @@ type argument_type =
   | PreIdentArgType
   | IntroPatternArgType
   | IdentArgType
+  | HypArgType
   | RefArgType
   (* Specific types *)
   | SortArgType
@@ -115,6 +116,10 @@ let rawwit_ident = IdentArgType
 let globwit_ident = IdentArgType
 let wit_ident = IdentArgType
 
+let rawwit_var = HypArgType
+let globwit_var = HypArgType
+let wit_var = HypArgType
+
 let rawwit_ref = RefArgType
 let globwit_ref = RefArgType
 let wit_ref = RefArgType
diff --git a/interp/genarg.mli b/interp/genarg.mli
index 18f1e33fb..343366ecb 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -61,9 +61,10 @@ BoolArgType                    bool                     bool
 IntArgType                     int                      int
 IntOrVarArgType                int or_var               int
 StringArgType                  string (parsed w/ "")    string
-PreIdentArgType                string (parsed w/o "")   string
-IdentArgType                   identifier               identifier         
+PreIdentArgType                string (parsed w/o "")   (vernac only)
+IdentArgType                   identifier               identifier
 IntroPatternArgType            intro_pattern_expr       intro_pattern_expr
+VarArgType                     identifier               constr
 RefArgType                     reference                global_reference
 ConstrArgType                  constr_expr              constr
 ConstrMayEvalArgType           constr_expr may_eval     constr
@@ -107,6 +108,10 @@ val rawwit_ident : (identifier,'co,'ta) abstract_argument_type
 val globwit_ident : (identifier,'co,'ta) abstract_argument_type
 val wit_ident : (identifier,'co,'ta) abstract_argument_type
 
+val rawwit_var : (identifier located,'co,'ta) abstract_argument_type
+val globwit_var : (identifier located,'co,'ta) abstract_argument_type
+val wit_var : ('co,'co,'ta) abstract_argument_type
+
 val rawwit_ref : (reference,constr_expr,'ta) abstract_argument_type
 val globwit_ref : (global_reference located or_var,rawconstr_and_expr,'ta) abstract_argument_type
 val wit_ref : (global_reference,constr,'ta) abstract_argument_type
@@ -214,6 +219,7 @@ type argument_type =
   | PreIdentArgType
   | IntroPatternArgType
   | IdentArgType
+  | HypArgType
   | RefArgType
   (* Specific types *)
   | SortArgType
diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4
index 6ed6c51e4..34ed30476 100644
--- a/parsing/argextend.ml4
+++ b/parsing/argextend.ml4
@@ -25,6 +25,7 @@ let rec make_rawwit loc = function
   | PreIdentArgType -> <:expr< Genarg.rawwit_pre_ident >>
   | IntroPatternArgType -> <:expr< Genarg.rawwit_intro_pattern >>
   | IdentArgType -> <:expr< Genarg.rawwit_ident >>
+  | HypArgType -> <:expr< Genarg.rawwit_var >>
   | RefArgType -> <:expr< Genarg.rawwit_ref >>
   | SortArgType -> <:expr< Genarg.rawwit_sort >>
   | ConstrArgType -> <:expr< Genarg.rawwit_constr >>
@@ -50,6 +51,7 @@ let rec make_globwit loc = function
   | PreIdentArgType -> <:expr< Genarg.globwit_pre_ident >>
   | IntroPatternArgType -> <:expr< Genarg.globwit_intro_pattern >>
   | IdentArgType -> <:expr< Genarg.globwit_ident >>
+  | HypArgType -> <:expr< Genarg.globwit_var >>
   | RefArgType -> <:expr< Genarg.globwit_ref >>
   | QuantHypArgType -> <:expr< Genarg.globwit_quant_hyp >>
   | SortArgType -> <:expr< Genarg.globwit_sort >>
@@ -75,6 +77,7 @@ let rec make_wit loc = function
   | PreIdentArgType -> <:expr< Genarg.wit_pre_ident >>
   | IntroPatternArgType -> <:expr< Genarg.wit_intro_pattern >>
   | IdentArgType -> <:expr< Genarg.wit_ident >>
+  | HypArgType -> <:expr< Genarg.wit_var >>
   | RefArgType -> <:expr< Genarg.wit_ref >>
   | QuantHypArgType -> <:expr< Genarg.wit_quant_hyp >>
   | SortArgType -> <:expr< Genarg.wit_sort >>
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index 7a1b910c6..03e02fc89 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -72,12 +72,15 @@ open Q
 
 GEXTEND Gram
   GLOBAL: ident natural integer bigint string preident ast
-    astlist qualid reference dirpath identref name base_ident var;
+    astlist qualid reference dirpath identref name base_ident var hyp;
 
  (* Compatibility: Prim.var is a synonym of Prim.ident *)
   var:
     [ [ id = ident -> id ] ]
   ;
+  hyp:
+    [ [ id = ident -> id ] ]
+  ;
   metaident:
     [ [ s = METAIDENT -> Nmeta (loc,s) ] ]
   ;
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 5aad710c7..5ef39419c 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -310,7 +310,10 @@ module Prim =
     let string = gec_gen rawwit_string "string"
     let reference = make_gen_entry uprim rawwit_ref "reference"
 
-    (* A synonym of ident, for compatibility *)
+    (* parsed like ident but interpreted as a term *)
+    let hyp = gec_gen rawwit_ident "hyp"
+
+    (* synonym of hyp/ident (before semantics split) for v7 compatibility *)
     let var = gec_gen rawwit_ident "var"
 
     let name = Gram.Entry.create "Prim.name"
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 68977fb3d..2bdd27eb9 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -120,6 +120,8 @@ module Prim :
     val reference : reference Gram.Entry.e
     val dirpath : dir_path Gram.Entry.e
     val ne_string : string Gram.Entry.e
+    val hyp : identifier Gram.Entry.e
+    (* v7 only entries *)
     val astpat: typed_ast Gram.Entry.e
     val ast : Coqast.t Gram.Entry.e
     val astlist : Coqast.t list Gram.Entry.e
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 22450cf98..6eab2a769 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -23,7 +23,7 @@ TACTIC EXTEND Rewrite
 END
 
 TACTIC EXTEND RewriteIn
- [ "Rewrite" orient(b) constr_with_bindings(c) "in" ident(h) ] ->
+ [ "Rewrite" orient(b) constr_with_bindings(c) "in" hyp(h) ] ->
  [general_rewrite_in b h c]
 END
 
@@ -34,7 +34,7 @@ TACTIC EXTEND Replace
 END
 
 TACTIC EXTEND ReplaceIn
-  [ "Replace" constr(c1) "with" constr(c2) "in" ident(h) ] ->
+  [ "Replace" constr(c1) "with" constr(c2) "in" hyp(h) ] ->
     [ replace_in h c1 c2 ]
 END
 
@@ -51,17 +51,17 @@ TACTIC EXTEND Replaceterm
 END
 
 TACTIC EXTEND ReplacetermInleft
-  [ "Replace"  "->" constr(c) "in" ident(h) ]
+  [ "Replace"  "->" constr(c) "in" hyp(h) ]
   -> [ replace_term_in_left c h ]
 END
 
 TACTIC EXTEND ReplacetermInright
-  [ "Replace"  "<-" constr(c) "in" ident(h) ]
+  [ "Replace"  "<-" constr(c) "in" hyp(h) ]
   -> [ replace_term_in_right c h ]
 END
 
 TACTIC EXTEND ReplacetermIn
-  [ "Replace" constr(c) "in" ident(h) ]
+  [ "Replace" constr(c) "in" hyp(h) ]
   -> [ replace_term_in c h ]
 END
 
@@ -88,14 +88,14 @@ END
 
 TACTIC EXTEND ConditionalRewriteIn
   [ "Conditional" tactic(tac) "Rewrite" orient(b) constr_with_bindings(c)
-    "in" ident(h) ]
+    "in" hyp(h) ]
     -> [ conditional_rewrite_in b h (snd tac) c ]
 END
 
 TACTIC EXTEND DependentRewrite
-| [ "Dependent" "Rewrite" orient(b) ident(id) ] -> [ substHypInConcl b id ]
+| [ "Dependent" "Rewrite" orient(b) hyp(id) ] -> [ substHypInConcl b id ]
 | [ "CutRewrite" orient(b) constr(eqn) ] -> [ substConcl b eqn ]
-| [ "CutRewrite" orient(b) constr(eqn) "in" ident(id) ]
+| [ "CutRewrite" orient(b) constr(eqn) "in" hyp(id) ]
       -> [ substHyp b eqn id ]
 END
 
@@ -184,16 +184,16 @@ open Inv
 open Leminv
 
 VERNAC COMMAND EXTEND DeriveInversionClear
-  [ "Derive" "Inversion_clear" ident(na) ident(id) ]
+  [ "Derive" "Inversion_clear" ident(na) hyp(id) ]
   -> [ inversion_lemma_from_goal 1 na id Term.mk_Prop false inv_clear_tac ]
 
-| [ "Derive" "Inversion_clear" natural(n) ident(na) ident(id) ]
+| [ "Derive" "Inversion_clear" natural(n) ident(na) hyp(id) ]
   -> [ inversion_lemma_from_goal n na id Term.mk_Prop false inv_clear_tac ]
 
 | [ "Derive" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort(s) ]
   -> [ add_inversion_lemma_exn na c s false inv_clear_tac ]
 
-| [ "Derive" "Inversion_clear"  ident(na) "with" constr(c) ]
+| [ "Derive" "Inversion_clear" ident(na) "with" constr(c) ]
   -> [ add_inversion_lemma_exn na c (Rawterm.RProp Term.Null) false inv_clear_tac ]
 END
 
@@ -207,10 +207,10 @@ VERNAC COMMAND EXTEND DeriveInversion
 | [ "Derive" "Inversion" ident(na) "with" constr(c) ]
   -> [ add_inversion_lemma_exn na c (RProp Null) false half_inv_tac ]
 
-| [ "Derive" "Inversion" ident(na) ident(id) ]
+| [ "Derive" "Inversion" ident(na) hyp(id) ]
   -> [ inversion_lemma_from_goal 1 na id Term.mk_Prop false half_inv_tac ]
 
-| [ "Derive" "Inversion" natural(n) ident(na) ident(id) ]
+| [ "Derive" "Inversion" natural(n) ident(na) hyp(id) ]
   -> [ inversion_lemma_from_goal n na id Term.mk_Prop false half_inv_tac ]
 END
 
@@ -227,7 +227,7 @@ END
 (* Subst *)
 
 TACTIC EXTEND Subst
-| [ "Subst" ne_ident_list(l) ] -> [ subst l ]
+| [ "Subst" ne_var_list(l) ] -> [ subst l ]
 | [ "Subst" ] -> [ subst_all ]
 END