diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2015-06-23 17:45:04 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2015-06-24 17:55:47 +0200 |
| commit | 2adff76c5466734c633923e768c9dcbdc6f28c86 (patch) | |
| tree | aca997d04a076e09ce62929415cd66820a5c92d3 /stm | |
| parent | 4a73e6b2bfb75451bcda7c74cf7478726a459799 (diff) | |
Add corresponding field in `VernacInductive`.
Makes sure not to generate inductive schemes of assumed positive types.
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/texmacspp.ml | 2 | ||||
| -rw-r--r-- | stm/vernac_classifier.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml index 9edc1f1c7..4cc362dda 100644 --- a/stm/texmacspp.ml +++ b/stm/texmacspp.ml @@ -580,7 +580,7 @@ let rec tmpp v loc = let l = match l with Some x -> x | None -> Decl_kinds.Global in let kind = string_of_assumption_kind l a many in xmlAssumption kind loc exprs - | VernacInductive (_, _, iednll) -> + | VernacInductive (_,_, _, iednll) -> let kind = let (_, _, _, k, _),_ = List.hd iednll in begin diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 2b5eb8683..03ade646b 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -144,7 +144,7 @@ let rec classify_vernac e = let ids = List.flatten (List.map (fun (_,(l,_)) -> List.map snd l) l) in VtSideff ids, VtLater | VernacDefinition (_,(_,id),DefineBody _) -> VtSideff [id], VtLater - | VernacInductive (_,_,l) -> + | VernacInductive (_,_,_,l) -> let ids = List.map (fun (((_,(_,id)),_,_,_,cl),_) -> id :: match cl with | Constructors l -> List.map (fun (_,((_,id),_)) -> id) l | RecordDecl (oid,l) -> (match oid with Some (_,x) -> [x] | _ -> []) @ |