diff options
author | 2004-03-02 09:13:39 +0000 | |
---|---|---|
committer | 2004-03-02 09:13:39 +0000 | |
commit | debb95371036f93504cfd49dc74839a9c7ed604e (patch) | |
tree | 804938a0fcf4d6299bb0d6ae4315a64c08825bc6 | |
parent | 26d73ca5440e45d7832935876fa8acdea6277df5 (diff) |
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
-rw-r--r-- | interp/genarg.ml | 5 | ||||
-rw-r--r-- | interp/genarg.mli | 10 | ||||
-rw-r--r-- | parsing/argextend.ml4 | 3 | ||||
-rw-r--r-- | parsing/g_prim.ml4 | 5 | ||||
-rw-r--r-- | parsing/pcoq.ml4 | 5 | ||||
-rw-r--r-- | parsing/pcoq.mli | 2 | ||||
-rw-r--r-- | tactics/extratactics.ml4 | 28 |
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 |