diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-08-31 19:57:54 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-08-31 19:57:54 +0000 |
| commit | d43364dc29b7f5a5612234d61af0856a6f3348b8 (patch) | |
| tree | 1766b33045141da8eadd8dc4275bedc2244103d9 /parsing/g_vernacnew.ml4 | |
| parent | b0579cf0d372f8d79f6f776149c7dc3f59f29181 (diff) | |
'Assumptions' sur le modèle général des lieurs
Syntaxe à la ML pour les constructeurs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4284 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/g_vernacnew.ml4')
| -rw-r--r-- | parsing/g_vernacnew.ml4 | 27 |
1 files changed, 19 insertions, 8 deletions
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4 index 02812d6de..d73ba26ea 100644 --- a/parsing/g_vernacnew.ml4 +++ b/parsing/g_vernacnew.ml4 @@ -102,11 +102,12 @@ GEXTEND Gram VernacStartTheoremProof (thm, id, (bl, c), false, (fun _ _ -> ())) | (f,d,e) = def_token; id = base_ident; b = def_body -> VernacDefinition (d, id, b, f, e) - | stre = assumption_token; bl = LIST1 assum_coe -> - VernacAssumption (stre, flatten_assum bl) - | stre = assumptions_token; bl = LIST1 assum_coe -> - test_plurial_form bl; + | stre = assumption_token; bl = assum_list -> VernacAssumption (stre, flatten_assum bl) + | stre = assumptions_token; bl = assum_list -> + let l = flatten_assum bl in + test_plurial_form l; + VernacAssumption (stre, l) (* Gallina inductive declarations *) | (* Non port (?) : OPT[IDENT "Mutual"];*) f = finite_token; indl = LIST1 inductive_definition SEP "with" -> @@ -152,6 +153,7 @@ GEXTEND Gram assumptions_token: [ [ IDENT "Hypotheses" -> (Local, Logical) | IDENT "Variables" -> (Local, Definitional) + | IDENT "Axioms" -> (Global, Logical) | IDENT "Parameters" -> (Global, Definitional) ] ] ; finite_token: @@ -271,9 +273,15 @@ GEXTEND Gram CCast(_,b,t) -> (false,DefExpr(id,b,Some t)) | _ -> (false,DefExpr(id,b,None)) ] ] ; + assum_list: + [ [ bl = LIST1 assum_coe -> bl | b = simple_assum_coe -> [b] ] ] + ; assum_coe: - [ [ "("; idl = LIST1 base_ident; oc = of_type_with_opt_coercion; - c = lconstr; ")" -> (oc,(idl,c)) ] ] + [ [ "("; a = simple_assum_coe; ")" -> a ] ] + ; + simple_assum_coe: + [ [ idl = LIST1 base_ident; oc = of_type_with_opt_coercion; c = lconstr -> + (oc,(idl,c)) ] ] ; simple_binder_coe: [ [ id=base_ident -> (false,(id,CHole loc)) @@ -283,8 +291,11 @@ GEXTEND Gram (oc,(id,t)) ] ] ; constructor: - [ [ id = base_ident; coe = of_type_with_opt_coercion; c = lconstr -> - (coe,(id,c)) ] ] + [ [ id = base_ident; l = LIST0 binder_let; + coe = of_type_with_opt_coercion; c = lconstr -> + (coe,(id,G_constrnew.mkCProdN loc l c)) + | id = base_ident; l = LIST0 binder_let -> + (false,(id,G_constrnew.mkCProdN loc l (CHole loc))) ] ] ; of_type_with_opt_coercion: [ [ ":>" -> true |