diff options
| author | Yves Bertot | 2013-03-02 14:00:46 -0500 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-05-06 09:58:57 +0200 |
| commit | 8a905458039b631165d068bbf62f88e11eb36eb1 (patch) | |
| tree | f4f96ea7b7d482fc79acb6edb3b1c96aec2555a5 /parsing | |
| parent | 29794b8acf407518716f8c02c2ed20729f8802e5 (diff) | |
Adapt Y. Bertot's path on private inductives (now the keyword is "Private").
A quick and dirty approach to private inductive types
Types for which computable functions are provided, but pattern-matching is disallowed.
This kind of type can be used to simulate simple forms of higher inductive types, with
convertibility for applications of the inductive principle to 0-constructors
Conflicts:
intf/vernacexpr.mli
kernel/declarations.ml
kernel/declarations.mli
kernel/entries.mli
kernel/indtypes.ml
library/declare.ml
parsing/g_vernac.ml4
plugins/funind/glob_term_to_relation.ml
pretyping/indrec.ml
pretyping/tacred.mli
printing/ppvernac.ml
toplevel/vernacentries.ml
Conflicts:
kernel/declarations.mli
kernel/declareops.ml
kernel/indtypes.ml
kernel/modops.ml
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 df3c18d10d..05e6549255 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -190,11 +190,11 @@ GEXTEND Gram | IDENT "Let"; id = identref; b = def_body -> VernacDefinition ((Some Discharge, Definition), id, b) (* Gallina inductive declarations *) - | f = finite_token; + | priv = private_token; f = finite_token; indl = LIST1 inductive_definition SEP "with" -> let (k,f) = f in let indl=List.map (fun ((a,b,c,d),e) -> ((a,b,c,k,d),e)) indl in - VernacInductive (f,false,indl) + VernacInductive (priv,f,false,indl) | "Fixpoint"; recs = LIST1 rec_definition SEP "with" -> VernacFixpoint (None, recs) | IDENT "Let"; "Fixpoint"; recs = LIST1 rec_definition SEP "with" -> @@ -212,13 +212,14 @@ GEXTEND Gram ; gallina_ext: - [ [ b = record_token; infer = infer_token; oc = opt_coercion; name = identref; + [ [ priv = private_token; + b = record_token; infer = infer_token; oc = opt_coercion; name = identref; ps = binders; s = OPT [ ":"; s = lconstr -> s ]; cfs = [ ":="; l = constructor_list_or_record_decl -> l | -> RecordDecl (None, []) ] -> let (recf,indf) = b in - VernacInductive (indf,infer,[((oc,name),ps,s,recf,cfs),[]]) + VernacInductive (priv,indf,infer,[((oc,name),ps,s,recf,cfs),[]]) ] ] ; thm_token: @@ -260,6 +261,9 @@ GEXTEND Gram infer_token: [ [ IDENT "Infer" -> true | -> false ] ] ; + private_token: + [ [ IDENT "Private" -> true | -> false ] ] + ; record_token: [ [ IDENT "Record" -> (Record,BiFinite) | IDENT "Structure" -> (Structure,BiFinite) |