diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-03-02 09:13:39 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-03-02 09:13:39 +0000 |
| commit | debb95371036f93504cfd49dc74839a9c7ed604e (patch) | |
| tree | 804938a0fcf4d6299bb0d6ae4315a64c08825bc6 /parsing | |
| 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
Diffstat (limited to 'parsing')
| -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 |
4 files changed, 13 insertions, 2 deletions
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 |