diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-06 14:17:55 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-06 14:17:55 +0000 |
| commit | cb8db3f7af710970a4ddba2fc559910ff7feaffb (patch) | |
| tree | e8f7756f762a7d8abedf4e49e54caa47bf7f985a /parsing | |
| parent | d36b4c46cc1cadf73808f4f9e7ef3d1e320c72aa (diff) | |
Mise en place possibilité de définitions locales dans les paramètres des inductifs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4316 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 9 | ||||
| -rw-r--r-- | parsing/g_vernacnew.ml4 | 2 |
2 files changed, 10 insertions, 1 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index d038e7d8c..21906628c 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -222,6 +222,9 @@ GEXTEND Gram oneind: [ [ id = base_ident; indpar = simple_binders_list; ":"; c = constr; ntn = OPT decl_notation ; ":="; lc = constructor_list -> + let indpar = + List.map (fun (id,t) -> LocalRawAssum ([dummy_loc,Name id],t)) + indpar in (id,ntn,indpar,c,lc) ] ] ; simple_binders_list: @@ -303,6 +306,9 @@ GEXTEND Gram gallina_ext: [ [ IDENT "Mutual"; bl = ne_simple_binders_list ; f = finite_token; indl = block_old_style -> + let bl = + List.map (fun (id,t) -> LocalRawAssum ([dummy_loc,Name id],t)) bl + in let indl' = List.map (fun (id,ar,c) -> (id,None,bl,ar,c)) indl in VernacInductive (f,indl') | b = record_token; oc = opt_coercion; name = base_ident; @@ -321,6 +327,9 @@ GEXTEND Gram | IDENT "Scheme"; l = schemes -> VernacScheme l | f = finite_token; s = csort; id = base_ident; indpar = simple_binders_list; ":="; lc = constructor_list -> + let indpar = + List.map (fun (id,t) -> LocalRawAssum ([dummy_loc,Name id],t)) + indpar in VernacInductive (f,[id,None,indpar,s,lc]) ] ] ; csort: diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4 index 6b11d5c98..31daf4afd 100644 --- a/parsing/g_vernacnew.ml4 +++ b/parsing/g_vernacnew.ml4 @@ -184,7 +184,7 @@ GEXTEND Gram ; (* Inductives and records *) inductive_definition: - [ [ id = base_ident; indpar = LIST0 simple_binder; ":"; c = lconstr; + [ [ id = base_ident; indpar = LIST0 binder_let; ":"; c = lconstr; ntn = decl_notation; ":="; lc = constructor_list -> (id,ntn,indpar,c,lc) ] ] ; |