diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-04-17 15:01:24 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-04-17 15:01:24 +0000 |
| commit | 5b318ca418ef27d1bf2b155bebbf2425f65b4f1f (patch) | |
| tree | b04fb45d1fd3e8fb6b4253a2acbd595754ec7dc6 /parsing/g_vernac.ml4 | |
| parent | 95f8a0ac38cbd792a0b5d8006aac1ef1a9f70da8 (diff) | |
Ajout "at next level" dans Notation
Mise en place structure pour définir un objet en même temps que sa notation
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3939 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/g_vernac.ml4')
| -rw-r--r-- | parsing/g_vernac.ml4 | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 2d1fcdd30..5b88cee39 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -216,8 +216,9 @@ GEXTEND Gram (id,c,lc) ] ] ; oneind: - [ [ id = base_ident; indpar = simple_binders_list; ":"; c = constr; ":="; - lc = constructor_list -> (id,indpar,c,lc) ] ] + [ [ ntn = OPT [ ntn = STRING; ":=" -> (ntn,None) ]; + id = base_ident; indpar = simple_binders_list; ":"; c = constr; ":="; + lc = constructor_list -> (id,ntn,indpar,c,lc) ] ] ; simple_binders_list: [ [ bl = ne_simple_binders_list -> bl @@ -298,7 +299,7 @@ GEXTEND Gram gallina_ext: [ [ IDENT "Mutual"; bl = ne_simple_binders_list ; f = finite_token; indl = block_old_style -> - let indl' = List.map (fun (id,ar,c) -> (id,bl,ar,c)) indl in + let indl' = List.map (fun (id,ar,c) -> (id,None,bl,ar,c)) indl in VernacInductive (f,indl') | record_token; oc = opt_coercion; name = base_ident; ps = simple_binders_list; ":"; @@ -316,7 +317,7 @@ GEXTEND Gram | IDENT "Scheme"; l = schemes -> VernacScheme l | f = finite_token; s = csort; id = base_ident; indpar = simple_binders_list; ":="; lc = constructor_list -> - VernacInductive (f,[id,indpar,s,lc]) ] ] + VernacInductive (f,[id,None,indpar,s,lc]) ] ] ; csort: [ [ s = sort -> CSort (loc,s) ] ] |