diff options
| -rw-r--r-- | contrib/interface/xlate.ml | 2 | ||||
| -rw-r--r-- | parsing/printer.ml | 17 | ||||
| -rw-r--r-- | tactics/extraargs.ml4 | 1 |
3 files changed, 13 insertions, 7 deletions
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index c16b5215a..fe1c55003 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -1823,6 +1823,8 @@ let rec xlate_vernac = CT_print_path (xlate_class id1, xlate_class id2) | PrintCanonicalConversions -> xlate_error "TODO: Print Canonical Structures" + | PrintNeededAssumptions _ -> + xlate_error "TODO: Print Needed Assumptions" | PrintInspect n -> CT_inspect (CT_int n) | PrintUniverses opt_s -> CT_print_universes(ctf_STRING_OPT opt_s) | PrintSetoids -> CT_print_setoids diff --git a/parsing/printer.ml b/parsing/printer.ml index 97c1f6b7b..4619e50ec 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 diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4 index c3377bca1..4a6c2ffb2 100644 --- a/tactics/extraargs.ml4 +++ b/tactics/extraargs.ml4 @@ -279,6 +279,7 @@ let pr_r_int31_field _ _ _ i31f = | Retroknowledge.Int31PhiInv -> str "phi inv" | Retroknowledge.Int31Plus -> str "plus" | Retroknowledge.Int31Times -> str "times" + | _ -> assert false let pr_retroknowledge_field _ _ _ f = match f with |