aboutsummaryrefslogtreecommitdiff
path: root/parsing
diff options
context:
space:
mode:
Diffstat (limited to 'parsing')
-rw-r--r--parsing/printer.ml17
1 files changed, 10 insertions, 7 deletions
diff --git a/parsing/printer.ml b/parsing/printer.ml
index 97c1f6b7bf..4619e50ec7 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -485,17 +485,20 @@ let pr_assumptionset env s =
(if not (Environ.AssumptionSet.is_empty vars) then
str "Section Variables:" ++ fnl () ++
(Environ.AssumptionSet.fold
- (function Variable (id,typ ) -> fun s ->
- s++str (string_of_identifier id)++str " : "++pr_ltype typ++spc ())
- vars (fnl ()))
- else
- mt ()
+ (function Variable (id,typ ) ->
+ (fun s -> s++str (string_of_identifier id)++str " : "++pr_ltype typ++spc ())
+ | _ -> assert false)
+ vars (fnl ()))
+ else
+ mt ()
)++
if not (Environ.AssumptionSet.is_empty axioms) then
str "Axioms:" ++ fnl () ++
(Environ.AssumptionSet.fold
- (function Axiom (cst, typ) -> fun s -> s++(pr_constant env cst)++str " : "++pr_ltype typ++spc ())
- axioms (mt ()))
+ (function Axiom (cst, typ) ->
+ (fun s -> s++(pr_constant env cst)++str " : "++pr_ltype typ++spc ())
+ | _ -> assert false)
+ axioms (mt ()))
else
mt ()
else