diff options
| author | letouzey | 2007-06-26 14:53:08 +0000 |
|---|---|---|
| committer | letouzey | 2007-06-26 14:53:08 +0000 |
| commit | e1438154fb28c8071ff4d26459996b9dc0a8bed0 (patch) | |
| tree | 9163001986f3c6d79fbabd2cd50a67517f21eba8 /parsing/printer.ml | |
| parent | 6288d74ca83dd5f93758da01f7028b8d9954c391 (diff) | |
killing some more non-exhaustive patterns
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9912 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/printer.ml')
| -rw-r--r-- | parsing/printer.ml | 17 |
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 |