diff options
| author | Pierre-Marie Pédrot | 2015-10-07 15:08:27 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-10-08 13:05:14 +0200 |
| commit | 33d153a01f2814c6e5486c07257667254b91fa0c (patch) | |
| tree | cc335368f42b3a879522cbf4888f842a138a6f18 /stm | |
| parent | 479d45e679e8486c65b77f2ddfa8718c24778a75 (diff) | |
Axioms now support the universe binding syntax.
We artificially restrict the syntax though, because it is unclear of
what the semantics of several axioms in a row is, in particular about the
resolution of remaining evars.
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/texmacspp.ml | 5 | ||||
| -rw-r--r-- | stm/vernac_classifier.ml | 2 |
2 files changed, 4 insertions, 3 deletions
diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml index fb41bb7bea..b912080413 100644 --- a/stm/texmacspp.ml +++ b/stm/texmacspp.ml @@ -575,10 +575,11 @@ let rec tmpp v loc = end | VernacExactProof _ as x -> xmlTODO loc x | VernacAssumption ((l, a), _, sbwcl) -> + let binders = List.map (fun (_, (id, c)) -> (List.map fst id, c)) sbwcl in let many = - List.length (List.flatten (List.map fst (List.map snd sbwcl))) > 1 in + List.length (List.flatten (List.map fst binders)) > 1 in let exprs = - List.flatten (List.map pp_simple_binder (List.map snd sbwcl)) in + List.flatten (List.map pp_simple_binder binders) in 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 diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 8aa2a59177..a898c687be 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -141,7 +141,7 @@ let rec classify_vernac e = else VtSideff ids, VtLater (* Sideff: apply to all open branches. usually run on master only *) | VernacAssumption (_,_,l) -> - let ids = List.flatten (List.map (fun (_,(l,_)) -> List.map snd l) l) in + let ids = List.flatten (List.map (fun (_,(l,_)) -> List.map (fun (id, _) -> snd id) l) l) in VtSideff ids, VtLater | VernacDefinition (_,((_,id),_),DefineBody _) -> VtSideff [id], VtLater | VernacInductive (_,_,l) -> |