diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-03-11 21:35:19 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-03-11 21:35:19 +0000 |
| commit | 7c281301637f783beaec858a5fee665e99a6813b (patch) | |
| tree | be517bc917ed6dba36024659335763850918e5d5 /parsing | |
| parent | 14d27313ae3bdec2a61ce04cee9129b6e6775252 (diff) | |
Allowing (Co)Fixpoint to be defined local and Let-style.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16266 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index e6f7480b6..c3d9438de 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -161,6 +161,8 @@ GEXTEND Gram VernacAssumption (stre, nl, bl) | d = def_token; id = identref; b = def_body -> VernacDefinition (d, id, b) + | IDENT "Let"; id = identref; b = def_body -> + VernacDefinition ((Discharge, Definition), id, b) (* Gallina inductive declarations *) | f = finite_token; indl = LIST1 inductive_definition SEP "with" -> @@ -168,9 +170,13 @@ GEXTEND Gram let indl=List.map (fun ((a,b,c,d),e) -> ((a,b,c,k,d),e)) indl in VernacInductive (f,false,indl) | "Fixpoint"; recs = LIST1 rec_definition SEP "with" -> - VernacFixpoint recs + VernacFixpoint (use_locality_exp (), recs) + | IDENT "Let"; "Fixpoint"; recs = LIST1 rec_definition SEP "with" -> + VernacFixpoint (Discharge, recs) | "CoFixpoint"; corecs = LIST1 corec_definition SEP "with" -> - VernacCoFixpoint corecs + VernacCoFixpoint (use_locality_exp (), corecs) + | IDENT "Let"; "CoFixpoint"; corecs = LIST1 corec_definition SEP "with" -> + VernacCoFixpoint (Discharge, corecs) | IDENT "Scheme"; l = LIST1 scheme SEP "with" -> VernacScheme l | IDENT "Combined"; IDENT "Scheme"; id = identref; IDENT "from"; l = LIST1 identref SEP "," -> VernacCombinedScheme (id, l) ] ] @@ -197,8 +203,6 @@ GEXTEND Gram def_token: [ [ "Definition" -> (use_locality_exp (), Definition) - | IDENT "Let" -> - (Discharge, Definition) | IDENT "Example" -> (use_locality_exp (), Example) | IDENT "SubClass" -> |