diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-07 15:08:27 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-08 13:05:14 +0200 |
| commit | 33d153a01f2814c6e5486c07257667254b91fa0c (patch) | |
| tree | cc335368f42b3a879522cbf4888f842a138a6f18 /stm/texmacspp.ml | |
| 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/texmacspp.ml')
| -rw-r--r-- | stm/texmacspp.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml index fb41bb7be..b91208041 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 |