diff options
| author |  pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-03-02 22:30:29 +0000 |
|---|---|---|
| committer | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-03-02 22:30:29 +0000 |
| commit | 401f17afa2e9cc3f2d734aef0d71a2c363838ebd (patch) | |
| tree | 7a3e0ce211585d4c09a182aad1358dfae0fb38ef | |
| parent | 15cb1aace0460e614e8af1269d874dfc296687b0 (diff) | |
Noise for nothing
Util only depends on Ocaml stdlib and Utf8 tables.
Generic pretty printing and loc functions are in Pp.
Generic errors are in Errors.
+ Training white-spaces, useless open, prlist copies random erasure.
Too many "open Errors" on the contrary.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15020 85f007b7-540e-0410-9357-904b9bb8a0f7
359 files changed, 989 insertions, 705 deletions
diff --git a/Makefile.common b/Makefile.common index d4492736a..88f035ac4 100644 --- a/Makefile.common +++ b/Makefile.common @@ -238,11 +238,11 @@ IDEMOD:=$(shell cat ide/ide.mllib) # coqmktop, coqc COQENVCMO:=$(CONFIG) \ - lib/pp_control.cmo lib/pp.cmo lib/compat.cmo lib/flags.cmo \ - lib/segmenttree.cmo lib/unicodetable.cmo lib/util.cmo lib/errors.cmo lib/system.cmo \ + lib/pp_control.cmo lib/compat.cmo lib/flags.cmo lib/pp.cmo \ + lib/segmenttree.cmo lib/unicodetable.cmo lib/errors.cmo lib/util.cmo lib/system.cmo \ lib/envars.cmo -COQMKTOPCMO:=$(COQENVCMO) scripts/tolink.cmo scripts/coqmktop.cmo +COQMKTOPCMO:=$(COQENVCMO) scripts/tolink.cmo scripts/coqmktop.cmo COQCCMO:=$(COQENVCMO) toplevel/usage.cmo scripts/coqc.cmo diff --git a/checker/check.ml b/checker/check.ml index bb42b949d..6f01107f5 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -7,6 +7,7 @@ (************************************************************************) open Pp +open Errors open Util open Names diff --git a/checker/check.mllib b/checker/check.mllib index 08dd78bcb..99b952a38 100644 --- a/checker/check.mllib +++ b/checker/check.mllib @@ -1,10 +1,11 @@ Coq_config Pp_control -Pp Compat Flags +Pp Segmenttree Unicodetable +Errors Util Option Hashcons diff --git a/checker/check_stat.ml b/checker/check_stat.ml index 5f28269ee..cdb0ade74 100644 --- a/checker/check_stat.ml +++ b/checker/check_stat.ml @@ -7,6 +7,7 @@ (************************************************************************) open Pp +open Errors open Util open System open Flags diff --git a/checker/checker.ml b/checker/checker.ml index 34ba7b010..4da4d14e1 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -8,6 +8,7 @@ open Compat open Pp +open Errors open Util open System open Flags diff --git a/checker/closure.ml b/checker/closure.ml index 033e2bd73..069b82017 100644 --- a/checker/closure.ml +++ b/checker/closure.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Pp open Term diff --git a/checker/declarations.ml b/checker/declarations.ml index 890996d10..ba56c243f 100644 --- a/checker/declarations.ml +++ b/checker/declarations.ml @@ -1,3 +1,4 @@ +open Errors open Util open Names open Term diff --git a/checker/declarations.mli b/checker/declarations.mli index 90beb326b..56a77571e 100644 --- a/checker/declarations.mli +++ b/checker/declarations.mli @@ -1,3 +1,4 @@ +open Errors open Util open Names open Term diff --git a/checker/environ.ml b/checker/environ.ml index 99b364579..d0b0b4ce9 100644 --- a/checker/environ.ml +++ b/checker/environ.ml @@ -1,3 +1,4 @@ +open Errors open Util open Names open Univ diff --git a/checker/indtypes.ml b/checker/indtypes.ml index 1e773df65..e48fdb6ef 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Names open Univ diff --git a/checker/inductive.ml b/checker/inductive.ml index 7a04cbfa3..67f61f161 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Names open Univ diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 9942816d1..cc9ca9031 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -1,5 +1,6 @@ open Pp +open Errors open Util open Names open Term diff --git a/checker/modops.ml b/checker/modops.ml index 2dc5d062c..4212a9361 100644 --- a/checker/modops.ml +++ b/checker/modops.ml @@ -7,6 +7,7 @@ (************************************************************************) (*i*) +open Errors open Util open Pp open Names diff --git a/checker/modops.mli b/checker/modops.mli index 5ed7b0ce2..5ac2fde50 100644 --- a/checker/modops.mli +++ b/checker/modops.mli @@ -7,6 +7,7 @@ (************************************************************************) (*i*) +open Errors open Util open Names open Univ diff --git a/checker/reduction.ml b/checker/reduction.ml index 3aeaa1023..c1eadcd64 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Names open Term diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml index bc067dc5f..57a9011cf 100644 --- a/checker/safe_typing.ml +++ b/checker/safe_typing.ml @@ -7,6 +7,7 @@ (************************************************************************) open Pp +open Errors open Util open Names open Declarations diff --git a/checker/subtyping.ml b/checker/subtyping.ml index 0c97254b5..8fb4eb34b 100644 --- a/checker/subtyping.ml +++ b/checker/subtyping.ml @@ -7,6 +7,7 @@ (************************************************************************) (*i*) +open Errors open Util open Names open Univ @@ -261,7 +262,7 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 = let c2 = force_constr lc2 in check_conv conv env c1 c2)) | IndType ((kn,i),mind1) -> - ignore (Util.error ( + ignore (Errors.error ( "The kernel does not recognize yet that a parameter can be " ^ "instantiated by an inductive type. Hint: you can rename the " ^ "inductive type and give a definition to map the old name to the new " ^ @@ -272,7 +273,7 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 = let typ2 = Typeops.type_of_constant_type env cb2.const_type in check_conv conv_leq env arity1 typ2 | IndConstr (((kn,i),j) as cstr,mind1) -> - ignore (Util.error ( + ignore (Errors.error ( "The kernel does not recognize yet that a parameter can be " ^ "instantiated by a constructor. Hint: you can rename the " ^ "constructor and give a definition to map the old name to the new " ^ diff --git a/checker/term.ml b/checker/term.ml index ab40b6fa7..db4b6599b 100644 --- a/checker/term.ml +++ b/checker/term.ml @@ -8,6 +8,7 @@ (* This module instantiates the structure of generic deBruijn terms to Coq *) +open Errors open Util open Pp open Names diff --git a/checker/typeops.ml b/checker/typeops.ml index 5226db534..b904e0b68 100644 --- a/checker/typeops.ml +++ b/checker/typeops.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Names open Univ diff --git a/dev/printers.mllib b/dev/printers.mllib index 40a5a8225..91d8b43a3 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -1,13 +1,13 @@ Coq_config Pp_control -Pp Compat Flags +Pp Segmenttree Unicodetable -Util Errors +Util Bigint Hashcons Dyn diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 3116cbf22..c765f3848 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -9,6 +9,7 @@ (* Printers for the ocaml toplevel. *) open System +open Errors open Util open Pp open Names @@ -131,7 +132,7 @@ let pppftreestate p = pp(print_pftreestate p) (* let pr_glls glls = *) (* hov 0 (pr_evar_defs (sig_sig glls) ++ fnl () ++ *) -(* prlist_with_sep pr_fnl db_pr_goal (sig_it glls)) *) +(* prlist_with_sep fnl db_pr_goal (sig_it glls)) *) (* let ppsigmagoal g = pp(pr_goal (sig_it g)) *) (* let prgls gls = pp(pr_gls gls) *) diff --git a/interp/constrextern.ml b/interp/constrextern.ml index f7bd32815..1ffa2c486 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -8,6 +8,7 @@ (*i*) open Pp +open Errors open Util open Univ open Names diff --git a/interp/constrextern.mli b/interp/constrextern.mli index 2a53eb85f..c112506ab 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Util +open Pp open Names open Term open Termops diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 04e252ca3..c94ac67de 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -7,6 +7,7 @@ (************************************************************************) open Pp +open Errors open Util open Flags open Names diff --git a/interp/coqlib.ml b/interp/coqlib.ml index eb7828eaa..9eda0b96a 100644 --- a/interp/coqlib.ml +++ b/interp/coqlib.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Pp open Names diff --git a/interp/coqlib.mli b/interp/coqlib.mli index 5d3580f26..27137e81b 100644 --- a/interp/coqlib.mli +++ b/interp/coqlib.mli @@ -11,6 +11,7 @@ open Libnames open Nametab open Term open Pattern +open Errors open Util (** This module collects the global references, constructions and diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index 07e813e74..5ea9cb986 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -124,7 +124,7 @@ let remove_sections dir = dir let interval loc = - let loc1,loc2 = Util.unloc loc in + let loc1,loc2 = Pp.unloc loc in loc1, loc2-1 let dump_ref loc filepath modpath ident ty = @@ -143,7 +143,7 @@ let add_glob_gen loc sp lib_dp ty = dump_ref loc filepath modpath ident ty let add_glob loc ref = - if dump () && loc <> Util.dummy_loc then + if dump () && loc <> Pp.dummy_loc then let sp = Nametab.path_of_global ref in let lib_dp = Lib.library_part ref in let ty = type_of_global_ref ref in @@ -154,7 +154,7 @@ let mp_of_kn kn = Names.MPdot (mp,l) let add_glob_kn loc kn = - if dump () && loc <> Util.dummy_loc then + if dump () && loc <> Pp.dummy_loc then let sp = Nametab.path_of_syndef kn in let lib_dp = Lib.dp_of_mp (mp_of_kn kn) in add_glob_gen loc sp lib_dp "syndef" @@ -237,7 +237,7 @@ let cook_notation df sc = let dump_notation (loc,(df,_)) sc sec = (* We dump the location of the opening '"' *) - dump_string (Printf.sprintf "not %d %s %s\n" (fst (Util.unloc loc)) + dump_string (Printf.sprintf "not %d %s %s\n" (fst (Pp.unloc loc)) (Names.string_of_dirpath (Lib.current_dirpath sec)) (cook_notation df sc)) let dump_notation_location posl df (((path,secpath),_),sc) = diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli index b02cc9669..90b56e0a9 100644 --- a/interp/dumpglob.mli +++ b/interp/dumpglob.mli @@ -26,17 +26,17 @@ type coqdoc_state = Lexer.location_table val coqdoc_freeze : unit -> coqdoc_state val coqdoc_unfreeze : coqdoc_state -> unit -val add_glob : Util.loc -> Libnames.global_reference -> unit -val add_glob_kn : Util.loc -> Names.kernel_name -> unit - -val dump_definition : Util.loc * Names.identifier -> bool -> string -> unit -val dump_moddef : Util.loc -> Names.module_path -> string -> unit -val dump_modref : Util.loc -> Names.module_path -> string -> unit -val dump_reference : Util.loc -> string -> string -> string -> unit -val dump_libref : Util.loc -> Names.dir_path -> string -> unit +val add_glob : Pp.loc -> Libnames.global_reference -> unit +val add_glob_kn : Pp.loc -> Names.kernel_name -> unit + +val dump_definition : Pp.loc * Names.identifier -> bool -> string -> unit +val dump_moddef : Pp.loc -> Names.module_path -> string -> unit +val dump_modref : Pp.loc -> Names.module_path -> string -> unit +val dump_reference : Pp.loc -> string -> string -> string -> unit +val dump_libref : Pp.loc -> Names.dir_path -> string -> unit val dump_notation_location : (int * int) list -> Topconstr.notation -> (Notation.notation_location * Topconstr.scope_name option) -> unit -val dump_binding : Util.loc -> Names.Idset.elt -> unit -val dump_notation : Util.loc * (Topconstr.notation * Notation.notation_location) -> Topconstr.scope_name option -> bool -> unit +val dump_binding : Pp.loc -> Names.Idset.elt -> unit +val dump_notation : Pp.loc * (Topconstr.notation * Notation.notation_location) -> Topconstr.scope_name option -> bool -> unit val dump_constraint : Topconstr.typeclass_constraint -> bool -> string -> unit val dump_string : string -> unit diff --git a/interp/genarg.ml b/interp/genarg.ml index e564bd11e..b4f87d96b 100644 --- a/interp/genarg.ml +++ b/interp/genarg.ml @@ -7,6 +7,7 @@ (************************************************************************) open Pp +open Errors open Util open Names open Nameops diff --git a/interp/genarg.mli b/interp/genarg.mli index 54aadba18..9c47c691a 100644 --- a/interp/genarg.mli +++ b/interp/genarg.mli @@ -6,7 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Util +open Errors +open Pp open Names open Term open Libnames diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index f27390435..e92699f64 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -15,6 +15,7 @@ open Evd open Environ open Nametab open Mod_subst +open Errors open Util open Glob_term open Topconstr diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli index ce518a9cb..14a1c630c 100644 --- a/interp/implicit_quantifiers.mli +++ b/interp/implicit_quantifiers.mli @@ -16,7 +16,7 @@ open Nametab open Mod_subst open Glob_term open Topconstr -open Util +open Pp open Libnames open Typeclasses diff --git a/interp/modintern.ml b/interp/modintern.ml index a13560c0f..5dde644b5 100644 --- a/interp/modintern.ml +++ b/interp/modintern.ml @@ -7,6 +7,7 @@ (************************************************************************) open Pp +open Errors open Util open Names open Entries diff --git a/interp/modintern.mli b/interp/modintern.mli index 71a00c2fe..e808cd980 100644 --- a/interp/modintern.mli +++ b/interp/modintern.mli @@ -9,7 +9,7 @@ open Declarations open Environ open Entries -open Util +open Pp open Libnames open Names open Topconstr diff --git a/interp/notation.ml b/interp/notation.ml index 8f19ab851..96de08da3 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -7,6 +7,7 @@ (************************************************************************) (*i*) +open Errors open Util open Pp open Bigint diff --git a/interp/notation.mli b/interp/notation.mli index f92ef94ed..25ea59419 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Pp open Bigint diff --git a/interp/ppextend.ml b/interp/ppextend.ml index ebf94bd80..176c2a76b 100644 --- a/interp/ppextend.ml +++ b/interp/ppextend.ml @@ -8,6 +8,7 @@ (*i*) open Pp +open Errors open Util open Names (*i*) diff --git a/interp/reserve.ml b/interp/reserve.ml index a07f5c846..7f30c6bac 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -8,6 +8,7 @@ (* Reserved names *) +open Errors open Util open Pp open Names diff --git a/interp/reserve.mli b/interp/reserve.mli index 97b22d2b2..f3b9d43a5 100644 --- a/interp/reserve.mli +++ b/interp/reserve.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Util +open Pp open Names open Glob_term open Topconstr diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml index 4e472b7a5..043c255a4 100644 --- a/interp/smartlocate.ml +++ b/interp/smartlocate.ml @@ -13,6 +13,7 @@ (* *) open Pp +open Errors open Util open Names open Libnames diff --git a/interp/smartlocate.mli b/interp/smartlocate.mli index 474058cc9..0c7bc6157 100644 --- a/interp/smartlocate.mli +++ b/interp/smartlocate.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Util +open Pp open Names open Libnames open Genarg diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index 8863bbbd3..eb6f50131 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Pp open Names diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli index e4da52a33..9e15ab970 100644 --- a/interp/syntax_def.mli +++ b/interp/syntax_def.mli @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Names open Topconstr diff --git a/interp/topconstr.ml b/interp/topconstr.ml index b2e1a7545..ca1706035 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -8,6 +8,7 @@ (*i*) open Pp +open Errors open Util open Names open Nameops @@ -857,7 +858,7 @@ type cases_pattern_expr = | CPatOr of loc * cases_pattern_expr list | CPatNotation of loc * notation * cases_pattern_notation_substitution | CPatPrim of loc * prim_token - | CPatRecord of Util.loc * (reference * cases_pattern_expr) list + | CPatRecord of loc * (reference * cases_pattern_expr) list | CPatDelimiters of loc * string * cases_pattern_expr and cases_pattern_notation_substitution = @@ -1272,8 +1273,8 @@ type module_ast = (* and which are then occupied by proper symbols of the notation (or spaces) *) let locs_of_notation loc locs ntn = - let (bl,el) = Util.unloc loc in - let locs = List.map Util.unloc locs in + let (bl,el) = unloc loc in + let locs = List.map unloc locs in let rec aux pos = function | [] -> if pos = el then [] else [(pos,el-1)] | (ba,ea)::l ->if pos = ba then aux ea l else (pos,ba-1)::aux ea l diff --git a/interp/topconstr.mli b/interp/topconstr.mli index 5ee0c5bc6..ea3191770 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -7,7 +7,7 @@ (************************************************************************) open Pp -open Util +open Errors open Names open Libnames open Glob_term @@ -130,7 +130,7 @@ type cases_pattern_expr = | CPatOr of loc * cases_pattern_expr list | CPatNotation of loc * notation * cases_pattern_notation_substitution | CPatPrim of loc * prim_token - | CPatRecord of Util.loc * (reference * cases_pattern_expr) list + | CPatRecord of loc * (reference * cases_pattern_expr) list | CPatDelimiters of loc * string * cases_pattern_expr and cases_pattern_notation_substitution = @@ -267,6 +267,6 @@ type module_ast = | CMwith of loc * module_ast * with_declaration_ast val ntn_loc : - Util.loc -> constr_notation_substitution -> string -> (int * int) list + loc -> constr_notation_substitution -> string -> (int * int) list val patntn_loc : - Util.loc -> cases_pattern_notation_substitution -> string -> (int * int) list + loc -> cases_pattern_notation_substitution -> string -> (int * int) list diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 8da06f435..86c8f4913 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -10,6 +10,7 @@ machine, Oct 2004 *) (* Extension: Arnaud Spiwack (support for native arithmetic), May 2005 *) +open Errors open Util open Names open Cbytecodes diff --git a/kernel/closure.ml b/kernel/closure.ml index 143d6eb49..d62ac79bf 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -19,6 +19,7 @@ (* This file implements a lazy reduction for the Calculus of Inductive Constructions *) +open Errors open Util open Pp open Term diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml index 92109258d..c195a5496 100644 --- a/kernel/conv_oracle.ml +++ b/kernel/conv_oracle.ml @@ -44,7 +44,7 @@ let set_strategy k l = cst_opacity := if l=default then Cmap.remove c !cst_opacity else Cmap.add c l !cst_opacity - | RelKey _ -> Util.error "set_strategy: RelKey" + | RelKey _ -> Errors.error "set_strategy: RelKey" let get_transp_state () = (Idmap.fold diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 02330339d..1a405e98b 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -14,6 +14,7 @@ declarations over global constants and inductive types *) open Pp +open Errors open Util open Names open Term diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 1a84b9876..db304e33d 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -21,6 +21,7 @@ global constants/axioms, mutual inductive definitions and the module system *) +open Errors open Util open Names open Univ diff --git a/kernel/environ.ml b/kernel/environ.ml index 7a41e62c4..c38d4186f 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -20,6 +20,7 @@ (* This file defines the type of environments on which the type-checker works, together with simple related functions *) +open Errors open Util open Names open Sign diff --git a/kernel/esubst.ml b/kernel/esubst.ml index cbce04d62..dad5b1420 100644 --- a/kernel/esubst.ml +++ b/kernel/esubst.ml @@ -10,6 +10,7 @@ (* Support for explicit substitutions *) +open Errors open Util (*********************) diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 46e866a04..aa5e132c6 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Names open Univ diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 21f86233a..b2d924714 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Names open Univ diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index 314cc0ee0..777f39183 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -14,6 +14,7 @@ substitution in module constructions *) open Pp +open Errors open Util open Names open Term diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index a384c836c..e2304f119 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -12,6 +12,7 @@ (* This module provides the main functions for type-checking module declarations *) +open Errors open Util open Names open Univ diff --git a/kernel/modops.ml b/kernel/modops.ml index 0c2c6bd71..a422bae66 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -15,6 +15,7 @@ (* This file provides with various operations on modules and module types *) +open Errors open Util open Pp open Names diff --git a/kernel/modops.mli b/kernel/modops.mli index b9c36d5af..9f8a306fa 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Names open Univ diff --git a/kernel/names.ml b/kernel/names.ml index ae8ad093c..b01d5675b 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -19,12 +19,16 @@ Élie Soubiran, ... *) open Pp +open Errors open Util (** {6 Identifiers } *) type identifier = string +let check_ident_soft x = Option.iter Pp.warning (ident_refutation x) +let check_ident x = Option.iter Errors.error (ident_refutation x) + let id_of_string s = check_ident_soft s; String.copy s let string_of_id id = String.copy id diff --git a/kernel/names.mli b/kernel/names.mli index 34c5e62c5..63c64f364 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -10,6 +10,9 @@ type identifier +val check_ident : string -> unit +val check_ident_soft : string -> unit + (** Parsing and printing of identifiers *) val string_of_id : identifier -> string val id_of_string : string -> identifier diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml index 985aac95f..ec4a2d195 100644 --- a/kernel/pre_env.ml +++ b/kernel/pre_env.ml @@ -13,6 +13,7 @@ (* This file defines the type of kernel environments *) +open Errors open Util open Names open Sign diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli index 40ce887b2..0d279bc39 100644 --- a/kernel/pre_env.mli +++ b/kernel/pre_env.mli @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Names open Sign diff --git a/kernel/reduction.ml b/kernel/reduction.ml index fc5e32cf5..10eccd059 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -15,6 +15,7 @@ (* Equal inductive types by Jacek Chrzaszcz as part of the module system, Aug 2002 *) +open Errors open Util open Names open Term diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index c2d71ebb2..e87bc9c1c 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -57,6 +57,7 @@ etc. *) +open Errors open Util open Names open Univ diff --git a/kernel/sign.ml b/kernel/sign.ml index 71169563b..861cb0b6c 100644 --- a/kernel/sign.ml +++ b/kernel/sign.ml @@ -16,6 +16,7 @@ names-based contexts *) open Names +open Errors open Util open Term diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index c141a02aa..9fb045407 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -12,6 +12,7 @@ (* This module checks subtyping of module types *) (*i*) +open Errors open Util open Names open Univ @@ -278,7 +279,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = let c2 = Declarations.force lc2 in check_conv NotConvertibleBodyField cst conv env c1 c2)) | IndType ((kn,i),mind1) -> - ignore (Util.error ( + ignore (Errors.error ( "The kernel does not recognize yet that a parameter can be " ^ "instantiated by an inductive type. Hint: you can rename the " ^ "inductive type and give a definition to map the old name to the new " ^ @@ -289,7 +290,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = let typ2 = Typeops.type_of_constant_type env cb2.const_type in check_conv NotConvertibleTypeField cst conv_leq env arity1 typ2 | IndConstr (((kn,i),j) as cstr,mind1) -> - ignore (Util.error ( + ignore (Errors.error ( "The kernel does not recognize yet that a parameter can be " ^ "instantiated by a constructor. Hint: you can rename the " ^ "constructor and give a definition to map the old name to the new " ^ diff --git a/kernel/term.ml b/kernel/term.ml index dcb63cf7b..0a4782d8c 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -23,6 +23,7 @@ Inductive Constructions (CIC) terms together with constructors, destructors, iterators and basic functions *) +open Errors open Util open Pp open Names diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 478b9c6fc..887a90010 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -12,6 +12,7 @@ (* This module provides the main entry points for type-checking basic declarations *) +open Errors open Util open Names open Univ diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 49106c912..a2dd09976 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Names open Univ diff --git a/kernel/univ.ml b/kernel/univ.ml index 0193542a3..d967846f1 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -14,6 +14,7 @@ (* Revisions by Bruno Barras, Hugo Herbelin, Pierre Letouzey *) open Pp +open Errors open Util (* Universes are stratified by a partial ordering $\le$. @@ -817,9 +818,9 @@ let pr_arc = function | _, Canonical {univ=u; lt=lt; le=le} -> pr_uni_level u ++ str " " ++ v 0 - (prlist_with_sep pr_spc (fun v -> str "< " ++ pr_uni_level v) lt ++ + (pr_sequence (fun v -> str "< " ++ pr_uni_level v) lt ++ (if lt <> [] & le <> [] then spc () else mt()) ++ - prlist_with_sep pr_spc (fun v -> str "<= " ++ pr_uni_level v) le) ++ + pr_sequence (fun v -> str "<= " ++ pr_uni_level v) le) ++ fnl () | u, Equiv v -> pr_uni_level u ++ str " = " ++ pr_uni_level v ++ fnl () diff --git a/kernel/vm.ml b/kernel/vm.ml index 86aed5d93..851b66d48 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -224,7 +224,7 @@ let whd_val : values -> whd = | 1 -> Vfix(Obj.obj o, None) | 2 -> Vfix(Obj.obj (Obj.field o 1), Some (Obj.obj o)) | 3 -> Vatom_stk(Aid(RelKey(int_tcode (fun_code o) 1)), []) - | _ -> Util.anomaly "Vm.whd : kind_of_closure does not work") + | _ -> Errors.anomaly "Vm.whd : kind_of_closure does not work") else Vconstr_block(Obj.obj o) diff --git a/lib/dyn.ml b/lib/dyn.ml index a0109b60e..04f6d431f 100644 --- a/lib/dyn.ml +++ b/lib/dyn.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util (* Dynamics, programmed with DANGER !!! *) diff --git a/lib/envars.ml b/lib/envars.ml index e5c938037..611b81a7e 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -38,7 +38,7 @@ let guess_coqlib () = in if Sys.file_exists (Filename.concat coqlib file) then coqlib - else Util.error "cannot guess a path for Coq libraries; please use -coqlib option") + else Errors.error "cannot guess a path for Coq libraries; please use -coqlib option") let coqlib () = if !Flags.coqlib_spec then !Flags.coqlib else diff --git a/lib/errors.ml b/lib/errors.ml index 3b5e67704..1060a8efd 100644 --- a/lib/errors.ml +++ b/lib/errors.ml @@ -6,10 +6,35 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) +open Compat open Pp -(* spiwack: it might be reasonable to decide and move the declarations - of Anomaly and so on to this module so as not to depend on Util. *) +(* Errors *) + +exception Anomaly of string * std_ppcmds (* System errors *) +let anomaly string = raise (Anomaly(string, str string)) +let anomalylabstrm string pps = raise (Anomaly(string,pps)) + +exception UserError of string * std_ppcmds (* User errors *) +let error string = raise (UserError("_", str string)) +let errorlabstrm l pps = raise (UserError(l,pps)) + +exception AlreadyDeclared of std_ppcmds (* for already declared Schemes *) +let alreadydeclared pps = raise (AlreadyDeclared(pps)) + +let todo s = prerr_string ("TODO: "^s^"\n") + +(* raising located exceptions *) +let anomaly_loc (loc,s,strm) = Loc.raise loc (Anomaly (s,strm)) +let user_err_loc (loc,s,strm) = Loc.raise loc (UserError (s,strm)) +let invalid_arg_loc (loc,s) = Loc.raise loc (Invalid_argument s) + +(* Like Exc_located, but specifies the outermost file read, the filename + associated to the location of the error, and the error itself. *) + +exception Error_in_file of string * (bool * string * loc) * exn + +exception Timeout let handle_stack = ref [] @@ -38,7 +63,7 @@ let where s = if !Flags.debug then str ("in "^s^":") ++ spc () else mt () let raw_anomaly e = match e with - | Util.Anomaly (s,pps) -> where s ++ pps ++ str "." + | Anomaly (s,pps) -> where s ++ pps ++ str "." | Assert_failure _ | Match_failure _ -> str (Printexc.to_string e ^ ".") | _ -> str ("Uncaught exception " ^ Printexc.to_string e ^ ".") @@ -62,7 +87,7 @@ let print_no_anomaly e = print_gen (fun e -> raise e) !handle_stack e (** Predefined handlers **) let _ = register_handler begin function - | Util.UserError(s,pps) -> hov 0 (str "Error: " ++ where s ++ pps) + | UserError(s,pps) -> hov 0 (str "Error: " ++ where s ++ pps) | _ -> raise Unhandled end diff --git a/lib/errors.mli b/lib/errors.mli index eb7fde8e7..a863c5e30 100644 --- a/lib/errors.mli +++ b/lib/errors.mli @@ -6,9 +6,45 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) +open Pp + (** This modules implements basic manipulations of errors for use throughout Coq's code. *) +(** {6 Generic errors.} + + [Anomaly] is used for system errors and [UserError] for the + user's ones. *) + +exception Anomaly of string * std_ppcmds +val anomaly : string -> 'a +val anomalylabstrm : string -> std_ppcmds -> 'a +val anomaly_loc : loc * string * std_ppcmds -> 'a + +exception UserError of string * std_ppcmds +val error : string -> 'a +val errorlabstrm : string -> std_ppcmds -> 'a +val user_err_loc : loc * string * std_ppcmds -> 'a + +exception AlreadyDeclared of std_ppcmds +val alreadydeclared : std_ppcmds -> 'a + +val invalid_arg_loc : loc * string -> 'a + +(** [todo] is for running of an incomplete code its implementation is + "do nothing" (or print a message), but this function should not be + used in a released code *) + +val todo : string -> unit + +exception Timeout + +(** Like [Exc_located], but specifies the outermost file read, the + input buffer associated to the location of the error (or the module name + if boolean is true), and the error itself. *) + +exception Error_in_file of string * (bool * string * loc) * exn + (** [register_handler h] registers [h] as a handler. When an expression is printed with [print e], it goes through all registered handles (the most diff --git a/lib/gmapl.ml b/lib/gmapl.ml index a00407426..01a277c78 100644 --- a/lib/gmapl.ml +++ b/lib/gmapl.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util type ('a,'b) t = ('a,'b list) Gmap.t diff --git a/lib/lib.mllib b/lib/lib.mllib index db79b5c24..eb834af78 100644 --- a/lib/lib.mllib +++ b/lib/lib.mllib @@ -2,13 +2,13 @@ Xml_lexer Xml_parser Xml_utils Pp_control -Pp Compat Flags +Pp Segmenttree Unicodetable -Util Errors +Util Bigint Hashcons Dyn diff --git a/lib/option.ml b/lib/option.ml index c3fe9ce46..ef7a2e9e5 100644 --- a/lib/option.ml +++ b/lib/option.ml @@ -153,6 +153,13 @@ module List = let rec flatten = function | x::l -> cons x (flatten l) | [] -> [] + + let rec find f = function + |[] -> None + |h :: t -> match f h with + |None -> find f t + |x -> x + end diff --git a/lib/option.mli b/lib/option.mli index b9fd7d2f3..217aa6696 100644 --- a/lib/option.mli +++ b/lib/option.mli @@ -100,6 +100,8 @@ module List : sig (** [List.flatten l] is the list of all the [y]s such that [l] contains [Some y] (in the same order). *) val flatten : 'a option list -> 'a list + + val find : ('a -> 'b option) -> 'a list -> 'b option end diff --git a/lib/pp.ml4 b/lib/pp.ml4 index c602b403e..4fc53270c 100644 --- a/lib/pp.ml4 +++ b/lib/pp.ml4 @@ -7,12 +7,13 @@ (************************************************************************) open Pp_control +open Compat (* This should not be used outside of this file. Use Flags.print_emacs instead. This one is updated when reading command line options. This was the only way to make [Pp] depend on - an option without creating a circularity: [Flags. -> [Util] -> - [Pp] -> [Flags. *) + an option without creating a circularity: [Flags] -> [Util] -> + [Pp] -> [Flags] *) let print_emacs = ref false let make_pp_emacs() = print_emacs:=true let make_pp_nonemacs() = print_emacs:=false @@ -336,3 +337,104 @@ let msg_warning x = msg_warning_with !err_ft x let string_of_ppcmds c = msg_with Format.str_formatter c; Format.flush_str_formatter () + +(* Locations management *) +type loc = Loc.t +let dummy_loc = Loc.ghost +let join_loc = Loc.merge +let make_loc = make_loc +let unloc = unloc + +type 'a located = loc * 'a +let located_fold_left f x (_,a) = f x a +let located_iter2 f (_,a) (_,b) = f a b +let down_located f (_,a) = f a + + +(* Copy paste from Util *) + +let pr_comma () = str "," ++ spc () +let pr_semicolon () = str ";" ++ spc () +let pr_bar () = str "|" ++ spc () +let pr_arg pr x = spc () ++ pr x +let pr_opt pr = function None -> mt () | Some x -> pr_arg pr x +let pr_opt_no_spc pr = function None -> mt () | Some x -> pr x + +let pr_nth n = + int n ++ str (match n mod 10 with 1 -> "st" | 2 -> "nd" | 3 -> "rd" | _ -> "th") + +(* [prlist pr [a ; ... ; c]] outputs [pr a ++ ... ++ pr c] *) + +let rec prlist elem l = match l with + | [] -> mt () + | h::t -> Stream.lapp (fun () -> elem h) (prlist elem t) + +(* unlike all other functions below, [prlist] works lazily. + if a strict behavior is needed, use [prlist_strict] instead. + evaluation is done from left to right. *) + +let prlist_sep_lastsep no_empty sep lastsep elem = + let rec start = function + |[] -> mt () + |[e] -> elem e + |h::t -> let e = elem h in + if no_empty && e = mt () then start t else + let rec aux = function + |[] -> mt () + |h::t -> + let e = elem h and r = aux t in + if no_empty && e = mt () then r else + if r = mt () + then let s = lastsep () in s ++ e + else let s = sep () in s ++ e ++ r + in let r = aux t in e ++ r + in start + +let prlist_strict pr l = prlist_sep_lastsep true mt mt pr l +(* [prlist_with_sep sep pr [a ; ... ; c]] outputs + [pr a ++ sep() ++ ... ++ sep() ++ pr c] *) +let prlist_with_sep sep pr l = prlist_sep_lastsep false sep sep pr l +(* Print sequence of objects separated by space (unless an element is empty) *) +let pr_sequence pr l = prlist_sep_lastsep true spc spc pr l +(* [pr_enum pr [a ; b ; ... ; c]] outputs + [pr a ++ str "," ++ pr b ++ str "," ++ ... ++ str "and" ++ pr c] *) +let pr_enum pr l = prlist_sep_lastsep true pr_comma (fun () -> str " and" ++ spc ()) pr l + +let pr_vertical_list pr = function + | [] -> str "none" ++ fnl () + | l -> fnl () ++ str " " ++ hov 0 (prlist_with_sep fnl pr l) ++ fnl () + +(* [prvecti_with_sep sep pr [|a0 ; ... ; an|]] outputs + [pr 0 a0 ++ sep() ++ ... ++ sep() ++ pr n an] *) + +let prvecti_with_sep sep elem v = + let rec pr i = + if i = 0 then + elem 0 v.(0) + else + let r = pr (i-1) and s = sep () and e = elem i v.(i) in + r ++ s ++ e + in + let n = Array.length v in + if n = 0 then mt () else pr (n - 1) + +(* [prvecti pr [|a0 ; ... ; an|]] outputs [pr 0 a0 ++ ... ++ pr n an] *) + +let prvecti elem v = prvecti_with_sep mt elem v + +(* [prvect_with_sep sep pr [|a ; ... ; c|]] outputs + [pr a ++ sep() ++ ... ++ sep() ++ pr c] *) + +let prvect_with_sep sep elem v = prvecti_with_sep sep (fun _ -> elem) v + +(* [prvect pr [|a ; ... ; c|]] outputs [pr a ++ ... ++ pr c] *) + +let prvect elem v = prvect_with_sep mt elem v + +let pr_located pr (loc,x) = + if Flags.do_beautify() && loc<>dummy_loc then + let (b,e) = unloc loc in + comment b ++ pr x ++ comment e + else pr x + +let surround p = hov 1 (str"(" ++ p ++ str")") diff --git a/lib/pp.mli b/lib/pp.mli index 7070e3f5f..2fd62d55a 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -7,6 +7,7 @@ (************************************************************************) open Pp_control +open Compat (** Modify pretty printing functions behavior for emacs ouput (special chars inserted at some places). This function should called once in @@ -114,3 +115,45 @@ val msgerrnl : std_ppcmds -> unit val msg_warning : std_ppcmds -> unit val string_of_ppcmds : std_ppcmds -> string + +(** {6 Location management. } *) + +type loc = Loc.t +val unloc : loc -> int * int +val make_loc : int * int -> loc +val dummy_loc : loc +val join_loc : loc -> loc -> loc + +type 'a located = loc * 'a +val located_fold_left : ('a -> 'b -> 'a) -> 'a -> 'b located -> 'a +val located_iter2 : ('a -> 'b -> unit) -> 'a located -> 'b located -> unit +val down_located : ('a -> 'b) -> 'a located -> 'b + +(** {6 Util copy/paste. } *) + +val pr_comma : unit -> std_ppcmds +val pr_semicolon : unit -> std_ppcmds +val pr_bar : unit -> std_ppcmds +val pr_arg : ('a -> std_ppcmds) -> 'a -> std_ppcmds +val pr_opt : ('a -> std_ppcmds) -> 'a option -> std_ppcmds +val pr_opt_no_spc : ('a -> std_ppcmds) -> 'a option -> std_ppcmds +val pr_nth : int -> std_ppcmds + +val prlist : ('a -> std_ppcmds) -> 'a list -> std_ppcmds + +(** unlike all other functions below, [prlist] works lazily. + if a strict behavior is needed, use [prlist_strict] instead. *) +val prlist_strict : ('a -> std_ppcmds) -> 'a list -> std_ppcmds +val prlist_with_sep : + (unit -> std_ppcmds) -> ('b -> std_ppcmds) -> 'b list -> std_ppcmds +val prvect : ('a -> std_ppcmds) -> 'a array -> std_ppcmds +val prvecti : (int -> 'a -> std_ppcmds) -> 'a array -> std_ppcmds +val prvect_with_sep : + (unit -> std_ppcmds) -> ('a -> std_ppcmds) -> 'a array -> std_ppcmds +val prvecti_with_sep : + (unit -> std_ppcmds) -> (int -> 'a -> std_ppcmds) -> 'a array -> std_ppcmds +val pr_vertical_list : ('b -> std_ppcmds) -> 'b list -> std_ppcmds +val pr_enum : ('a -> std_ppcmds) -> 'a list -> std_ppcmds +val pr_located : ('a -> std_ppcmds) -> 'a located -> std_ppcmds +val pr_sequence : ('a -> std_ppcmds) -> 'a list -> std_ppcmds +val surround : std_ppcmds -> std_ppcmds diff --git a/lib/rtree.ml b/lib/rtree.ml index 22d3d72b4..4fccd282f 100644 --- a/lib/rtree.ml +++ b/lib/rtree.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util @@ -173,11 +174,11 @@ let rec pp_tree prl t = | Node(lab,[||]) -> hov 2 (str"("++prl lab++str")") | Node(lab,v) -> hov 2 (str"("++prl lab++str","++brk(1,0)++ - Util.prvect_with_sep Util.pr_comma (pp_tree prl) v++str")") + prvect_with_sep pr_comma (pp_tree prl) v++str")") | Rec(i,v) -> if Array.length v = 0 then str"Rec{}" else if Array.length v = 1 then hov 2 (str"Rec{"++pp_tree prl v.(0)++str"}") else hov 2 (str"Rec{"++int i++str","++brk(1,0)++ - Util.prvect_with_sep Util.pr_comma (pp_tree prl) v++str"}") + prvect_with_sep pr_comma (pp_tree prl) v++str"}") diff --git a/lib/system.ml b/lib/system.ml index 7d54e2c3a..7e0347530 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -9,6 +9,7 @@ (* $Id$ *) open Pp +open Errors open Util open Unix @@ -140,7 +141,7 @@ let exclude_search_in_dirname f = skipped_dirnames := f :: !skipped_dirnames let ok_dirname f = f <> "" && f.[0] <> '.' && not (List.mem f !skipped_dirnames) && - try ignore (check_ident f); true with _ -> false + match ident_refutation f with |None -> true |_ -> false let all_subdirs ~unix_path:root = let l = ref [] in diff --git a/lib/util.ml b/lib/util.ml index 287dd3719..879884283 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -6,47 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -open Pp -open Compat - -(* Errors *) - -exception Anomaly of string * std_ppcmds (* System errors *) -let anomaly string = raise (Anomaly(string, str string)) -let anomalylabstrm string pps = raise (Anomaly(string,pps)) - -exception UserError of string * std_ppcmds (* User errors *) -let error string = raise (UserError("_", str string)) -let errorlabstrm l pps = raise (UserError(l,pps)) - -exception AlreadyDeclared of std_ppcmds (* for already declared Schemes *) -let alreadydeclared pps = raise (AlreadyDeclared(pps)) - -let todo s = prerr_string ("TODO: "^s^"\n") - -exception Timeout - -type loc = Loc.t -let dummy_loc = Loc.ghost -let join_loc = Loc.merge -let make_loc = make_loc -let unloc = unloc - -(* raising located exceptions *) -type 'a located = loc * 'a -let anomaly_loc (loc,s,strm) = Loc.raise loc (Anomaly (s,strm)) -let user_err_loc (loc,s,strm) = Loc.raise loc (UserError (s,strm)) -let invalid_arg_loc (loc,s) = Loc.raise loc (Invalid_argument s) - -let located_fold_left f x (_,a) = f x a -let located_iter2 f (_,a) (_,b) = f a b -let down_located f (_,a) = f a - -(* Like Exc_located, but specifies the outermost file read, the filename - associated to the location of the error, and the error itself. *) - -exception Error_in_file of string * (bool * string * loc) * exn - (* Mapping under pairs *) let on_fst f (a,b) = (f a,b) @@ -319,40 +278,39 @@ let next_utf8 s i = (* Check the well-formedness of an identifier *) -let check_initial handle j n s = +let initial_refutation j n s = match classify_unicode n with - | UnicodeLetter -> () + | UnicodeLetter -> None | _ -> let c = String.sub s 0 j in - handle ("Invalid character '"^c^"' at beginning of identifier \""^s^"\".") + Some ("Invalid character '"^c^"' at beginning of identifier \""^s^"\".") -let check_trailing handle i j n s = +let trailing_refutation i j n s = match classify_unicode n with - | UnicodeLetter | UnicodeIdentPart -> () + | UnicodeLetter | UnicodeIdentPart -> None | _ -> let c = String.sub s i j in - handle ("Invalid character '"^c^"' in identifier \""^s^"\".") + Some ("Invalid character '"^c^"' in identifier \""^s^"\".") -let check_ident_gen handle s = - let i = ref 0 in - if s <> ".." then try +let ident_refutation s = + if s = ".." then None else try let j, n = next_utf8 s 0 in - check_initial handle j n s; - i := !i + j; - try - while true do - let j, n = next_utf8 s !i in - check_trailing handle !i j n s; - i := !i + j - done - with End_of_input -> () + match initial_refutation j n s with + |None -> + begin try + let rec aux i = + let j, n = next_utf8 s i in + match trailing_refutation i j n s with + |None -> aux (i + j) + |x -> x + in aux j + with End_of_input -> None + end + |x -> x with - | End_of_input -> error "The empty string is not an identifier." - | UnsupportedUtf8 -> error (s^": unsupported character in utf8 sequence.") - | Invalid_argument _ -> error (s^": invalid utf8 sequence.") - -let check_ident_soft = check_ident_gen warning -let check_ident = check_ident_gen error + | End_of_input -> Some "The empty string is not an identifier." + | UnsupportedUtf8 -> Some (s^": unsupported character in utf8 sequence.") + | Invalid_argument _ -> Some (s^": invalid utf8 sequence.") let lowercase_unicode = let tree = Segmenttree.make Unicodetable.to_lower in @@ -1288,102 +1246,6 @@ let map_succeed f = in map_f -(* Pretty-printing *) - -let pr_spc = spc -let pr_fnl = fnl -let pr_int = int -let pr_str = str -let pr_comma () = str "," ++ spc () -let pr_semicolon () = str ";" ++ spc () -let pr_bar () = str "|" ++ spc () -let pr_arg pr x = spc () ++ pr x -let pr_opt pr = function None -> mt () | Some x -> pr_arg pr x -let pr_opt_no_spc pr = function None -> mt () | Some x -> pr x - -let nth n = str (ordinal n) - -(* [prlist pr [a ; ... ; c]] outputs [pr a ++ ... ++ pr c] *) - -let rec prlist elem l = match l with - | [] -> mt () - | h::t -> Stream.lapp (fun () -> elem h) (prlist elem t) - -(* unlike all other functions below, [prlist] works lazily. - if a strict behavior is needed, use [prlist_strict] instead. - evaluation is done from left to right. *) - -let rec prlist_strict elem l = match l with - | [] -> mt () - | h::t -> - let e = elem h in let r = prlist_strict elem t in e++r - -(* [prlist_with_sep sep pr [a ; ... ; c]] outputs - [pr a ++ sep() ++ ... ++ sep() ++ pr c] *) - -let rec prlist_with_sep sep elem l = match l with - | [] -> mt () - | [h] -> elem h - | h::t -> - let e = elem h and s = sep() and r = prlist_with_sep sep elem t in - e ++ s ++ r - -(* Print sequence of objects separated by space (unless an element is empty) *) - -let rec pr_sequence elem = function - | [] -> mt () - | [h] -> elem h - | h::t -> - let e = elem h and r = pr_sequence elem t in - if e = mt () then r else e ++ spc () ++ r - -(* [pr_enum pr [a ; b ; ... ; c]] outputs - [pr a ++ str "," ++ pr b ++ str "," ++ ... ++ str "and" ++ pr c] *) - -let pr_enum pr l = - let c,l' = list_sep_last l in - prlist_with_sep pr_comma pr l' ++ - (if l'<>[] then str " and" ++ spc () else mt()) ++ pr c - -let pr_vertical_list pr = function - | [] -> str "none" ++ fnl () - | l -> fnl () ++ str " " ++ hov 0 (prlist_with_sep pr_fnl pr l) ++ fnl () - -(* [prvecti_with_sep sep pr [|a0 ; ... ; an|]] outputs - [pr 0 a0 ++ sep() ++ ... ++ sep() ++ pr n an] *) - -let prvecti_with_sep sep elem v = - let rec pr i = - if i = 0 then - elem 0 v.(0) - else - let r = pr (i-1) and s = sep () and e = elem i v.(i) in - r ++ s ++ e - in - let n = Array.length v in - if n = 0 then mt () else pr (n - 1) - -(* [prvecti pr [|a0 ; ... ; an|]] outputs [pr 0 a0 ++ ... ++ pr n an] *) - -let prvecti elem v = prvecti_with_sep mt elem v - -(* [prvect_with_sep sep pr [|a ; ... ; c|]] outputs - [pr a ++ sep() ++ ... ++ sep() ++ pr c] *) - -let prvect_with_sep sep elem v = prvecti_with_sep sep (fun _ -> elem) v - -(* [prvect pr [|a ; ... ; c|]] outputs [pr a ++ ... ++ pr c] *) - -let prvect elem v = prvect_with_sep mt elem v - -let pr_located pr (loc,x) = - if Flags.do_beautify() && loc<>dummy_loc then - let (b,e) = unloc loc in - comment b ++ pr x ++ comment e - else pr x - -let surround p = hov 1 (str"(" ++ p ++ str")") - (*s Memoization *) let memo1_eq eq f = diff --git a/lib/util.mli b/lib/util.mli index 1fec22954..caf1723b3 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -6,57 +6,9 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp -open Compat - (** This module contains numerous utility functions on strings, lists, arrays, etc. *) -(** {6 ... } *) -(** Errors. [Anomaly] is used for system errors and [UserError] for the - user's ones. *) - -exception Anomaly of string * std_ppcmds -val anomaly : string -> 'a -val anomalylabstrm : string -> std_ppcmds -> 'a - -exception UserError of string * std_ppcmds -val error : string -> 'a -val errorlabstrm : string -> std_ppcmds -> 'a - -exception AlreadyDeclared of std_ppcmds -val alreadydeclared : std_ppcmds -> 'a - -(** [todo] is for running of an incomplete code its implementation is - "do nothing" (or print a message), but this function should not be - used in a released code *) - -val todo : string -> unit - -exception Timeout - -type loc = Loc.t - -type 'a located = loc * 'a - -val unloc : loc -> int * int -val make_loc : int * int -> loc -val dummy_loc : loc -val join_loc : loc -> loc -> loc - -val anomaly_loc : loc * string * std_ppcmds -> 'a -val user_err_loc : loc * string * std_ppcmds -> 'a -val invalid_arg_loc : loc * string -> 'a -val located_fold_left : ('a -> 'b -> 'a) -> 'a -> 'b located -> 'a -val located_iter2 : ('a -> 'b -> unit) -> 'a located -> 'b located -> unit -val down_located : ('a -> 'b) -> 'a located -> 'b - -(** Like [Exc_located], but specifies the outermost file read, the - input buffer associated to the location of the error (or the module name - if boolean is true), and the error itself. *) - -exception Error_in_file of string * (bool * string * loc) * exn - (** Mapping under pairs *) val on_fst : ('a -> 'b) -> 'a * 'c -> 'b * 'c @@ -86,6 +38,7 @@ val is_letter : char -> bool val is_digit : char -> bool val is_ident_tail : char -> bool val is_blank : char -> bool +val next_utf8 : string -> int -> int * int (** {6 Strings. } *) @@ -108,9 +61,8 @@ type utf8_status = UnicodeLetter | UnicodeIdentPart | UnicodeSymbol exception UnsupportedUtf8 +val ident_refutation : string -> string option val classify_unicode : int -> utf8_status -val check_ident : string -> unit -val check_ident_soft : string -> unit val lowercase_first_char_utf8 : string -> string val ascii_of_ident : string -> string @@ -336,39 +288,6 @@ val interval : int -> int -> int list val map_succeed : ('a -> 'b) -> 'a list -> 'b list -(** {6 Pretty-printing. } *) - -val pr_spc : unit -> std_ppcmds -val pr_fnl : unit -> std_ppcmds -val pr_int : int -> std_ppcmds -val pr_str : string -> std_ppcmds -val pr_comma : unit -> std_ppcmds -val pr_semicolon : unit -> std_ppcmds -val pr_bar : unit -> std_ppcmds -val pr_arg : ('a -> std_ppcmds) -> 'a -> std_ppcmds -val pr_opt : ('a -> std_ppcmds) -> 'a option -> std_ppcmds -val pr_opt_no_spc : ('a -> std_ppcmds) -> 'a option -> std_ppcmds -val nth : int -> std_ppcmds - -val prlist : ('a -> std_ppcmds) -> 'a list -> std_ppcmds - -(** unlike all other functions below, [prlist] works lazily. - if a strict behavior is needed, use [prlist_strict] instead. *) -val prlist_strict : ('a -> std_ppcmds) -> 'a list -> std_ppcmds -val prlist_with_sep : - (unit -> std_ppcmds) -> ('b -> std_ppcmds) -> 'b list -> std_ppcmds -val prvect : ('a -> std_ppcmds) -> 'a array -> std_ppcmds -val prvecti : (int -> 'a -> std_ppcmds) -> 'a array -> std_ppcmds -val prvect_with_sep : - (unit -> std_ppcmds) -> ('a -> std_ppcmds) -> 'a array -> std_ppcmds -val prvecti_with_sep : - (unit -> std_ppcmds) -> (int -> 'a -> std_ppcmds) -> 'a array -> std_ppcmds -val pr_vertical_list : ('b -> std_ppcmds) -> 'b list -> std_ppcmds -val pr_enum : ('a -> std_ppcmds) -> 'a list -> std_ppcmds -val pr_located : ('a -> std_ppcmds) -> 'a located -> std_ppcmds -val pr_sequence : ('a -> std_ppcmds) -> 'a list -> std_ppcmds -val surround : std_ppcmds -> std_ppcmds - (** {6 Memoization. } *) (** General comments on memoization: diff --git a/lib/xml_lexer.mli b/lib/xml_lexer.mli index a1ca05765..ebb867190 100644 --- a/lib/xml_lexer.mli +++ b/lib/xml_lexer.mli @@ -41,4 +41,4 @@ val init : Lexing.lexbuf -> unit val close : Lexing.lexbuf -> unit val token : Lexing.lexbuf -> token val pos : Lexing.lexbuf -> pos -val restore : pos -> unit
\ No newline at end of file +val restore : pos -> unit diff --git a/library/assumptions.ml b/library/assumptions.ml index adc7f8edc..e047b62a6 100644 --- a/library/assumptions.ml +++ b/library/assumptions.ml @@ -14,6 +14,7 @@ (* Initial author: Arnaud Spiwack Module-traversing code: Pierre Letouzey *) +open Errors open Util open Names open Sign diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml index ba40f98c0..e8734cbaa 100644 --- a/library/decl_kinds.ml +++ b/library/decl_kinds.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Libnames diff --git a/library/decl_kinds.mli b/library/decl_kinds.mli index 88ef763c9..5b81d54ee 100644 --- a/library/decl_kinds.mli +++ b/library/decl_kinds.mli @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Libnames diff --git a/library/declare.ml b/library/declare.ml index 288580850..fd3139cf6 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -9,6 +9,7 @@ (** This module is about the low-level declaration of logical objects *) open Pp +open Errors open Util open Names open Libnames @@ -277,7 +278,7 @@ let declare_mind isrecord mie = (* Declaration messages *) -let pr_rank i = str (ordinal (i+1)) +let pr_rank i = pr_nth (i+1) let fixpoint_message indexes l = Flags.if_verbose msgnl (match l with diff --git a/library/declaremods.ml b/library/declaremods.ml index 90d4245a4..122404e22 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -7,6 +7,7 @@ (************************************************************************) open Pp +open Errors open Util open Names open Declarations diff --git a/library/declaremods.mli b/library/declaremods.mli index 9d44ba973..4027d9fad 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Pp +open Errors open Util open Names open Entries diff --git a/library/dischargedhypsmap.ml b/library/dischargedhypsmap.ml index ec92f679a..cd79e598d 100644 --- a/library/dischargedhypsmap.ml +++ b/library/dischargedhypsmap.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Libnames open Names diff --git a/library/global.ml b/library/global.ml index ab70bb7c3..926284f91 100644 --- a/library/global.ml +++ b/library/global.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Names open Term diff --git a/library/goptions.ml b/library/goptions.ml index 5af186899..30804fa5f 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -9,6 +9,7 @@ (* This module manages customization parameters at the vernacular level *) open Pp +open Errors open Util open Libobject open Names diff --git a/library/goptions.mli b/library/goptions.mli index d25c1202f..979bca2d2 100644 --- a/library/goptions.mli +++ b/library/goptions.mli @@ -44,6 +44,7 @@ (synchronous = consistent with the resetting commands) *) open Pp +open Errors open Util open Names open Libnames diff --git a/library/heads.ml b/library/heads.ml index 9f9f1ca25..327b883ee 100644 --- a/library/heads.ml +++ b/library/heads.ml @@ -7,6 +7,7 @@ (************************************************************************) open Pp +open Errors open Util open Names open Term diff --git a/library/impargs.ml b/library/impargs.ml index ef7f59216..b7dbd05fd 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Names open Libnames diff --git a/library/lib.ml b/library/lib.ml index 7554fd0bb..b98ad4110 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -7,6 +7,7 @@ (************************************************************************) open Pp +open Errors open Util open Libnames open Nameops diff --git a/library/lib.mli b/library/lib.mli index 0d6eb34b8..0a445f076 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -154,9 +154,9 @@ val close_section : unit -> unit (** {6 Backtracking (undo). } *) val reset_to : Libnames.object_name -> unit -val reset_name : Names.identifier Util.located -> unit -val remove_name : Names.identifier Util.located -> unit -val reset_mod : Names.identifier Util.located -> unit +val reset_name : Names.identifier Pp.located -> unit +val remove_name : Names.identifier Pp.located -> unit +val reset_mod : Names.identifier Pp.located -> unit (** [back n] resets to the place corresponding to the {% $ %}n{% $ %}-th call of [mark_end_of_command] (counting backwards) *) diff --git a/library/libnames.ml b/library/libnames.ml index b91d24bd6..24f083887 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -7,6 +7,7 @@ (************************************************************************) open Pp +open Errors open Util open Names open Nameops diff --git a/library/libnames.mli b/library/libnames.mli index 18b6ac49a..d3eed0364 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -7,6 +7,7 @@ (************************************************************************) open Pp +open Errors open Util open Names open Term diff --git a/library/libobject.ml b/library/libobject.ml index bc62913d9..b201c63a3 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Names open Libnames diff --git a/library/library.ml b/library/library.ml index 376228748..e2adb3fb9 100644 --- a/library/library.ml +++ b/library/library.ml @@ -7,6 +7,7 @@ (************************************************************************) open Pp +open Errors open Util open Names diff --git a/library/library.mli b/library/library.mli index ed17ed15b..c569ff485 100644 --- a/library/library.mli +++ b/library/library.mli @@ -6,7 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Util +open Errors +open Pp open Names open Libnames open Libobject diff --git a/library/nameops.ml b/library/nameops.ml index 799b8ebe1..ac163d3ef 100644 --- a/library/nameops.ml +++ b/library/nameops.ml @@ -7,6 +7,7 @@ (************************************************************************) open Pp +open Errors open Util open Names diff --git a/library/nametab.ml b/library/nametab.ml index 6dbd927d8..42edb156f 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Compat open Pp diff --git a/library/nametab.mli b/library/nametab.mli index c5b55f2ca..5183abbe8 100644 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Pp open Names diff --git a/library/states.ml b/library/states.ml index c88858f7e..82146f6b1 100644 --- a/library/states.ml +++ b/library/states.ml @@ -22,7 +22,7 @@ let (extern_state,intern_state) = extern_intern Coq_config.state_magic_number ".coq" in (fun s -> if !Flags.load_proofs <> Flags.Force then - Util.error "Write State only works with option -force-load-proofs"; + Errors.error "Write State only works with option -force-load-proofs"; raw_extern s (freeze())), (fun s -> unfreeze diff --git a/library/summary.ml b/library/summary.ml index 697f57e8e..d2168540b 100644 --- a/library/summary.ml +++ b/library/summary.ml @@ -7,6 +7,7 @@ (************************************************************************) open Pp +open Errors open Util type 'a summary_declaration = { diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4 index 3266fcf9a..788e664e2 100644 --- a/parsing/argextend.ml4 +++ b/parsing/argextend.ml4 @@ -14,8 +14,8 @@ open Egrammar open Pcoq open Compat -let loc = Util.dummy_loc -let default_loc = <:expr< Util.dummy_loc >> +let loc = Pp.dummy_loc +let default_loc = <:expr< Pp.dummy_loc >> let rec make_rawwit loc = function | BoolArgType -> <:expr< Genarg.rawwit_bool >> @@ -203,8 +203,8 @@ let declare_vernac_argument loc s pr cl = (None, [(None, None, $rules$)]); Pptactic.declare_extra_genarg_pprule ($rawwit$, $pr_rules$) - ($globwit$, fun _ _ _ _ -> Util.anomaly "vernac argument needs not globwit printer") - ($wit$, fun _ _ _ _ -> Util.anomaly "vernac argument needs not wit printer") } + ($globwit$, fun _ _ _ _ -> Errors.anomaly "vernac argument needs not globwit printer") + ($wit$, fun _ _ _ _ -> Errors.anomaly "vernac argument needs not wit printer") } >> ] open Vernacexpr diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml index 4418a45f7..f30e061ff 100644 --- a/parsing/egrammar.ml +++ b/parsing/egrammar.ml @@ -8,6 +8,7 @@ open Pp open Compat +open Errors open Util open Pcoq open Extend diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli index 1d85c74e5..4a5f3c4c6 100644 --- a/parsing/egrammar.mli +++ b/parsing/egrammar.mli @@ -7,7 +7,8 @@ (************************************************************************) open Compat -open Util +open Errors +open Pp open Names open Topconstr open Pcoq diff --git a/parsing/extend.ml b/parsing/extend.ml index fca24ed5a..22d640f50 100644 --- a/parsing/extend.ml +++ b/parsing/extend.ml @@ -7,6 +7,7 @@ (************************************************************************) open Compat +open Errors open Util (** Entry keys for constr notations *) diff --git a/parsing/extrawit.ml b/parsing/extrawit.ml index ce7346220..cc5b58ee7 100644 --- a/parsing/extrawit.ml +++ b/parsing/extrawit.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Genarg diff --git a/parsing/extrawit.mli b/parsing/extrawit.mli index 2d2eef37d..3043fd04b 100644 --- a/parsing/extrawit.mli +++ b/parsing/extrawit.mli @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Genarg open Tacexpr diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index af63e215f..a8adfb19a 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -44,7 +44,7 @@ let mk_fixb (id,bl,ann,body,(loc,tyc)) = let mk_cofixb (id,bl,ann,body,(loc,tyc)) = let _ = Option.map (fun (aloc,_) -> - Util.user_err_loc + Errors.user_err_loc (aloc,"Constr:mk_cofixb", Pp.str"Annotation forbidden in cofix expression.")) (fst ann) in let ty = match tyc with @@ -332,7 +332,7 @@ GEXTEND Gram [ p = pattern; lp = LIST1 NEXT -> (match p with | CPatAtom (_, Some r) -> CPatCstr (loc, r, lp) - | _ -> Util.user_err_loc + | _ -> Errors.user_err_loc (cases_pattern_expr_loc p, "compound_pattern", Pp.str "Constructor expected.")) |"@"; r = Prim.reference; lp = LIST1 NEXT -> diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4 index 307e1779e..fd6fc7dd8 100644 --- a/parsing/g_prim.ml4 +++ b/parsing/g_prim.ml4 @@ -29,7 +29,7 @@ let my_int_of_string loc s = if n > 1024 * 2048 then raise Exit; n with Failure _ | Exit -> - Util.user_err_loc (loc,"",Pp.str "Cannot support a so large number.") + Errors.user_err_loc (loc,"",Pp.str "Cannot support a so large number.") GEXTEND Gram GLOBAL: @@ -94,7 +94,7 @@ GEXTEND Gram ; ne_string: [ [ s = STRING -> - if s="" then Util.user_err_loc(loc,"",Pp.str"Empty string."); s + if s="" then Errors.user_err_loc(loc,"",Pp.str"Empty string."); s ] ] ; ne_lstring: diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 442aab00e..7d5e976d3 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -8,6 +8,7 @@ open Pp open Pcoq +open Errors open Util open Tacexpr open Glob_term @@ -117,7 +118,7 @@ let mk_fix_tac (loc,id,bl,ann,ty) = let mk_cofix_tac (loc,id,bl,ann,ty) = let _ = Option.map (fun (aloc,_) -> - Util.user_err_loc + Errors.user_err_loc (aloc,"Constr:mk_cofix_tac", Pp.str"Annotation forbidden in cofix expression.")) ann in (id,CProdN(loc,bl,ty)) diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index a2e053ab8..a52903df0 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -9,6 +9,7 @@ open Pp open Compat open Tok +open Errors open Util open Names open Topconstr diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4 index 1d55a587f..09af49f62 100644 --- a/parsing/g_xml.ml4 +++ b/parsing/g_xml.ml4 @@ -7,6 +7,7 @@ (************************************************************************) open Pp +open Errors open Util open Names open Term diff --git a/parsing/grammar.mllib b/parsing/grammar.mllib index ba393e637..0d7cd3649 100644 --- a/parsing/grammar.mllib +++ b/parsing/grammar.mllib @@ -2,13 +2,13 @@ Coq_config Profile Pp_control -Pp Compat Flags +Pp Segmenttree Unicodetable -Util Errors +Util Bigint Dyn Hashcons diff --git a/parsing/lexer.mli b/parsing/lexer.mli index 1899f7f4d..eda9cea49 100644 --- a/parsing/lexer.mli +++ b/parsing/lexer.mli @@ -7,6 +7,7 @@ (************************************************************************) open Pp +open Errors open Util val add_keyword : string -> unit diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index 075440f1c..ee241384b 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -9,6 +9,7 @@ open Pp open Compat open Tok +open Errors open Util open Names open Extend diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index bba0e5602..ebcc53264 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -6,7 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Util +open Pp +open Errors open Names open Glob_term open Extend diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index 1f37e36df..20479fe14 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -7,6 +7,7 @@ (************************************************************************) (*i*) +open Errors open Util open Pp open Nametab diff --git a/parsing/ppconstr.mli b/parsing/ppconstr.mli index afcdad3e4..c61d4c206 100644 --- a/parsing/ppconstr.mli +++ b/parsing/ppconstr.mli @@ -14,6 +14,7 @@ open Pcoq open Glob_term open Topconstr open Names +open Errors open Util open Genarg diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 3305acb77..2f80afdbe 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -9,6 +9,7 @@ open Pp open Names open Namegen +open Errors open Util open Tacexpr open Glob_term @@ -133,7 +134,7 @@ let rec pr_raw_generic prc prlc prtac prpat prref (x:Genarg.rlevel Genarg.generi match Genarg.genarg_tag x with | BoolArgType -> str (if out_gen rawwit_bool x then "true" else "false") | IntArgType -> int (out_gen rawwit_int x) - | IntOrVarArgType -> pr_or_var pr_int (out_gen rawwit_int_or_var x) + | IntOrVarArgType -> pr_or_var int (out_gen rawwit_int_or_var x) | StringArgType -> str "\"" ++ str (out_gen rawwit_string x) ++ str "\"" | PreIdentArgType -> str (out_gen rawwit_pre_ident x) | IntroPatternArgType -> pr_intro_pattern (out_gen rawwit_intro_pattern x) @@ -176,7 +177,7 @@ let rec pr_glob_generic prc prlc prtac prpat x = match Genarg.genarg_tag x with | BoolArgType -> str (if out_gen globwit_bool x then "true" else "false") | IntArgType -> int (out_gen globwit_int x) - | IntOrVarArgType -> pr_or_var pr_int (out_gen globwit_int_or_var x) + | IntOrVarArgType -> pr_or_var int (out_gen globwit_int_or_var x) | StringArgType -> str "\"" ++ str (out_gen globwit_string x) ++ str "\"" | PreIdentArgType -> str (out_gen globwit_pre_ident x) | IntroPatternArgType -> pr_intro_pattern (out_gen globwit_intro_pattern x) @@ -222,7 +223,7 @@ let rec pr_generic prc prlc prtac prpat x = match Genarg.genarg_tag x with | BoolArgType -> str (if out_gen wit_bool x then "true" else "false") | IntArgType -> int (out_gen wit_int x) - | IntOrVarArgType -> pr_or_var pr_int (out_gen wit_int_or_var x) + | IntOrVarArgType -> pr_or_var int (out_gen wit_int_or_var x) | StringArgType -> str "\"" ++ str (out_gen wit_string x) ++ str "\"" | PreIdentArgType -> str (out_gen wit_pre_ident x) | IntroPatternArgType -> pr_intro_pattern (out_gen wit_intro_pattern x) @@ -423,8 +424,8 @@ let pr_orient b = if b then mt () else str " <-" let pr_multi = function | Precisely 1 -> mt () - | Precisely n -> pr_int n ++ str "!" - | UpTo n -> pr_int n ++ str "?" + | Precisely n -> int n ++ str "!" + | UpTo n -> int n ++ str "?" | RepeatStar -> str "?" | RepeatPlus -> str "!" diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index 5a8f2db79..5b8985e9a 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -11,6 +11,7 @@ open Names open Nameops open Nametab open Compat +open Errors open Util open Extend open Vernacexpr @@ -928,7 +929,7 @@ let rec pr_vernac = function | VernacProof (None, None) -> str "Proof" | VernacProof (None, Some l) -> str "Proof using" ++spc()++ prlist pr_lident l | VernacProof (Some te, None) -> str "Proof with" ++ spc() ++ pr_raw_tactic te - | VernacProof (Some te, Some l) -> + | VernacProof (Some te, Some l) -> str "Proof using" ++spc()++ prlist pr_lident l ++ spc() ++ str "with" ++ spc() ++pr_raw_tactic te | VernacProofMode s -> str ("Proof Mode "^s) @@ -938,7 +939,7 @@ let rec pr_vernac = function | Plus -> str"+" end ++ spc() | VernacSubproof None -> str "BeginSubproof" - | VernacSubproof (Some i) -> str "BeginSubproof " ++ pr_int i + | VernacSubproof (Some i) -> str "BeginSubproof " ++ int i | VernacEndSubproof -> str "EndSubproof" and pr_extend s cl = diff --git a/parsing/ppvernac.mli b/parsing/ppvernac.mli index 6d83ca474..91bb19a8c 100644 --- a/parsing/ppvernac.mli +++ b/parsing/ppvernac.mli @@ -12,6 +12,7 @@ open Vernacexpr open Names open Nameops open Nametab +open Errors open Util open Ppconstr open Pptactic diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index e30979bf9..fad4e879e 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -11,6 +11,7 @@ *) open Pp +open Errors open Util open Names open Nameops @@ -152,7 +153,7 @@ let print_argument_scopes prefix = function | l when not (List.for_all ((=) None) l) -> [add_colon prefix ++ hov 2 (str"Argument scopes are" ++ spc() ++ str "[" ++ - prlist_with_sep spc (function Some sc -> str sc | None -> str "_") l ++ + pr_sequence (function Some sc -> str sc | None -> str "_") l ++ str "]")] | _ -> [] @@ -168,12 +169,7 @@ let print_simpl_behaviour ref = let pp_nomatch = spc() ++ if nomatch then str "avoiding to expose match constructs" else str"" in let pp_recargs = spc() ++ str "when the " ++ - let rec aux = function - | [] -> mt() - | [x] -> str (ordinal (x+1)) - | [x;y] -> str (ordinal (x+1)) ++ str " and " ++ str (ordinal (y+1)) - | x::tl -> str (ordinal (x+1)) ++ str ", " ++ aux tl in - aux recargs ++ str (plural (List.length recargs) " argument") ++ + pr_enum (fun x -> pr_nth (x+1)) recargs ++ str (plural (List.length recargs) " argument") ++ str (plural (if List.length recargs >= 2 then 1 else 2) " evaluate") ++ str " to a constructor" in let pp_nargs = @@ -722,13 +718,13 @@ let print_path ((i,j),p) = let _ = Classops.install_path_printer print_path let print_graph () = - prlist_with_sep pr_fnl print_path (inheritance_graph()) + prlist_with_sep fnl print_path (inheritance_graph()) let print_classes () = - prlist_with_sep pr_spc pr_class (classes()) + pr_sequence pr_class (classes()) let print_coercions () = - prlist_with_sep pr_spc print_coercion_value (coercions()) + pr_sequence print_coercion_value (coercions()) let index_of_class cl = try @@ -751,7 +747,7 @@ let print_path_between cls clt = print_path ((i,j),p) let print_canonical_projections () = - prlist_with_sep pr_fnl + prlist_with_sep fnl (fun ((r1,r2),o) -> pr_cs_pattern r2 ++ str " <- " ++ pr_global r1 ++ str " ( " ++ pr_lconstr o.o_DEF ++ str " )") diff --git a/parsing/prettyp.mli b/parsing/prettyp.mli index 6d9c6ecc6..40ba7f047 100644 --- a/parsing/prettyp.mli +++ b/parsing/prettyp.mli @@ -7,6 +7,7 @@ (************************************************************************) open Pp +open Errors open Util open Names open Sign diff --git a/parsing/printer.ml b/parsing/printer.ml index 0a3926660..3d2f3e089 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -7,6 +7,7 @@ (************************************************************************) open Pp +open Errors open Util open Names open Nameops @@ -505,17 +506,17 @@ let pr_prim_rule = function ++ pr_id id ++ str" (type of " ++ pr_id id ++ str ")") | Thin ids -> - (str"clear " ++ prlist_with_sep pr_spc pr_id ids) + (str"clear " ++ pr_sequence pr_id ids) | ThinBody ids -> - (str"clearbody " ++ prlist_with_sep pr_spc pr_id ids) + (str"clearbody " ++ pr_sequence pr_id ids) | Move (withdep,id1,id2) -> (str (if withdep then "dependent " else "") ++ str"move " ++ pr_id id1 ++ pr_move_location pr_id id2) | Order ord -> - (str"order " ++ prlist_with_sep pr_spc pr_id ord) + (str"order " ++ pr_sequence pr_id ord) | Rename (id1,id2) -> (str "rename " ++ pr_id id1 ++ str " into " ++ pr_id id2) diff --git a/parsing/printmod.ml b/parsing/printmod.ml index 9cf76585e..cf047bfa3 100644 --- a/parsing/printmod.ml +++ b/parsing/printmod.ml @@ -7,6 +7,7 @@ (************************************************************************) open Pp +open Errors open Util open Names open Declarations diff --git a/parsing/q_constr.ml4 b/parsing/q_constr.ml4 index 605432692..5bd215190 100644 --- a/parsing/q_constr.ml4 +++ b/parsing/q_constr.ml4 @@ -13,13 +13,13 @@ open Term open Names open Pattern open Q_util -open Util +open Pp open Compat open Pcaml open PcamlSig let loc = dummy_loc -let dloc = <:expr< Util.dummy_loc >> +let dloc = <:expr< Pp.dummy_loc >> let apply_ref f l = <:expr< diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index 552c86903..389118c34 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Util +open Pp open Names open Libnames open Q_util @@ -24,7 +24,7 @@ let anti loc x = (* We don't give location for tactic quotation! *) let loc = dummy_loc -let dloc = <:expr< Util.dummy_loc >> +let dloc = <:expr< Pp.dummy_loc >> let mlexpr_of_ident id = <:expr< Names.id_of_string $str:Names.string_of_id id$ >> diff --git a/parsing/q_util.ml4 b/parsing/q_util.ml4 index 91ab29f1d..cfaa2a654 100644 --- a/parsing/q_util.ml4 +++ b/parsing/q_util.ml4 @@ -10,7 +10,7 @@ open Extrawit open Compat -open Util +open Pp let mlexpr_of_list f l = List.fold_right @@ -64,6 +64,6 @@ let rec mlexpr_of_prod_entry_key = function | Pcoq.Aself -> <:expr< Pcoq.Aself >> | Pcoq.Anext -> <:expr< Pcoq.Anext >> | Pcoq.Atactic n -> <:expr< Pcoq.Atactic $mlexpr_of_int n$ >> - | Pcoq.Agram s -> Util.anomaly "Agram not supported" + | Pcoq.Agram s -> Errors.anomaly "Agram not supported" | Pcoq.Aentry ("",s) -> <:expr< Pcoq.Agram (Pcoq.Gram.Entry.obj $lid:s$) >> | Pcoq.Aentry (u,s) -> <:expr< Pcoq.Aentry $str:u$ $str:s$ >> diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4 index 2fe1fdda7..838c771c6 100644 --- a/parsing/tacextend.ml4 +++ b/parsing/tacextend.ml4 @@ -9,6 +9,7 @@ (*i camlp4deps: "tools/compat5b.cmo" i*) open Util +open Pp open Genarg open Q_util open Q_coqast @@ -196,7 +197,7 @@ EXTEND let t, g = interp_entry_name false None e sep in GramNonTerminal (loc, t, g, Some (Names.id_of_string s)) | s = STRING -> - if s = "" then Util.user_err_loc (loc,"",Pp.str "Empty terminal."); + if s = "" then Errors.user_err_loc (loc,"",Pp.str "Empty terminal."); GramTerminal s ] ] ; diff --git a/parsing/tactic_printer.ml b/parsing/tactic_printer.ml index 83dae3dce..b2b59f166 100644 --- a/parsing/tactic_printer.ml +++ b/parsing/tactic_printer.ml @@ -7,6 +7,7 @@ (************************************************************************) open Pp +open Errors open Util open Sign open Evd @@ -66,7 +67,7 @@ let rec print_proof sigma osign pf = spc () ++ str" BY " ++ hov 0 (pr_rule r) ++ fnl () ++ str" " ++ - hov 0 (prlist_with_sep pr_fnl (print_proof sigma hyps) spfl)) + hov 0 (prlist_with_sep fnl (print_proof sigma hyps) spfl)) let pr_change sigma gl = str"change " ++ @@ -110,11 +111,11 @@ let print_script ?(nochange=true) sigma pf = end | Some(Daimon,spfl) -> ((if nochange then (mt ()) else (pr_change sigma pf.goal ++ fnl ())) ++ - prlist_with_sep pr_fnl print_prf spfl ) + prlist_with_sep fnl print_prf spfl ) | Some(rule,spfl) -> ((if nochange then (mt ()) else (pr_change sigma pf.goal ++ fnl ())) ++ pr_rule_dot_fnl rule ++ - prlist_with_sep pr_fnl print_prf spfl ) in + prlist_with_sep fnl print_prf spfl ) in print_prf pf (* printed by Show Script command *) @@ -140,7 +141,7 @@ let print_treescript ?(nochange=true) sigma pf = end | Some(Daimon,spfl) -> (if nochange then mt () else pr_change sigma pf.goal ++ fnl ()) ++ - prlist_with_sep pr_fnl (print_script ~nochange sigma) spfl + prlist_with_sep fnl (print_script ~nochange sigma) spfl | Some(r,spfl) -> let indent = if List.length spfl >= 2 then 1 else 0 in (if nochange then mt () else pr_change sigma pf.goal ++ fnl ()) ++ @@ -162,7 +163,7 @@ let rec print_info_script sigma osign pf = print_info_script sigma (Environ.named_context_of_val sign) pf1) | _ -> (str"." ++ fnl () ++ - prlist_with_sep pr_fnl + prlist_with_sep fnl (print_info_script sigma (Environ.named_context_of_val sign)) spfl)) diff --git a/parsing/vernacextend.ml4 b/parsing/vernacextend.ml4 index 88a750792..7553aef4a 100644 --- a/parsing/vernacextend.ml4 +++ b/parsing/vernacextend.ml4 @@ -8,6 +8,7 @@ (*i camlp4deps: "tools/compat5b.cmo" i*) +open Pp open Util open Genarg open Q_util @@ -79,7 +80,7 @@ EXTEND rule: [ [ "["; s = STRING; l = LIST0 args; "]"; "->"; "["; e = Pcaml.expr; "]" -> - if s = "" then Util.user_err_loc (loc,"",Pp.str"Command name is empty."); + if s = "" then Errors.user_err_loc (loc,"",Pp.str"Command name is empty."); (Some s,l,<:expr< fun () -> $e$ >>) | "[" ; "-" ; l = LIST1 args ; "]" ; "->" ; "[" ; e = Pcaml.expr ; "]" -> (None,l,<:expr< fun () -> $e$ >>) diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index e3d27f719..7434f5e8a 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -9,6 +9,7 @@ (* This file implements the basic congruence-closure algorithm by *) (* Downey,Sethi and Tarjan. *) +open Errors open Util open Pp open Goptions diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli index 78dbee3fe..d530495f8 100644 --- a/plugins/cc/ccalgo.mli +++ b/plugins/cc/ccalgo.mli @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Term open Names diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml index bb1d50c99..4c8c80ba4 100644 --- a/plugins/cc/ccproof.ml +++ b/plugins/cc/ccproof.ml @@ -9,6 +9,7 @@ (* This file uses the (non-compressed) union-find structure to generate *) (* proof-trees that will be transformed into proof-terms in cctac.ml4 *) +open Errors open Util open Names open Term diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index ec31f8917..0a3697e2a 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -26,6 +26,7 @@ open Ccalgo open Tacinterp open Ccproof open Pp +open Errors open Util open Format @@ -410,7 +411,7 @@ let cc_tactic depth additionnal_terms gls= begin str "\"congruence with (" ++ prlist_with_sep - (fun () -> str ")" ++ pr_spc () ++ str "(") + (fun () -> str ")" ++ spc () ++ str "(") (Termops.print_constr_env (pf_env gls)) terms_to_complete ++ str ")\"," diff --git a/plugins/decl_mode/decl_expr.mli b/plugins/decl_mode/decl_expr.mli index fa6acaeb1..e84864f96 100644 --- a/plugins/decl_mode/decl_expr.mli +++ b/plugins/decl_mode/decl_expr.mli @@ -7,7 +7,7 @@ (************************************************************************) open Names -open Util +open Pp open Tacexpr type 'it statement = diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index b3e076c49..512269e55 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Names open Topconstr diff --git a/plugins/decl_mode/decl_mode.ml b/plugins/decl_mode/decl_mode.ml index af6aa4bf5..5f9563cb2 100644 --- a/plugins/decl_mode/decl_mode.ml +++ b/plugins/decl_mode/decl_mode.ml @@ -9,6 +9,7 @@ open Names open Term open Evd +open Errors open Util diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index c1553b35d..e3a95fb4f 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Pp open Evd diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4 index 27def8cc1..88e62e46d 100644 --- a/plugins/decl_mode/g_decl_mode.ml4 +++ b/plugins/decl_mode/g_decl_mode.ml4 @@ -46,15 +46,15 @@ let pr_open_subgoals () = *) let pr_proof_instr instr = - Util.anomaly "Cannot print a proof_instr" + Errors.anomaly "Cannot print a proof_instr" (* arnaud: Il nous faut quelque chose de type extr_genarg_printer si on veut aller dans cette direction Ppdecl_proof.pr_proof_instr (Global.env()) instr *) let pr_raw_proof_instr instr = - Util.anomaly "Cannot print a raw proof_instr" + Errors.anomaly "Cannot print a raw proof_instr" let pr_glob_proof_instr instr = - Util.anomaly "Cannot print a non-interpreted proof_instr" + Errors.anomaly "Cannot print a non-interpreted proof_instr" let interp_proof_instr _ { Evd.it = gl ; sigma = sigma }= Decl_interp.interp_proof_instr @@ -65,7 +65,7 @@ let interp_proof_instr _ { Evd.it = gl ; sigma = sigma }= let vernac_decl_proof () = let pf = Proof_global.give_me_the_proof () in if Proof.is_done pf then - Util.error "Nothing left to prove here." + Errors.error "Nothing left to prove here." else Proof.transaction pf begin fun () -> Decl_proof_instr.go_to_proof_mode () ; diff --git a/plugins/decl_mode/ppdecl_proof.ml b/plugins/decl_mode/ppdecl_proof.ml index b866efaba..a2e078ee2 100644 --- a/plugins/decl_mode/ppdecl_proof.ml +++ b/plugins/decl_mode/ppdecl_proof.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Pp open Decl_expr diff --git a/plugins/dp/dp.ml b/plugins/dp/dp.ml index 837195e44..fd96b6d1c 100644 --- a/plugins/dp/dp.ml +++ b/plugins/dp/dp.ml @@ -11,6 +11,7 @@ Zenon) *) +open Errors open Util open Pp open Libobject diff --git a/plugins/dp/dp_zenon.mll b/plugins/dp/dp_zenon.mll index 949e91e34..1e82034c0 100644 --- a/plugins/dp/dp_zenon.mll +++ b/plugins/dp/dp_zenon.mll @@ -3,7 +3,7 @@ open Lexing open Pp - open Util + open Errors open Names open Tacmach open Dp_why diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index 0bd5b8434..1b443f753 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -7,6 +7,7 @@ (************************************************************************) open Pp +open Errors open Util open Names open Term diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 73062328b..7c517dd9b 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -11,6 +11,7 @@ open Declarations open Names open Libnames open Pp +open Errors open Util open Miniml open Table diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 219b3913f..d9ee92c05 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -7,6 +7,7 @@ (************************************************************************) (*i*) +open Errors open Util open Names open Term diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml index 96731ed27..fe249cd65 100644 --- a/plugins/extraction/haskell.ml +++ b/plugins/extraction/haskell.ml @@ -9,6 +9,7 @@ (*s Production of Haskell syntax. *) open Pp +open Errors open Util open Names open Nameops diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli index 5a19cc3f5..a5b57a474 100644 --- a/plugins/extraction/miniml.mli +++ b/plugins/extraction/miniml.mli @@ -9,6 +9,7 @@ (*s Target language for extraction: a core ML called MiniML. *) open Pp +open Errors open Util open Names open Libnames diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index c244e046d..f03170948 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -8,6 +8,7 @@ (*i*) open Pp +open Errors open Util open Names open Libnames diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli index 029e8cf46..630db6f06 100644 --- a/plugins/extraction/mlutil.mli +++ b/plugins/extraction/mlutil.mli @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Names open Term diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index 9e8dd8286..123edd4c3 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -10,6 +10,7 @@ open Names open Declarations open Environ open Libnames +open Errors open Util open Miniml open Table diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index ed69ec457..d99bca6f4 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -9,6 +9,7 @@ (*s Production of Ocaml syntax. *) open Pp +open Errors open Util open Names open Nameops diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml index 215076555..157788ece 100644 --- a/plugins/extraction/scheme.ml +++ b/plugins/extraction/scheme.ml @@ -9,6 +9,7 @@ (*s Production of Scheme syntax. *) open Pp +open Errors open Util open Names open Nameops diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 238befd25..667182480 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -15,6 +15,7 @@ open Summary open Libobject open Goptions open Libnames +open Errors open Util open Pp open Miniml @@ -337,7 +338,7 @@ let warning_both_mod_and_cst q mp r = let error_axiom_scheme r i = err (str "The type scheme axiom " ++ spc () ++ - safe_pr_global r ++ spc () ++ str "needs " ++ pr_int i ++ + safe_pr_global r ++ spc () ++ str "needs " ++ int i ++ str " type variable(s).") let check_inside_module () = diff --git a/plugins/field/field.ml4 b/plugins/field/field.ml4 index 9e4f4d745..15c495ae7 100644 --- a/plugins/field/field.ml4 +++ b/plugins/field/field.ml4 @@ -15,6 +15,7 @@ open Tacinterp open Tacmach open Term open Typing +open Errors open Util open Vernacinterp open Vernacexpr diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml index d67dceeac..566b2b8b0 100644 --- a/plugins/firstorder/formula.ml +++ b/plugins/firstorder/formula.ml @@ -12,6 +12,7 @@ open Term open Termops open Reductionops open Tacmach +open Errors open Util open Declarations open Libnames diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index 4a38c48dc..f5b16e43f 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -17,7 +17,6 @@ open Tacticals open Tacinterp open Term open Names -open Util open Libnames (* declaring search depth as a global option *) @@ -103,6 +102,7 @@ let normalize_evaluables= unfold_in_hyp (Lazy.force defined_connectives) (Tacexpr.InHypType id)) *) +open Pp open Genarg open Ppconstr open Printer diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index 16831d3ec..8d4b0eee1 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -10,6 +10,8 @@ open Formula open Sequent open Unify open Rules +open Pp +open Errors open Util open Term open Glob_term diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index 23eeb2f66..b56fe4e50 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Names open Term diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index f75678c60..780e3f3e7 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -7,6 +7,7 @@ (************************************************************************) open Term +open Errors open Util open Formula open Unify @@ -235,7 +236,7 @@ let print_cmap map= let print_entry c l s= let xc=Constrextern.extern_constr false (Global.env ()) c in str "| " ++ - Util.prlist Printer.pr_global l ++ + prlist Printer.pr_global l ++ str " : " ++ Ppconstr.pr_constr_expr xc ++ cut () ++ diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli index c5c2bb954..5587e9fbb 100644 --- a/plugins/firstorder/sequent.mli +++ b/plugins/firstorder/sequent.mli @@ -7,6 +7,7 @@ (************************************************************************) open Term +open Errors open Util open Formula open Tacmach diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml index 299a0054a..48c402cc0 100644 --- a/plugins/firstorder/unify.ml +++ b/plugins/firstorder/unify.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Formula open Tacmach diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index 484937858..1a629aac9 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -503,11 +503,11 @@ let rec fourier gl= with _ -> ()) hyps; (* lineq = les inéquations découlant des hypothèses *) - if !lineq=[] then Util.error "No inequalities"; + if !lineq=[] then Errors.error "No inequalities"; let res=fourier_lineq (!lineq) in let tac=ref tclIDTAC in if res=[] - then Util.error "fourier failed" + then Errors.error "fourier failed" (* l'algorithme de Fourier a réussi: on va en tirer une preuve Coq *) else (match res with [(cres,sres,lc)]-> diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 865074d6b..13b3dabdf 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -1,4 +1,5 @@ open Printer +open Errors open Util open Term open Namegen @@ -1048,7 +1049,7 @@ let do_replace params rec_arg_num rev_args_id f fun_num all_funs g = {finfos with equation_lemma = Some (match Nametab.locate (qualid_of_ident equation_lemma_id) with ConstRef c -> c - | _ -> Util.anomaly "Not a constant" + | _ -> Errors.anomaly "Not a constant" ) } | _ -> () diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 6df9d574f..0f776ee6e 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -1,4 +1,5 @@ open Printer +open Errors open Util open Term open Namegen @@ -304,7 +305,7 @@ let defined () = Lemmas.save_named false with | UserError("extract_proof",msg) -> - Util.errorlabstrm + Errors.errorlabstrm "defined" ((try str "On goal : " ++ fnl () ++ pr_open_subgoals () ++ fnl () @@ -659,9 +660,9 @@ let build_scheme fas = try match Nametab.global f with | Libnames.ConstRef c -> c - | _ -> Util.error "Functional Scheme can only be used with functions" + | _ -> Errors.error "Functional Scheme can only be used with functions" with Not_found -> - Util.error ("Cannot find "^ Libnames.string_of_reference f) + Errors.error ("Cannot find "^ Libnames.string_of_reference f) in (f_as_constant,sort) ) @@ -692,7 +693,7 @@ let build_case_scheme fa = let funs = (fun (_,f,_) -> try Libnames.constr_of_global (Nametab.global f) with Not_found -> - Util.error ("Cannot find "^ Libnames.string_of_reference f)) fa in + Errors.error ("Cannot find "^ Libnames.string_of_reference f)) fa in let first_fun = destConst funs in let funs_mp,funs_dp,_ = Names.repr_con first_fun in diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 123399d56..f330f9ff9 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -25,10 +25,10 @@ let pr_binding prc = function let pr_bindings prc prlc = function | Glob_term.ImplicitBindings l -> brk (1,1) ++ str "with" ++ brk (1,1) ++ - Util.prlist_with_sep spc prc l + pr_sequence prc l | Glob_term.ExplicitBindings l -> brk (1,1) ++ str "with" ++ brk (1,1) ++ - Util.prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l + pr_sequence (fun b -> str"(" ++ pr_binding prlc b ++ str")") l | Glob_term.NoBindings -> mt () let pr_with_bindings prc prlc (c,bl) = @@ -111,7 +111,7 @@ TACTIC EXTEND snewfunind END -let pr_constr_coma_sequence prc _ _ = Util.prlist_with_sep Util.pr_comma prc +let pr_constr_coma_sequence prc _ _ = prlist_with_sep pr_comma prc ARGUMENT EXTEND constr_coma_sequence' TYPED AS constr_list @@ -180,12 +180,12 @@ let warning_error names e = | Building_graph e -> Pp.msg_warning (str "Cannot define graph(s) for " ++ - h 1 (prlist_with_sep (fun _ -> str","++spc ()) Libnames.pr_reference names) ++ + h 1 (pr_enum Libnames.pr_reference names) ++ if do_observe () then (spc () ++ Errors.print e) else mt ()) | Defining_principle e -> Pp.msg_warning (str "Cannot define principle(s) for "++ - h 1 (prlist_with_sep (fun _ -> str","++spc ()) Libnames.pr_reference names) ++ + h 1 (pr_enum Libnames.pr_reference names) ++ if do_observe () then Errors.print e else mt ()) | _ -> raise e @@ -207,7 +207,7 @@ VERNAC COMMAND EXTEND NewFunctionalScheme ; try Functional_principles_types.build_scheme fas with Functional_principles_types.No_graph_found -> - Util.error ("Cannot generate induction principle(s)") + Errors.error ("Cannot generate induction principle(s)") | e -> let names = List.map (fun (_,na,_) -> na) fas in warning_error names e @@ -377,7 +377,7 @@ let finduction (oid:identifier option) (heuristic: fapp_info list -> fapp_info l let info_list = find_fapp test g in let ordered_info_list = heuristic info_list in prlistconstr (List.map (fun x -> applist (x.fname,x.largs)) ordered_info_list); - if List.length ordered_info_list = 0 then Util.error "function not found in goal\n"; + if List.length ordered_info_list = 0 then Errors.error "function not found in goal\n"; let taclist: Proof_type.tactic list = List.map (fun info -> @@ -419,7 +419,7 @@ TACTIC EXTEND finduction ["finduction" ident(id) natural_opt(oi)] -> [ match oi with - | Some(n) when n<=0 -> Util.error "numerical argument must be > 0" + | Some(n) when n<=0 -> Errors.error "numerical argument must be > 0" | _ -> let heuristic = chose_heuristic oi in finduction (Some id) heuristic tclIDTAC @@ -458,19 +458,19 @@ VERNAC COMMAND EXTEND MergeFunind "with" "(" ident(id2) ne_ident_list(cl2) ")" "using" ident(id) ] -> [ let f1 = Constrintern.interp_constr Evd.empty (Global.env()) - (CRef (Libnames.Ident (Util.dummy_loc,id1))) in + (CRef (Libnames.Ident (Pp.dummy_loc,id1))) in let f2 = Constrintern.interp_constr Evd.empty (Global.env()) - (CRef (Libnames.Ident (Util.dummy_loc,id2))) in + (CRef (Libnames.Ident (Pp.dummy_loc,id2))) in let f1type = Typing.type_of (Global.env()) Evd.empty f1 in let f2type = Typing.type_of (Global.env()) Evd.empty f2 in let ar1 = List.length (fst (decompose_prod f1type)) in let ar2 = List.length (fst (decompose_prod f2type)) in let _ = if ar1 <> List.length cl1 then - Util.error ("not the right number of arguments for " ^ string_of_id id1) in + Errors.error ("not the right number of arguments for " ^ string_of_id id1) in let _ = if ar2 <> List.length cl2 then - Util.error ("not the right number of arguments for " ^ string_of_id id2) in + Errors.error ("not the right number of arguments for " ^ string_of_id id2) in Merge.merge id1 id2 (Array.of_list cl1) (Array.of_list cl2) id ] END diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index c88c66693..6a5888874 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -5,6 +5,7 @@ open Term open Glob_term open Libnames open Indfun_common +open Errors open Util open Glob_termops @@ -977,8 +978,8 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = ((Util.list_chop nparam args')) in let rt_typ = - GApp(Util.dummy_loc, - GRef (Util.dummy_loc,Libnames.IndRef ind), + GApp(Pp.dummy_loc, + GRef (Pp.dummy_loc,Libnames.IndRef ind), (List.map (fun p -> Detyping.detype false [] (Termops.names_of_rel_context env) diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index cdd0eaf71..b458346d4 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -1,5 +1,6 @@ open Pp open Glob_term +open Errors open Util open Names (* Ocaml 3.06 Map.S does not handle is_empty *) diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli index bfd153579..80a8811f1 100644 --- a/plugins/funind/glob_termops.mli +++ b/plugins/funind/glob_termops.mli @@ -84,9 +84,9 @@ val alpha_rt : Names.identifier list -> glob_constr -> glob_constr (* same as alpha_rt but for case branches *) val alpha_br : Names.identifier list -> - Util.loc * Names.identifier list * Glob_term.cases_pattern list * + Pp.loc * Names.identifier list * Glob_term.cases_pattern list * Glob_term.glob_constr -> - Util.loc * Names.identifier list * Glob_term.cases_pattern list * + Pp.loc * Names.identifier list * Glob_term.cases_pattern list * Glob_term.glob_constr diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 97a49d6f0..449dcd20e 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -1,3 +1,4 @@ +open Errors open Util open Names open Term diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli index e65b58086..faa5f2e46 100644 --- a/plugins/funind/indfun.mli +++ b/plugins/funind/indfun.mli @@ -1,3 +1,4 @@ +open Errors open Util open Names open Term @@ -17,7 +18,7 @@ val functional_induction : bool -> Term.constr -> (Term.constr * Term.constr Glob_term.bindings) option -> - Genarg.intro_pattern_expr Util.located option -> + Genarg.intro_pattern_expr Pp.located option -> Proof_type.goal Tacmach.sigma -> Proof_type.goal list Evd.sigma diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index d6fb28ba5..60aa99b12 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -54,7 +54,7 @@ let locate_with_msg msg f x = try f x with - | Not_found -> raise (Util.UserError("", msg)) + | Not_found -> raise (Errors.UserError("", msg)) | e -> raise e @@ -79,7 +79,7 @@ let chop_rlambda_n = | Glob_term.GLambda(_,name,k,t,b) -> chop_lambda_n ((name,t,false)::acc) (n-1) b | Glob_term.GLetIn(_,name,v,b) -> chop_lambda_n ((name,v,true)::acc) (n-1) b | _ -> - raise (Util.UserError("chop_rlambda_n", + raise (Errors.UserError("chop_rlambda_n", str "chop_rlambda_n: Not enough Lambdas")) in chop_lambda_n [] @@ -91,7 +91,7 @@ let chop_rprod_n = else match rt with | Glob_term.GProd(_,name,k,t,b) -> chop_prod_n ((name,t)::acc) (n-1) b - | _ -> raise (Util.UserError("chop_rprod_n",str "chop_rprod_n: Not enough products")) + | _ -> raise (Errors.UserError("chop_rprod_n",str "chop_rprod_n: Not enough products")) in chop_prod_n [] @@ -112,10 +112,10 @@ let list_add_set_eq eq_fun x l = let const_of_id id = let _,princ_ref = - qualid_of_reference (Libnames.Ident (Util.dummy_loc,id)) + qualid_of_reference (Libnames.Ident (Pp.dummy_loc,id)) in try Nametab.locate_constant princ_ref - with Not_found -> Util.error ("cannot find "^ string_of_id id) + with Not_found -> Errors.error ("cannot find "^ string_of_id id) let def_of_const t = match (Term.kind_of_term t) with @@ -361,7 +361,7 @@ let pr_info f_info = let pr_table tb = let l = Cmap.fold (fun k v acc -> v::acc) tb [] in - Util.prlist_with_sep fnl pr_info l + Pp.prlist_with_sep fnl pr_info l let in_Function : function_info -> Libobject.obj = Libobject.declare_object @@ -397,7 +397,7 @@ let _ = let find_or_none id = try Some - (match Nametab.locate (qualid_of_ident id) with ConstRef c -> c | _ -> Util.anomaly "Not a constant" + (match Nametab.locate (qualid_of_ident id) with ConstRef c -> c | _ -> Errors.anomaly "Not a constant" ) with Not_found -> None @@ -425,7 +425,7 @@ let add_Function is_general f = and prop_lemma = find_or_none (Nameops.add_suffix f_id "_ind") and graph_ind = match Nametab.locate (qualid_of_ident (mk_rel_id f_id)) - with | IndRef ind -> ind | _ -> Util.anomaly "Not an inductive" + with | IndRef ind -> ind | _ -> Errors.anomaly "Not an inductive" in let finfos = { function_constant = f; diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 9835ad605..a9b162819 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -7,6 +7,7 @@ (************************************************************************) open Tacexpr open Declarations +open Errors open Util open Names open Term @@ -29,10 +30,10 @@ let pr_binding prc = let pr_bindings prc prlc = function | Glob_term.ImplicitBindings l -> brk (1,1) ++ str "with" ++ brk (1,1) ++ - Util.prlist_with_sep spc prc l + pr_sequence prc l | Glob_term.ExplicitBindings l -> brk (1,1) ++ str "with" ++ brk (1,1) ++ - Util.prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l + pr_sequence (fun b -> str"(" ++ pr_binding prlc b ++ str")") l | Glob_term.NoBindings -> mt () @@ -1142,7 +1143,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g mk_correct_id f_id in - ignore(try Vernacentries.vernac_reset_name (Util.dummy_loc,first_lemma_id) with _ -> ()); + ignore(try Vernacentries.vernac_reset_name (Pp.dummy_loc,first_lemma_id) with _ -> ()); raise e @@ -1239,7 +1240,7 @@ let invfun qhyp f = let f = match f with | ConstRef f -> f - | _ -> raise (Util.UserError("",str "Not a function")) + | _ -> raise (Errors.UserError("",str "Not a function")) in try let finfos = find_Function_infos f in diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 4eedf8dc2..3b3f3057b 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -11,6 +11,7 @@ open Libnames open Tactics open Indfun_common +open Errors open Util open Topconstr open Vernacexpr diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 5e0aac4c2..c37de6e4a 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -17,6 +17,7 @@ open Pp open Names open Libnames open Nameops +open Errors open Util open Closure open RedFlags @@ -1273,7 +1274,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_ let sign = initialize_named_context_for_proof () in let na = next_global_ident_away name [] in if Termops.occur_existential gls_type then - Util.error "\"abstract\" cannot handle existentials"; + Errors.error "\"abstract\" cannot handle existentials"; let hook _ _ = let opacity = let na_ref = Libnames.Ident (dummy_loc,na) in @@ -1553,7 +1554,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num hook with e -> begin - ignore(try Vernacentries.vernac_reset_name (Util.dummy_loc,functional_id) with _ -> ()); + ignore(try Vernacentries.vernac_reset_name (Pp.dummy_loc,functional_id) with _ -> ()); (* anomaly "Cannot create termination Lemma" *) raise e end diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4 index 3b6b69879..9deeb6066 100644 --- a/plugins/micromega/g_micromega.ml4 +++ b/plugins/micromega/g_micromega.ml4 @@ -20,7 +20,7 @@ open Quote open Ring open Mutils open Glob_term -open Util +open Errors let out_arg = function | ArgVar _ -> anomaly "Unevaluated or_var variable" diff --git a/plugins/nsatz/nsatz.ml4 b/plugins/nsatz/nsatz.ml4 index a317307e0..c6d23afa6 100644 --- a/plugins/nsatz/nsatz.ml4 +++ b/plugins/nsatz/nsatz.ml4 @@ -9,6 +9,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) open Pp +open Errors open Util open Names open Term diff --git a/plugins/nsatz/polynom.ml b/plugins/nsatz/polynom.ml index 45fcb2d25..b940ab89d 100644 --- a/plugins/nsatz/polynom.ml +++ b/plugins/nsatz/polynom.ml @@ -8,6 +8,7 @@ (* Recursive polynomials: R[x1]...[xn]. *) open Utile +open Errors open Util (* 1. Coefficients: R *) diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index d7dfe1491..1057c646f 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -13,6 +13,7 @@ (* *) (**************************************************************************) +open Errors open Util open Pp open Reduction diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4 index 84cc8464f..4aad8e738 100644 --- a/plugins/omega/g_omega.ml4 +++ b/plugins/omega/g_omega.ml4 @@ -25,7 +25,7 @@ let omega_tactic l = | "positive" -> Tacinterp.interp <:tactic<zify_positive>> | "N" -> Tacinterp.interp <:tactic<zify_N>> | "Z" -> Tacinterp.interp <:tactic<zify_op>> - | s -> Util.error ("No Omega knowledge base for type "^s)) + | s -> Errors.error ("No Omega knowledge base for type "^s)) (Util.list_uniquize (List.sort compare l)) in tclTHEN diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4 index 1f4ea97fd..4b3385677 100644 --- a/plugins/quote/g_quote.ml4 +++ b/plugins/quote/g_quote.ml4 @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -open Util +open Pp open Tacexpr open Quote diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index fbb754204..fe025e6da 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -102,6 +102,7 @@ (*i*) open Pp +open Errors open Util open Names open Term diff --git a/plugins/ring/ring.ml b/plugins/ring/ring.ml index 98d6361c0..b3151f26c 100644 --- a/plugins/ring/ring.ml +++ b/plugins/ring/ring.ml @@ -9,6 +9,7 @@ (* ML part of the Ring tactic *) open Pp +open Errors open Util open Flags open Term diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml index e810e15c1..298b24850 100644 --- a/plugins/romega/const_omega.ml +++ b/plugins/romega/const_omega.ml @@ -39,7 +39,7 @@ let destructurate t = | Term.Var id,[] -> Kvar(Names.string_of_id id) | Term.Prod (Names.Anonymous,typ,body), [] -> Kimp(typ,body) | Term.Prod (Names.Name _,_,_),[] -> - Util.error "Omega: Not a quantifier-free goal" + Errors.error "Omega: Not a quantifier-free goal" | _ -> Kufo exception Destruct diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4 index 2db86e005..87e42354b 100644 --- a/plugins/romega/g_romega.ml4 +++ b/plugins/romega/g_romega.ml4 @@ -18,7 +18,7 @@ let romega_tactic l = | "positive" -> Tacinterp.interp <:tactic<zify_positive>> | "N" -> Tacinterp.interp <:tactic<zify_N>> | "Z" -> Tacinterp.interp <:tactic<zify_op>> - | s -> Util.error ("No ROmega knowledge base for type "^s)) + | s -> Errors.error ("No ROmega knowledge base for type "^s)) (Util.list_uniquize (List.sort compare l)) in tclTHEN diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml index 4a6d462ec..550a4af2b 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -6,6 +6,7 @@ *************************************************************************) +open Errors open Util open Const_omega module OmegaSolver = Omega.MakeOmegaSolver (Bigint) @@ -450,7 +451,7 @@ let rec scalar n = function | Omult(t1,Oint x) -> do_list [Lazy.force coq_c_mult_assoc_reduced], Omult(t1,Oint (n*x)) | Omult(t1,t2) -> - Util.error "Omega: Can't solve a goal with non-linear products" + Errors.error "Omega: Can't solve a goal with non-linear products" | (Oatom _ as t) -> do_list [], Omult(t,Oint n) | Oint i -> do_list [Lazy.force coq_c_reduce],Oint(n*i) | (Oufo _ as t)-> do_list [], Oufo (Omult(t,Oint n)) @@ -469,7 +470,7 @@ let rec negate = function | Omult(t1,Oint x) -> do_list [Lazy.force coq_c_opp_mult_r], Omult(t1,Oint (Bigint.neg x)) | Omult(t1,t2) -> - Util.error "Omega: Can't solve a goal with non-linear products" + Errors.error "Omega: Can't solve a goal with non-linear products" | (Oatom _ as t) -> do_list [Lazy.force coq_c_opp_one], Omult(t,Oint(negone)) | Oint i -> do_list [Lazy.force coq_c_reduce] ,Oint(Bigint.neg i) @@ -541,7 +542,7 @@ let shrink_pair f1 f2 = Lazy.force coq_c_red4, Omult(Oatom v,Oplus(c1,c2)) | t1,t2 -> oprint stdout t1; print_newline (); oprint stdout t2; print_newline (); - flush Pervasives.stdout; Util.error "shrink.1" + flush Pervasives.stdout; Errors.error "shrink.1" end (* \subsection{Calcul d'une sous formule constante} *) @@ -555,9 +556,9 @@ let reduce_factor = function let rec compute = function Oint n -> n | Oplus(t1,t2) -> compute t1 + compute t2 - | _ -> Util.error "condense.1" in + | _ -> Errors.error "condense.1" in [Lazy.force coq_c_reduce], Omult(Oatom v,Oint(compute c)) - | t -> Util.error "reduce_factor.1" + | t -> Errors.error "reduce_factor.1" (* \subsection{Réordonnancement} *) @@ -1291,7 +1292,7 @@ let total_reflexive_omega_tactic gl = let systems_list = destructurate_hyps full_reified_goal in if !debug then display_systems systems_list; resolution env full_reified_goal systems_list gl - with NO_CONTRADICTION -> Util.error "ROmega can't solve this system" + with NO_CONTRADICTION -> Errors.error "ROmega can't solve this system" (*i let tester = Tacmach.hide_atomic_tactic "TestOmega" test_tactic i*) diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml index d773b1535..2448a2d39 100644 --- a/plugins/rtauto/proof_search.ml +++ b/plugins/rtauto/proof_search.ml @@ -7,6 +7,7 @@ (************************************************************************) open Term +open Errors open Util open Goptions diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index 4a9a0e47f..60ef81286 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -8,6 +8,7 @@ module Search = Explore.Make(Proof_search) +open Errors open Util open Term open Names diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index 9d61c06de..e834650ac 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -9,6 +9,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) open Pp +open Errors open Util open Names open Term diff --git a/plugins/subtac/eterm.ml b/plugins/subtac/eterm.ml index f4d8b769c..0bde8dca9 100644 --- a/plugins/subtac/eterm.ml +++ b/plugins/subtac/eterm.ml @@ -11,6 +11,7 @@ open Names open Evd open List open Pp +open Errors open Util open Subtac_utils open Proof_type diff --git a/plugins/subtac/eterm.mli b/plugins/subtac/eterm.mli index 03d76f29a..4812fe0a6 100644 --- a/plugins/subtac/eterm.mli +++ b/plugins/subtac/eterm.mli @@ -11,6 +11,7 @@ open Tacmach open Term open Evd open Names +open Pp open Util open Tacinterp diff --git a/plugins/subtac/g_subtac.ml4 b/plugins/subtac/g_subtac.ml4 index c37f0db5a..27de89f67 100644 --- a/plugins/subtac/g_subtac.ml4 +++ b/plugins/subtac/g_subtac.ml4 @@ -14,7 +14,8 @@ open Flags -open Util +open Errors +open Pp open Names open Nameops open Vernacentries diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml index 710149ae4..cccb12e41 100644 --- a/plugins/subtac/subtac.ml +++ b/plugins/subtac/subtac.ml @@ -9,6 +9,7 @@ open Compat open Global open Pp +open Errors open Util open Names open Sign diff --git a/plugins/subtac/subtac.mli b/plugins/subtac/subtac.mli index b51150aa0..32d484091 100644 --- a/plugins/subtac/subtac.mli +++ b/plugins/subtac/subtac.mli @@ -1,2 +1,2 @@ val require_library : string -> unit -val subtac : Util.loc * Vernacexpr.vernac_expr -> unit +val subtac : Pp.loc * Vernacexpr.vernac_expr -> unit diff --git a/plugins/subtac/subtac_cases.ml b/plugins/subtac/subtac_cases.ml index 16d4e21ee..d60841e72 100644 --- a/plugins/subtac/subtac_cases.ml +++ b/plugins/subtac/subtac_cases.ml @@ -7,6 +7,7 @@ (************************************************************************) open Cases +open Errors open Util open Names open Nameops diff --git a/plugins/subtac/subtac_cases.mli b/plugins/subtac/subtac_cases.mli index 77537d33a..11a811597 100644 --- a/plugins/subtac/subtac_cases.mli +++ b/plugins/subtac/subtac_cases.mli @@ -7,6 +7,7 @@ (************************************************************************) (*i*) +open Errors open Util open Names open Term diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml index cac0988c0..a81243f73 100644 --- a/plugins/subtac/subtac_classes.ml +++ b/plugins/subtac/subtac_classes.ml @@ -22,6 +22,7 @@ open Typeclasses open Typeclasses_errors open Decl_kinds open Entries +open Errors open Util module SPretyping = Subtac_pretyping.Pretyping @@ -71,8 +72,8 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p let t = if b then let _k = class_info cl in - CHole (Util.dummy_loc, Some Evd.InternalHole) - else CHole (Util.dummy_loc, None) + CHole (Pp.dummy_loc, Some Evd.InternalHole) + else CHole (Pp.dummy_loc, None) in t, avoid | None -> failwith ("new instance: under-applied typeclass")) cl @@ -149,7 +150,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p k.cl_projs; c :: props, rest' with Not_found -> - (CHole (Util.dummy_loc, None) :: props), rest + (CHole (Pp.dummy_loc, None) :: props), rest else props, rest) ([], props) k.cl_props in diff --git a/plugins/subtac/subtac_classes.mli b/plugins/subtac/subtac_classes.mli index 5b5c02037..5b8636a12 100644 --- a/plugins/subtac/subtac_classes.mli +++ b/plugins/subtac/subtac_classes.mli @@ -16,6 +16,7 @@ open Environ open Nametab open Mod_subst open Topconstr +open Errors open Util open Typeclasses open Implicit_quantifiers diff --git a/plugins/subtac/subtac_coercion.ml b/plugins/subtac/subtac_coercion.ml index eb29bd045..3cbf9fcab 100644 --- a/plugins/subtac/subtac_coercion.ml +++ b/plugins/subtac/subtac_coercion.ml @@ -5,6 +5,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Names open Term diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml index ecae6759f..e5d93ace2 100644 --- a/plugins/subtac/subtac_command.ml +++ b/plugins/subtac/subtac_command.ml @@ -9,6 +9,7 @@ open Pp open Glob_term open Sign open Tacred +open Errors open Util open Names open Nameops diff --git a/plugins/subtac/subtac_errors.ml b/plugins/subtac/subtac_errors.ml index 067da150e..f07bbeb43 100644 --- a/plugins/subtac/subtac_errors.ml +++ b/plugins/subtac/subtac_errors.ml @@ -1,3 +1,4 @@ +open Errors open Util open Pp open Printer diff --git a/plugins/subtac/subtac_errors.mli b/plugins/subtac/subtac_errors.mli index 8d75b9c01..c65203075 100644 --- a/plugins/subtac/subtac_errors.mli +++ b/plugins/subtac/subtac_errors.mli @@ -1,13 +1,13 @@ type term_pp = Pp.std_ppcmds type subtyping_error = - UncoercibleInferType of Util.loc * term_pp * term_pp - | UncoercibleInferTerm of Util.loc * term_pp * term_pp * term_pp * term_pp + UncoercibleInferType of Pp.loc * term_pp * term_pp + | UncoercibleInferTerm of Pp.loc * term_pp * term_pp * term_pp * term_pp | UncoercibleRewrite of term_pp * term_pp type typing_error = - NonFunctionalApp of Util.loc * term_pp * term_pp * term_pp - | NonConvertible of Util.loc * term_pp * term_pp - | NonSigma of Util.loc * term_pp - | IllSorted of Util.loc * term_pp + NonFunctionalApp of Pp.loc * term_pp * term_pp * term_pp + | NonConvertible of Pp.loc * term_pp * term_pp + | NonSigma of Pp.loc * term_pp + | IllSorted of Pp.loc * term_pp exception Subtyping_error of subtyping_error exception Typing_error of typing_error exception Debug_msg of string diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml index 6a5878b3e..527c5e084 100644 --- a/plugins/subtac/subtac_obligations.ml +++ b/plugins/subtac/subtac_obligations.ml @@ -11,6 +11,7 @@ open Summary open Libobject open Entries open Decl_kinds +open Errors open Util open Evd open Declare @@ -18,7 +19,7 @@ open Proof_type open Compat let ppwarn cmd = Pp.warn (str"Program:" ++ cmd) -let pperror cmd = Util.errorlabstrm "Program" cmd +let pperror cmd = Errors.errorlabstrm "Program" cmd let error s = pperror (str s) let reduce c = @@ -551,7 +552,7 @@ and solve_obligation_by_tac prg obls i tac = | Loc.Exc_located(_, Refiner.FailError (_, s)) | Refiner.FailError (_, s) -> user_err_loc (fst obl.obl_location, "solve_obligation", Lazy.force s) - | Util.Anomaly _ as e -> raise e + | Errors.Anomaly _ as e -> raise e | e -> false and solve_prg_obligations prg ?oblset tac = diff --git a/plugins/subtac/subtac_obligations.mli b/plugins/subtac/subtac_obligations.mli index c1d665aac..284e975db 100644 --- a/plugins/subtac/subtac_obligations.mli +++ b/plugins/subtac/subtac_obligations.mli @@ -1,4 +1,5 @@ open Names +open Pp open Util open Libnames open Evd diff --git a/plugins/subtac/subtac_pretyping.ml b/plugins/subtac/subtac_pretyping.ml index 7c0d12325..c8acf7e0b 100644 --- a/plugins/subtac/subtac_pretyping.ml +++ b/plugins/subtac/subtac_pretyping.ml @@ -8,6 +8,7 @@ open Global open Pp +open Errors open Util open Names open Sign diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml index 528a2e683..fbeed381d 100644 --- a/plugins/subtac/subtac_pretyping_F.ml +++ b/plugins/subtac/subtac_pretyping_F.ml @@ -8,6 +8,7 @@ open Pp open Compat +open Errors open Util open Names open Sign diff --git a/plugins/subtac/subtac_utils.ml b/plugins/subtac/subtac_utils.ml index 28bbdd35e..0ed78a23b 100644 --- a/plugins/subtac/subtac_utils.ml +++ b/plugins/subtac/subtac_utils.ml @@ -5,6 +5,8 @@ open Libnames open Coqlib open Term open Names +open Errors +open Pp open Util let ($) f x = f x @@ -426,7 +428,7 @@ let pr_meta_map evd = in prlist pr_meta_binding ml -let pr_idl idl = prlist_with_sep pr_spc pr_id idl +let pr_idl idl = pr_sequence pr_id idl let pr_evar_info evi = let phyps = @@ -443,14 +445,14 @@ let pr_evar_info evi = let pr_evar_map sigma = h 0 - (prlist_with_sep pr_fnl + (prlist_with_sep fnl (fun (ev,evi) -> h 0 (str(string_of_existential ev)++str"=="++ pr_evar_info evi)) (to_list sigma)) let pr_constraints pbs = h 0 - (prlist_with_sep pr_fnl (fun (pbty,t1,t2) -> + (prlist_with_sep fnl (fun (pbty,t1,t2) -> Termops.print_constr t1 ++ spc() ++ str (match pbty with | Reduction.CONV -> "==" diff --git a/plugins/subtac/subtac_utils.mli b/plugins/subtac/subtac_utils.mli index de96cc602..70ad0bcc8 100644 --- a/plugins/subtac/subtac_utils.mli +++ b/plugins/subtac/subtac_utils.mli @@ -7,6 +7,7 @@ open Evd open Decl_kinds open Topconstr open Glob_term +open Errors open Util open Evarutil open Names diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml index bd2285bb3..cf51af134 100644 --- a/plugins/syntax/ascii_syntax.ml +++ b/plugins/syntax/ascii_syntax.ml @@ -7,6 +7,7 @@ (***********************************************************************) open Pp +open Errors open Util open Names open Pcoq diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml index 446ae5225..5a355b971 100644 --- a/plugins/syntax/nat_syntax.ml +++ b/plugins/syntax/nat_syntax.ml @@ -11,6 +11,7 @@ (*i*) open Pcoq open Pp +open Errors open Util open Names open Coqlib @@ -20,6 +21,7 @@ open Bigint open Coqlib open Notation open Pp +open Errors open Util open Names (*i*) diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml index 19a3c899f..cbc8d7fd6 100644 --- a/plugins/syntax/numbers_syntax.ml +++ b/plugins/syntax/numbers_syntax.ml @@ -111,7 +111,7 @@ let int31_of_pos_bigint dloc n = GApp (dloc, ref_construct, List.rev (args 31 n)) let error_negative dloc = - Util.user_err_loc (dloc, "interp_int31", Pp.str "int31 are only non-negative numbers.") + Errors.user_err_loc (dloc, "interp_int31", Pp.str "int31 are only non-negative numbers.") let interp_int31 dloc n = if is_pos_or_zero n then @@ -143,7 +143,7 @@ let uninterp_int31 i = let _ = Notation.declare_numeral_interpreter int31_scope (int31_path, int31_module) interp_int31 - ([GRef (Util.dummy_loc, int31_construct)], + ([GRef (Pp.dummy_loc, int31_construct)], uninterp_int31, true) @@ -201,7 +201,7 @@ let bigN_of_pos_bigint dloc n = result hght (word_of_pos_bigint dloc hght n) let bigN_error_negative dloc = - Util.user_err_loc (dloc, "interp_bigN", Pp.str "bigN are only non-negative numbers.") + Errors.user_err_loc (dloc, "interp_bigN", Pp.str "bigN are only non-negative numbers.") let interp_bigN dloc n = if is_pos_or_zero n then @@ -257,7 +257,7 @@ let uninterp_bigN rc = let bigN_list_of_constructors = let rec build i = if less_than i (add_1 n_inlined) then - GRef (Util.dummy_loc, bigN_constructor i)::(build (add_1 i)) + GRef (Pp.dummy_loc, bigN_constructor i)::(build (add_1 i)) else [] in @@ -303,8 +303,8 @@ let uninterp_bigZ rc = let _ = Notation.declare_numeral_interpreter bigZ_scope (bigZ_path, bigZ_module) interp_bigZ - ([GRef (Util.dummy_loc, bigZ_pos); - GRef (Util.dummy_loc, bigZ_neg)], + ([GRef (Pp.dummy_loc, bigZ_pos); + GRef (Pp.dummy_loc, bigZ_neg)], uninterp_bigZ, true) @@ -324,5 +324,5 @@ let uninterp_bigQ rc = let _ = Notation.declare_numeral_interpreter bigQ_scope (bigQ_path, bigQ_module) interp_bigQ - ([GRef (Util.dummy_loc, bigQ_z)], uninterp_bigQ, + ([GRef (Pp.dummy_loc, bigQ_z)], uninterp_bigQ, true) diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml index b9c0bcd6f..b3195f281 100644 --- a/plugins/syntax/r_syntax.ml +++ b/plugins/syntax/r_syntax.ml @@ -7,6 +7,7 @@ (************************************************************************) open Pp +open Errors open Util open Names open Pcoq diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml index d670f6026..640806d87 100644 --- a/plugins/syntax/string_syntax.ml +++ b/plugins/syntax/string_syntax.ml @@ -7,6 +7,7 @@ (***********************************************************************) open Pp +open Errors open Util open Names open Pcoq diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml index f8bce8f79..450d57969 100644 --- a/plugins/syntax/z_syntax.ml +++ b/plugins/syntax/z_syntax.ml @@ -8,6 +8,7 @@ open Pcoq open Pp +open Errors open Util open Names open Topconstr diff --git a/plugins/xml/acic2Xml.ml4 b/plugins/xml/acic2Xml.ml4 index 97f7e2bd4..75bc84074 100644 --- a/plugins/xml/acic2Xml.ml4 +++ b/plugins/xml/acic2Xml.ml4 @@ -21,7 +21,7 @@ let typesdtdname = "http://mowgli.cs.unibo.it/dtd/cictypes.dtd";; let rec find_last_id = function - [] -> Util.anomaly "find_last_id: empty list" + [] -> Errors.anomaly "find_last_id: empty list" | [id,_,_] -> id | _::tl -> find_last_id tl ;; diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml index da0a65ff5..78a402898 100644 --- a/plugins/xml/cic2acic.ml +++ b/plugins/xml/cic2acic.ml @@ -59,7 +59,7 @@ let get_uri_of_var v pvars = let module N = Names in let rec search_in_open_sections = function - [] -> Util.error ("Variable "^v^" not found") + [] -> Errors.error ("Variable "^v^" not found") | he::tl as modules -> let dirpath = N.make_dirpath modules in if List.mem (N.id_of_string v) (D.last_section_hyps dirpath) then @@ -162,7 +162,7 @@ let family_of_term ty = match Term.kind_of_term ty with Term.Sort s -> Coq_sort (Term.family_of_sort s) | Term.Const _ -> CProp (* I could check that the constant is CProp *) - | _ -> Util.anomaly "family_of_term" + | _ -> Errors.anomaly "family_of_term" ;; module CPropRetyping = @@ -177,7 +177,7 @@ module CPropRetyping = | h::rest -> match T.kind_of_term (DoubleTypeInference.whd_betadeltaiotacprop env sigma typ) with | T.Prod (na,c1,c2) -> subst_type env sigma (T.subst1 h c2) rest - | _ -> Util.anomaly "Non-functional construction" + | _ -> Errors.anomaly "Non-functional construction" let sort_of_atomic_type env sigma ft args = @@ -193,7 +193,7 @@ let typeur sigma metamap = match Term.kind_of_term cstr with | T.Meta n -> (try T.strip_outer_cast (List.assoc n metamap) - with Not_found -> Util.anomaly "type_of: this is not a well-typed term") + with Not_found -> Errors.anomaly "type_of: this is not a well-typed term") | T.Rel n -> let (_,_,ty) = Environ.lookup_rel n env in T.lift n ty @@ -202,7 +202,7 @@ let typeur sigma metamap = let (_,_,ty) = Environ.lookup_named id env in ty with Not_found -> - Util.anomaly ("type_of: variable "^(Names.string_of_id id)^" unbound")) + Errors.anomaly ("type_of: variable "^(Names.string_of_id id)^" unbound")) | T.Const c -> let cb = Environ.lookup_constant c env in Typeops.type_of_constant_type env (cb.Declarations.const_type) @@ -212,7 +212,7 @@ let typeur sigma metamap = | T.Case (_,p,c,lf) -> let Inductiveops.IndType(_,realargs) = try Inductiveops.find_rectype env sigma (type_of env c) - with Not_found -> Util.anomaly "type_of: Bad recursive type" in + with Not_found -> Errors.anomaly "type_of: Bad recursive type" in let t = Reductionops.whd_beta sigma (T.applist (p, realargs)) in (match Term.kind_of_term (DoubleTypeInference.whd_betadeltaiotacprop env sigma (type_of env t)) with | T.Prod _ -> Reductionops.whd_beta sigma (T.applist (t, [c])) @@ -253,7 +253,7 @@ let typeur sigma metamap = | _, (CProp as s) -> s) | T.App(f,args) -> sort_of_atomic_type env sigma (type_of env f) args | T.Lambda _ | T.Fix _ | T.Construct _ -> - Util.anomaly "sort_of: Not a type (1)" + Errors.anomaly "sort_of: Not a type (1)" | _ -> outsort env sigma (type_of env t) and sort_family_of env t = @@ -265,7 +265,7 @@ let typeur sigma metamap = | T.App(f,args) -> sort_of_atomic_type env sigma (type_of env f) args | T.Lambda _ | T.Fix _ | T.Construct _ -> - Util.anomaly "sort_of: Not a type (1)" + Errors.anomaly "sort_of: Not a type (1)" | _ -> outsort env sigma (type_of env t) in type_of, sort_of, sort_family_of @@ -523,7 +523,7 @@ print_endline "PASSATO" ; flush stdout ; add_inner_type fresh_id'' ; A.AEvar (fresh_id'', n, Array.to_list (Array.map (aux' env idrefs) l)) - | T.Meta _ -> Util.anomaly "Meta met during exporting to XML" + | T.Meta _ -> Errors.anomaly "Meta met during exporting to XML" | T.Sort s -> A.ASort (fresh_id'', s) | T.Cast (v,_, t) -> Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; @@ -737,7 +737,7 @@ print_endline "PASSATO" ; flush stdout ; let ids = ref (Termops.ids_of_context env) in Array.map (function - N.Anonymous -> Util.error "Anonymous fix function met" + N.Anonymous -> Errors.error "Anonymous fix function met" | N.Name id as n -> let res = N.Name (Namegen.next_name_away n !ids) in ids := id::!ids ; @@ -750,7 +750,7 @@ print_endline "PASSATO" ; flush stdout ; let fi' = match fi with N.Name fi -> fi - | N.Anonymous -> Util.error "Anonymous fix function met" + | N.Anonymous -> Errors.error "Anonymous fix function met" in (id, fi', ai, aux' env idrefs ti, @@ -771,7 +771,7 @@ print_endline "PASSATO" ; flush stdout ; let ids = ref (Termops.ids_of_context env) in Array.map (function - N.Anonymous -> Util.error "Anonymous fix function met" + N.Anonymous -> Errors.error "Anonymous fix function met" | N.Name id as n -> let res = N.Name (Namegen.next_name_away n !ids) in ids := id::!ids ; @@ -784,7 +784,7 @@ print_endline "PASSATO" ; flush stdout ; let fi' = match fi with N.Name fi -> fi - | N.Anonymous -> Util.error "Anonymous fix function met" + | N.Anonymous -> Errors.error "Anonymous fix function met" in (id, fi', aux' env idrefs ti, diff --git a/plugins/xml/doubleTypeInference.ml b/plugins/xml/doubleTypeInference.ml index a21a919ad..30cd5c18b 100644 --- a/plugins/xml/doubleTypeInference.ml +++ b/plugins/xml/doubleTypeInference.ml @@ -67,7 +67,7 @@ let double_type_of env sigma cstr expectedty subterms_to_types = let judgement = match T.kind_of_term cstr with T.Meta n -> - Util.error + Errors.error "DoubleTypeInference.double_type_of: found a non-instanciated goal" | T.Evar ((n,l) as ev) -> diff --git a/plugins/xml/dumptree.ml4 b/plugins/xml/dumptree.ml4 index 3c3e54fa3..69b9e6ea7 100644 --- a/plugins/xml/dumptree.ml4 +++ b/plugins/xml/dumptree.ml4 @@ -128,7 +128,7 @@ let pr_goal_xml sigma g = ;; let print_proof_xml () = - Util.anomaly "Dump Tree command not supported in this version." + Errors.anomaly "Dump Tree command not supported in this version." VERNAC COMMAND EXTEND DumpTree diff --git a/plugins/xml/proofTree2Xml.ml4 b/plugins/xml/proofTree2Xml.ml4 index 2f5eb6ac2..21058a7b9 100644 --- a/plugins/xml/proofTree2Xml.ml4 +++ b/plugins/xml/proofTree2Xml.ml4 @@ -53,7 +53,7 @@ let constr_to_xml obj sigma env = in Acic2Xml.print_term ids_to_inner_sorts annobj with e -> - Util.anomaly + Errors.anomaly ("Problem during the conversion of constr into XML: " ^ Printexc.to_string e) (* CSC: debugging stuff diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml index 1037bbf08..13821488a 100644 --- a/plugins/xml/xmlcommand.ml +++ b/plugins/xml/xmlcommand.ml @@ -424,7 +424,7 @@ let kind_of_variable id = | DK.IsAssumption DK.Conjectural -> "VARIABLE","Conjecture" | DK.IsDefinition DK.Definition -> "VARIABLE","LocalDefinition" | DK.IsProof _ -> "VARIABLE","LocalFact" - | _ -> Util.anomaly "Unsupported variable kind" + | _ -> Errors.anomaly "Unsupported variable kind" ;; let kind_of_constant kn = @@ -541,7 +541,7 @@ let print internal glob_ref kind xml_library_root = D.mind_finite=finite} = mib in Cic2acic.Inductive kn,mk_inductive_obj kn mib packs variables nparams hyps finite | Ln.ConstructRef _ -> - Util.error ("a single constructor cannot be printed in XML") + Errors.error ("a single constructor cannot be printed in XML") in let fn = filename_of_path xml_library_root tag in let uri = Cic2acic.uri_of_kernel_name tag in @@ -560,7 +560,7 @@ let print_ref qid fn = (* pretty prints via Xml.pp the proof in progress on dest *) let show_pftreestate internal fn (kind,pftst) id = if true then - Util.anomaly "Xmlcommand.show_pftreestate is not supported in this version." + Errors.anomaly "Xmlcommand.show_pftreestate is not supported in this version." let show fn = let pftst = Pfedit.get_pftreestate () in @@ -656,7 +656,7 @@ let _ = let options = " --html -s --body-only --no-index --latin1 --raw-comments" in let command cmd = if Sys.command cmd <> 0 then - Util.anomaly ("Error executing \"" ^ cmd ^ "\"") + Errors.anomaly ("Error executing \"" ^ cmd ^ "\"") in command (coqdoc^options^" -o "^fn^".xml "^fn^".v"); command ("rm "^fn^".v "^fn^".glob"); diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml index 5e2284e13..54ffcd653 100644 --- a/pretyping/arguments_renaming.ml +++ b/pretyping/arguments_renaming.ml @@ -16,6 +16,7 @@ open Evd open Environ open Nametab open Mod_subst +open Errors open Util open Pp open Libobject diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 3f5b3f1bf..d413bfbcd 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -7,6 +7,8 @@ (************************************************************************) open Compat +open Pp +open Errors open Util open Names open Nameops diff --git a/pretyping/cases.mli b/pretyping/cases.mli index f773da0ee..fcfee055c 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -6,7 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Util +open Errors +open Pp open Names open Term open Evd diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index ad33bae1f..95ab968f0 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Pp open Term diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 62d774bd7..3be7e7862 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Pp open Flags @@ -273,7 +274,7 @@ let print_path x = !path_printer x let message_ambig l = (str"Ambiguous paths:" ++ spc () ++ - prlist_with_sep pr_fnl (fun ijp -> print_path ijp) l) + prlist_with_sep fnl (fun ijp -> print_path ijp) l) (* add_coercion_in_graph : coe_index * cl_index * cl_index -> unit coercion,source,target *) diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 553c91274..0c340f9ed 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -14,6 +14,8 @@ Corbineau, Feb 2008 *) (* Turned into an abstract compilation unit by Matthieu Sozeau, March 2006 *) +open Pp +open Errors open Util open Names open Term diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli index 5d814b294..f312802a8 100644 --- a/pretyping/coercion.mli +++ b/pretyping/coercion.mli @@ -6,7 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Util +open Errors +open Pp open Evd open Names open Term diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index c194a0f23..b3daad79e 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -7,6 +7,7 @@ (************************************************************************) open Pp +open Errors open Util open Univ open Names diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index 40e3d0f82..0912a3f23 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -6,7 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Util +open Errors +open Pp open Names open Term open Sign diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 04f86e709..8e61cdebb 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -7,6 +7,7 @@ (************************************************************************) open Pp +open Errors open Util open Names open Term diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index fba35925c..5faa86cb0 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Pp open Names diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index 61f503c7d..82205c91f 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors +open Pp open Util open Names open Glob_term diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 5d6ca2cac..b4354d0cc 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -7,6 +7,7 @@ (************************************************************************) open Pp +open Errors open Util open Names open Nameops @@ -761,7 +762,7 @@ let pr_evar_source = function spc () ++ print_constr (constr_of_global c) | InternalHole -> str "internal placeholder" | TomatchTypeParameter (ind,n) -> - nth n ++ str " argument of type " ++ print_constr (mkInd ind) + pr_nth n ++ str " argument of type " ++ print_constr (mkInd ind) | GoalEvar -> str "goal evar" | ImpossibleCase -> str "type of impossible pattern-matching clause" | MatchingVar _ -> str "matching variable" @@ -770,7 +771,7 @@ let pr_evar_info evi = let phyps = try let decls = List.combine (evar_context evi) (evar_filter evi) in - prlist_with_sep pr_spc pr_decl (List.rev decls) + prlist_with_sep spc pr_decl (List.rev decls) with Invalid_argument _ -> str "Ill-formed filtered context" in let pty = print_constr evi.evar_concl in let pb = @@ -810,7 +811,7 @@ let evar_dependency_closure n sigma = let pr_evar_map_t depth sigma = let (evars,(uvs,univs)) = sigma.evars in let pr_evar_list l = - h 0 (prlist_with_sep pr_fnl + h 0 (prlist_with_sep fnl (fun (ev,evi) -> h 0 (str(string_of_existential ev) ++ str"==" ++ pr_evar_info evi)) l) in @@ -830,7 +831,7 @@ let pr_evar_map_t depth sigma = and svs = if Univ.UniverseLSet.is_empty uvs then mt () else str"UNIVERSE VARIABLES:"++brk(0,1)++ - h 0 (prlist_with_sep pr_fnl + h 0 (prlist_with_sep fnl (fun u -> Univ.pr_uni_level u) (Univ.UniverseLSet.elements uvs))++fnl() and cs = if Univ.is_initial_universes univs then mt () @@ -844,12 +845,12 @@ let print_env_short env = let pr_rel_decl (n, b, _) = pr_body n b in let nc = List.rev (named_context env) in let rc = List.rev (rel_context env) in - str "[" ++ prlist_with_sep pr_spc pr_named_decl nc ++ str "]" ++ spc () ++ - str "[" ++ prlist_with_sep pr_spc pr_rel_decl rc ++ str "]" + str "[" ++ pr_sequence pr_named_decl nc ++ str "]" ++ spc () ++ + str "[" ++ pr_sequence pr_rel_decl rc ++ str "]" let pr_constraints pbs = h 0 - (prlist_with_sep pr_fnl + (prlist_with_sep fnl (fun (pbty,env,t1,t2) -> print_env_short env ++ spc () ++ str "|-" ++ spc () ++ print_constr t1 ++ spc() ++ @@ -859,7 +860,7 @@ let pr_constraints pbs = spc() ++ print_constr t2) pbs) let pr_evar_map_constraints evd = - if evd.conv_pbs = [] then mt() + if evd.conv_pbs = [] then mt() else pr_constraints evd.conv_pbs++fnl() let pr_evar_map allevars evd = @@ -874,4 +875,4 @@ let pr_evar_map allevars evd = v 0 (pp_evm ++ cstrs ++ pp_met) let pr_metaset metas = - str "[" ++ prlist_with_sep spc pr_meta (Metaset.elements metas) ++ str "]" + str "[" ++ pr_sequence pr_meta (Metaset.elements metas) ++ str "]" diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 55c54f2c6..5e596e0de 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Pp +open Errors open Util open Names open Term diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml index a736e6eec..5922d38dc 100644 --- a/pretyping/glob_term.ml +++ b/pretyping/glob_term.ml @@ -7,6 +7,8 @@ (************************************************************************) (*i*) +open Errors +open Pp open Util open Names open Sign diff --git a/pretyping/glob_term.mli b/pretyping/glob_term.mli index fcd28eb8f..f13d0bee9 100644 --- a/pretyping/glob_term.mli +++ b/pretyping/glob_term.mli @@ -12,7 +12,8 @@ and notations are done, but coercions, inference of implicit arguments and pattern-matching compilation are not. *) -open Util +open Errors +open Pp open Names open Sign open Term diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index a09760295..f08b7493c 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -11,6 +11,7 @@ (* This file builds various inductive schemes *) open Pp +open Errors open Util open Names open Libnames diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index da316fd63..cd86b1e67 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Names open Univ diff --git a/pretyping/matching.ml b/pretyping/matching.ml index 7a7451187..ac0022c8c 100644 --- a/pretyping/matching.ml +++ b/pretyping/matching.ml @@ -8,6 +8,7 @@ (*i*) open Pp +open Errors open Util open Names open Libnames diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml index abb6b510d..0d086919a 100644 --- a/pretyping/namegen.ml +++ b/pretyping/namegen.ml @@ -12,6 +12,7 @@ (* This file is about generating new or fresh names and dealing with alpha-renaming *) +open Errors open Util open Names open Term diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index 65f342d88..49b63a4b5 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Names open Libnames diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index 2cf167919..409e405f5 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -7,6 +7,7 @@ (************************************************************************) open Compat +open Errors open Util open Names open Sign @@ -43,8 +44,8 @@ type pretype_error = exception PretypeError of env * Evd.evar_map * pretype_error let precatchable_exception = function - | Util.UserError _ | TypeError _ | PretypeError _ - | Loc.Exc_located(_,(Util.UserError _ | TypeError _ | + | Errors.UserError _ | TypeError _ | PretypeError _ + | Loc.Exc_located(_,(Errors.UserError _ | TypeError _ | Nametab.GlobalizationError _ | PretypeError _)) -> true | _ -> false diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index 3a3dccb4b..43f934520 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -7,6 +7,7 @@ (************************************************************************) open Pp +open Errors open Util open Names open Term diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 901936f33..246993f1a 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -23,6 +23,7 @@ open Compat open Pp +open Errors open Util open Names open Sign diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 47b3ec875..cf47d194e 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -23,7 +23,7 @@ open Evarutil (** An auxiliary function for searching for fixpoint guard indexes *) val search_guard : - Util.loc -> env -> int list list -> rec_declaration -> int array + Pp.loc -> env -> int list list -> rec_declaration -> int array type typing_constraint = OfType of types option | IsType diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index b3be7afd9..e35004ef1 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -13,6 +13,7 @@ (* This file registers properties of records: projections and canonical structures *) +open Errors open Util open Pp open Names diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index bdb47d689..4e6a702e7 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -7,6 +7,7 @@ (************************************************************************) open Pp +open Errors open Util open Names open Term diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 502e238b3..5d7c7ec9f 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Term open Inductive diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 0ab43e49c..13b2ddcaa 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -7,6 +7,7 @@ (************************************************************************) open Pp +open Errors open Util open Names open Nameops diff --git a/pretyping/term_dnet.ml b/pretyping/term_dnet.ml index 98091087d..2bf15d2f3 100644 --- a/pretyping/term_dnet.ml +++ b/pretyping/term_dnet.ml @@ -7,6 +7,7 @@ (************************************************************************) (*i*) +open Errors open Util open Term open Sign @@ -304,7 +305,7 @@ struct let rec pr_term_pattern p = (fun pr_t -> function | Term t -> pr_t t - | Meta m -> str"["++Util.pr_int (Obj.magic m)++str"]" + | Meta m -> str"["++Pp.int (Obj.magic m)++str"]" ) (pr_dconstr pr_term_pattern) p let search_pat cpat dpat dn (up,plug) = diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 6371fd3a7..f64625707 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -7,6 +7,7 @@ (************************************************************************) open Pp +open Errors open Util open Names open Nameops diff --git a/pretyping/termops.mli b/pretyping/termops.mli index 5448d97c8..68db293b6 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Pp open Names diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index d8a09f95c..8fe06539c 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -16,6 +16,7 @@ open Evd open Environ open Nametab open Mod_subst +open Errors open Util open Typeclasses_errors open Libobject diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index b49eeac4f..3d36168fd 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -16,6 +16,7 @@ open Environ open Nametab open Mod_subst open Topconstr +open Errors open Util type direction = Forward | Backward diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml index ab7bb9dcb..f6de344a9 100644 --- a/pretyping/typeclasses_errors.ml +++ b/pretyping/typeclasses_errors.ml @@ -17,6 +17,7 @@ open Nametab open Mod_subst open Topconstr open Compat +open Pp open Util open Libnames (*i*) diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli index 79f0678ff..fd709763d 100644 --- a/pretyping/typeclasses_errors.mli +++ b/pretyping/typeclasses_errors.mli @@ -15,7 +15,8 @@ open Environ open Nametab open Mod_subst open Topconstr -open Util +open Errors +open Pp open Libnames type contexts = Parameters | Properties diff --git a/pretyping/typing.ml b/pretyping/typing.ml index efcdff9dc..9c8c3989e 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Names open Term diff --git a/pretyping/unification.ml b/pretyping/unification.ml index e6fa6eecc..48a2c8c42 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -7,6 +7,7 @@ (************************************************************************) open Pp +open Errors open Util open Names open Nameops diff --git a/proofs/clenv.ml b/proofs/clenv.ml index d06c6f2e6..9d2c1c7ab 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -7,6 +7,7 @@ (************************************************************************) open Pp +open Errors open Util open Names open Nameops diff --git a/proofs/clenv.mli b/proofs/clenv.mli index abd67236a..04f532654 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Names open Term diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index eb935d05d..45765805f 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -7,6 +7,7 @@ (************************************************************************) open Pp +open Errors open Util open Names open Nameops diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli index 49a961f5d..a14f261e9 100644 --- a/proofs/clenvtac.mli +++ b/proofs/clenvtac.mli @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Names open Term diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index 36268de1e..c606600d7 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Names open Term diff --git a/proofs/goal.ml b/proofs/goal.ml index d68ab8c55..f0ab31c5b 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -10,7 +10,7 @@ open Pp open Term (* This module implements the abstract interface to goals *) -(* A general invariant of the module, is that a goal whose associated +(* A general invariant of the module, is that a goal whose associated evar is defined in the current evar_map, should not be accessed. *) (* type of the goals *) @@ -47,22 +47,22 @@ let get_by_uid u = for instance. *) build (int_of_string u) -(* Builds a new goal with content evar [e] and +(* Builds a new goal with content evar [e] and inheriting from goal [gl]*) let descendent gl e = { gl with content = e} -(* [advance sigma g] returns [Some g'] if [g'] is undefined and +(* [advance sigma g] returns [Some g'] if [g'] is undefined and is the current avatar of [g] (for instance [g] was changed by [clear] into [g']). It returns [None] if [g] has been (partially) solved. *) open Store.Field let rec advance sigma g = let evi = Evd.find sigma g.content in if Option.default false (Evarutil.cleared.get evi.Evd.evar_extra) then - let v = - match evi.Evd.evar_body with + let v = + match evi.Evd.evar_body with | Evd.Evar_defined c -> c - | _ -> Util.anomaly "Some goal is marked as 'cleared' but is uninstantiated" + | _ -> Errors.anomaly "Some goal is marked as 'cleared' but is uninstantiated" in let (e,_) = Term.destEvar v in let g' = { g with content = e } in @@ -81,10 +81,10 @@ type subgoals = { subgoals: goal list } (* type of the base elements of the goal API.*) (* it has an extra evar_info with respect to what would be expected, it is supposed to be the evar_info of the goal in the evar_map. - The idea is that it is computed by the [run] function as an - optimisation, since it will generaly not change during the + The idea is that it is computed by the [run] function as an + optimisation, since it will generaly not change during the evaluation. *) -type 'a sensitive = +type 'a sensitive = Environ.env -> Evd.evar_map ref -> goal -> Evd.evar_info -> 'a (* evaluates a goal sensitive value in a given goal (knowing the current evar_map). *) @@ -105,7 +105,7 @@ let bind e f env rdefs goal info = let return v _ _ _ _ = v (* interpretation of "open" constr *) -(* spiwack: it is a wrapper around [Constrintern.interp_open_constr]. +(* spiwack: it is a wrapper around [Constrintern.interp_open_constr]. In an ideal world, this could/should be the other way round. As of now, though, it seems at least quite useful to build tactics. *) let interp_constr cexpr env rdefs _ _ = @@ -114,7 +114,7 @@ let interp_constr cexpr env rdefs _ _ = c (* Type of constr with holes used by refine. *) -(* The list of evars doesn't necessarily contain all the evars in the constr, +(* The list of evars doesn't necessarily contain all the evars in the constr, only those the constr has introduced. *) (* The variables in [myevars] are supposed to be stored in decreasing order. Breaking this invariant might cause @@ -129,7 +129,7 @@ module Refinable = struct type handle = Evd.evar list ref - let make t env rdefs gl info = + let make t env rdefs gl info = let r = ref [] in let me = t r env rdefs gl info in { me = me; @@ -144,9 +144,9 @@ module Refinable = struct let (e,_) = Term.destEvar ev in handle := e::!handle; ev - + (* [with_type c typ] constrains term [c] to have type [typ]. *) - let with_type t typ env rdefs _ _ = + let with_type t typ env rdefs _ _ = (* spiwack: this function assumes that no evars can be created during this sort of coercion. If it is not the case it could produce bugs. We would need to add a handle @@ -154,13 +154,13 @@ module Refinable = struct let my_type = Retyping.get_type_of env !rdefs t in let j = Environ.make_judge t my_type in let tycon = Evarutil.mk_tycon_type typ in - let (new_defs,j') = - Coercion.Default.inh_conv_coerce_to (Util.dummy_loc) env !rdefs j tycon + let (new_defs,j') = + Coercion.Default.inh_conv_coerce_to (Pp.dummy_loc) env !rdefs j tycon in rdefs := new_defs; - j'.Environ.uj_val + j'.Environ.uj_val - (* spiwack: it is not very fine grain since it solves all typeclasses holes, + (* spiwack: it is not very fine grain since it solves all typeclasses holes, not only those containing the current goal, or a given term. But it seems to fit our needs so far. *) let resolve_typeclasses ?onlyargs ?split ?(fail=false) () env rdefs _ _ = @@ -214,23 +214,23 @@ module Refinable = struct let constr_of_raw handle check_type resolve_classes rawc env rdefs gl info = (* We need to keep trace of what [rdefs] was originally*) let init_defs = !rdefs in - (* if [check_type] is true, then creates a type constraint for the + (* if [check_type] is true, then creates a type constraint for the proof-to-be *) let tycon = Pretyping.OfType (Option.init check_type (Evd.evar_concl info)) in (* call to [understand_tcc_evars] returns a constr with undefined evars these evars will be our new goals *) - let open_constr = + let open_constr = Pretyping.Default.understand_tcc_evars ~resolve_classes rdefs env tycon rawc in ignore(update_handle handle init_defs !rdefs); - open_constr - + open_constr + let constr_of_open_constr handle check_type (evars, c) env rdefs gl info = let delta = update_handle handle !rdefs evars in rdefs := Evd.fold (fun ev evi evd -> Evd.add evd ev evi) delta !rdefs; if check_type then with_type c (Evd.evar_concl (content !rdefs gl)) env rdefs gl info else c - + end (* [refine t] takes a refinable term and use it as a partial proof for current @@ -245,10 +245,10 @@ let refine step env rdefs gl info = (* creates the new [evar_map] by defining the evar of the current goal as being [refine_step]. *) let new_defs = Evd.define gl.content (step.me) !rdefs in - rdefs := new_defs; + rdefs := new_defs; (* Filtering the [subgoals] for uninstanciated (=unsolved) goals. *) - let subgoals = - Option.List.flatten (List.map (advance !rdefs) subgoals) + let subgoals = + Option.List.flatten (List.map (advance !rdefs) subgoals) in { subgoals = subgoals } @@ -267,12 +267,12 @@ let clear ids env rdefs gl info = { subgoals = [cleared_goal] } let wrap_apply_to_hyp_and_dependent_on sign id f g = - try Environ.apply_to_hyp_and_dependent_on sign id f g - with Environ.Hyp_not_found -> - Util.error "No such assumption" + try Environ.apply_to_hyp_and_dependent_on sign id f g + with Environ.Hyp_not_found -> + Errors.error "No such assumption" let check_typability env sigma c = - let _ = Typing.type_of env sigma c in () + let _ = Typing.type_of env sigma c in () let recheck_typability (what,id) env sigma t = try check_typability env sigma t @@ -280,7 +280,7 @@ let recheck_typability (what,id) env sigma t = let s = match what with | None -> "the conclusion" | Some id -> "hypothesis "^(Names.string_of_id id) in - Util.error + Errors.error ("The correctness of "^s^" relies on the body of "^(Names.string_of_id id)) let remove_hyp_body env sigma id = @@ -288,11 +288,11 @@ let remove_hyp_body env sigma id = wrap_apply_to_hyp_and_dependent_on (Environ.named_context_val env) id (fun (_,c,t) _ -> match c with - | None -> Util.error ((Names.string_of_id id)^" is not a local definition") + | None -> Errors.error ((Names.string_of_id id)^" is not a local definition") | Some c ->(id,None,t)) (fun (id',c,t as d) sign -> ( - begin + begin let env = Environ.reset_with_named_context sign env in match c with | None -> recheck_typability (Some id',id) env sigma t @@ -301,18 +301,18 @@ let remove_hyp_body env sigma id = recheck_typability (Some id',id) env sigma b' end;d)) in - Environ.reset_with_named_context sign env + Environ.reset_with_named_context sign env let clear_body idents env rdefs gl info = let info = content !rdefs gl in let full_env = Environ.reset_with_named_context (Evd.evar_hyps info) env in - let aux env id = + let aux env id = let env' = remove_hyp_body env !rdefs id in recheck_typability (None,id) env' !rdefs (Evd.evar_concl info); env' in - let new_env = + let new_env = List.fold_left aux full_env idents in let concl = Evd.evar_concl info in @@ -334,7 +334,7 @@ let concl _ _ _ info = let hyps _ _ _ info = Evd.evar_hyps info -(* [env] is the current [Environ.env] containing both the +(* [env] is the current [Environ.env] containing both the environment in which the proof is ran, and the goal hypotheses *) let env env _ _ _ = env @@ -359,7 +359,7 @@ let equal { content = e1 } { content = e2 } = e1 = e2 let here goal value _ _ goal' _ = if equal goal goal' then value - else + else raise UndefinedHere (* arnaud: voir à la passer dans Util ? *) @@ -384,52 +384,52 @@ let convert_hyp check (id,b,bt as d) env rdefs gl info = let replace_function = (fun _ (_,c,ct) _ -> if check && not (Reductionops.is_conv env sigma bt ct) then - Util.error ("Incorrect change of the type of "^(Names.string_of_id id)); + Errors.error ("Incorrect change of the type of "^(Names.string_of_id id)); if check && not (Option.Misc.compare (Reductionops.is_conv env sigma) b c) then - Util.error ("Incorrect change of the body of "^(Names.string_of_id id)); + Errors.error ("Incorrect change of the body of "^(Names.string_of_id id)); d) in (* Modified named context. *) - let new_hyps = + let new_hyps = Environ.apply_to_hyp (hyps env rdefs gl info) id replace_function - in + in let new_env = Environ.reset_with_named_context new_hyps env in - let new_constr = + let new_constr = Evarutil.e_new_evar rdefs new_env (concl env rdefs gl info) in let (new_evar,_) = Term.destEvar new_constr in let new_goal = descendent gl new_evar in rdefs := Evd.define gl.content new_constr !rdefs; { subgoals = [new_goal] } - + let convert_concl check cl' env rdefs gl info = let sigma = !rdefs in let cl = concl env rdefs gl info in check_typability env sigma cl'; if (not check) || Reductionops.is_conv_leq env sigma cl' cl then - let new_constr = - Evarutil.e_new_evar rdefs env cl' + let new_constr = + Evarutil.e_new_evar rdefs env cl' in let (new_evar,_) = Term.destEvar new_constr in let new_goal = descendent gl new_evar in rdefs := Evd.define gl.content new_constr !rdefs; { subgoals = [new_goal] } else - Util.error "convert-concl rule passed non-converting term" + Errors.error "convert-concl rule passed non-converting term" -(*** Bureaucracy in hypotheses ***) +(*** Bureaucracy in hypotheses ***) (* Renames a hypothesis. *) let rename_hyp_sign id1 id2 sign = Environ.apply_to_hyp_and_dependent_on sign id1 (fun (_,b,t) _ -> (id2,b,t)) (fun d _ -> map_named_declaration (replace_vars [id1,mkVar id2]) d) -let rename_hyp id1 id2 env rdefs gl info = +let rename_hyp id1 id2 env rdefs gl info = let hyps = hyps env rdefs gl info in if id1 <> id2 && List.mem id2 (Termops.ids_of_named_context (Environ.named_context_of_val hyps)) then - Util.error ((Names.string_of_id id2)^" is already used."); + Errors.error ((Names.string_of_id id2)^" is already used."); let new_hyps = rename_hyp_sign id1 id2 hyps in let new_env = Environ.reset_with_named_context new_hyps env in let new_concl = Term.replace_vars [id1,mkVar id2] (concl env rdefs gl info) in @@ -442,13 +442,13 @@ let rename_hyp id1 id2 env rdefs gl info = (*** Additional functions ***) -(* emulates List.map for functions of type +(* emulates List.map for functions of type [Evd.evar_map -> 'a -> 'b * Evd.evar_map] on lists of type 'a, by propagating new evar_map to next definition. *) (*This sort of construction actually works with any monad (here the State monade in Haskell). There is a generic construction in Haskell called mapM. *) -let rec list_map f l s = +let rec list_map f l s = match l with | [] -> ([],s) | a::l -> let (a,s) = f s a in @@ -456,18 +456,18 @@ let rec list_map f l s = (a::l,s) -(* Layer to implement v8.2 tactic engine ontop of the new architecture. +(* Layer to implement v8.2 tactic engine ontop of the new architecture. Types are different from what they used to be due to a change of the internal types. *) module V82 = struct (* Old style env primitive *) - let env evars gl = + let env evars gl = let evi = content evars gl in Evd.evar_env evi (* For printing *) - let unfiltered_env evars gl = + let unfiltered_env evars gl = let evi = content evars gl in Evd.evar_unfiltered_env evi @@ -494,14 +494,14 @@ module V82 = struct (* Old style mk_goal primitive *) let mk_goal evars hyps concl extra = let evk = Evarutil.new_untyped_evar () in - let evi = { Evd.evar_hyps = hyps; - Evd.evar_concl = concl; - Evd.evar_filter = List.map (fun _ -> true) - (Environ.named_context_of_val hyps); - Evd.evar_body = Evd.Evar_empty; - Evd.evar_source = (Util.dummy_loc,Evd.GoalEvar); - Evd.evar_candidates = None; - Evd.evar_extra = extra } + let evi = { Evd.evar_hyps = hyps; + Evd.evar_concl = concl; + Evd.evar_filter = List.map (fun _ -> true) + (Environ.named_context_of_val hyps); + Evd.evar_body = Evd.Evar_empty; + Evd.evar_source = (Pp.dummy_loc,Evd.GoalEvar); + Evd.evar_candidates = None; + Evd.evar_extra = extra } in let evi = Typeclasses.mark_unresolvable evi in let evars = Evd.add evars evk evi in @@ -518,7 +518,7 @@ module V82 = struct (* Creates a dummy [goal sigma] for use in auto *) let dummy_goal = - (* This goal seems to be marshalled somewhere. Therefore it cannot be + (* This goal seems to be marshalled somewhere. Therefore it cannot be marked unresolvable for typeclasses, as non-empty Store.t-s happen to have functional content. *) let evi = Evd.make_evar Environ.empty_named_context_val Term.mkProp in @@ -532,14 +532,14 @@ module V82 = struct (* Instantiates a goal with an open term *) let partial_solution sigma { content=evk } c = Evd.define evk c sigma - + (* Parts of the progress tactical *) let same_goal evars1 gl1 evars2 gl2 = let evi1 = content evars1 gl1 in let evi2 = content evars2 gl2 in Term.eq_constr evi1.Evd.evar_concl evi2.Evd.evar_concl && Environ.eq_named_context_val evi1.Evd.evar_hyps evi2.Evd.evar_hyps - + let weak_progress glss gls = match glss.Evd.it with | [ g ] -> not (same_goal glss.Evd.sigma g gls.Evd.sigma gls.Evd.it) @@ -548,12 +548,12 @@ module V82 = struct let progress glss gls = weak_progress glss gls (* spiwack: progress normally goes like this: - (Evd.progress_evar_map gls.Evd.sigma glss.Evd.sigma) || (weak_progress glss gls) + (Evd.progress_evar_map gls.Evd.sigma glss.Evd.sigma) || (weak_progress glss gls) This is immensly slow in the current implementation. Maybe we could reimplement progress_evar_map with restricted folds like "fold_undefined", with a good implementation of them. *) - + (* Used for congruence closure *) let new_goal_with sigma gl new_hyps = let evi = content sigma gl in @@ -571,12 +571,12 @@ module V82 = struct (gl,sigma) (* Goal represented as a type, doesn't take into account section variables *) - let abstract_type sigma gl = + let abstract_type sigma gl = let (gl,sigma) = nf_evar sigma gl in let env = env sigma gl in let genv = Global.env () in - let is_proof_var decl = - try ignore (Environ.lookup_named (Util.pi1 decl) genv); false + let is_proof_var decl = + try ignore (Environ.lookup_named (Util.pi1 decl) genv); false with Not_found -> true in Environ.fold_named_context_reverse (fun t decl -> if is_proof_var decl then diff --git a/proofs/logic.ml b/proofs/logic.ml index 5babd03a8..c7df86e1f 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -8,6 +8,7 @@ open Compat open Pp +open Errors open Util open Names open Nameops @@ -48,7 +49,7 @@ open Pretype_errors let rec catchable_exception = function | Loc.Exc_located(_,e) -> catchable_exception e | LtacLocated(_,e) -> catchable_exception e - | Util.UserError _ | TypeError _ | PretypeError (_,_,TypingError _) + | Errors.UserError _ | TypeError _ | PretypeError (_,_,TypingError _) | RefinerError _ | Indrec.RecursionSchemeError _ | Nametab.GlobalizationError _ | PretypeError (_,_,VarNotFound _) (* reduction errors *) @@ -179,7 +180,7 @@ let reorder_context env sign ord = errorlabstrm "reorder_context" (str "Cannot move declaration " ++ pr_id top ++ spc() ++ str "before " ++ - prlist_with_sep pr_spc pr_id + pr_sequence pr_id (Idset.elements (Idset.inter h (global_vars_set_of_decl env d)))); step ord' expected ctxt_head mh (d::ctxt_tail) diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 3d507f358..9be475ac4 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -7,6 +7,7 @@ (************************************************************************) open Pp +open Errors open Util open Names open Nameops @@ -79,7 +80,7 @@ let cook_proof hook = hook prf; match Proof_global.close_proof () with | (i,([e],cg,str,h)) -> (i,(e,cg,str,h)) - | _ -> Util.anomaly "Pfedit.cook_proof: more than one proof term." + | _ -> Errors.anomaly "Pfedit.cook_proof: more than one proof term." let xml_cook_proof = ref (fun _ -> ()) let set_xml_cook_proof f = xml_cook_proof := f @@ -98,7 +99,7 @@ let get_used_variables () = exception NoSuchGoal let _ = Errors.register_handler begin function - | NoSuchGoal -> Util.error "No such goal." + | NoSuchGoal -> Errors.error "No such goal." | _ -> raise Errors.Unhandled end let get_nth_V82_goal i = @@ -112,11 +113,11 @@ let get_goal_context_gen i = try let { it=goal ; sigma=sigma } = get_nth_V82_goal i in (sigma, Refiner.pf_env { it=goal ; sigma=sigma }) - with Proof_global.NoCurrentProof -> Util.error "No focused proof." + with Proof_global.NoCurrentProof -> Errors.error "No focused proof." let get_goal_context i = try get_goal_context_gen i - with NoSuchGoal -> Util.error "No such goal." + with NoSuchGoal -> Errors.error "No such goal." let get_current_goal_context () = try get_goal_context_gen 1 @@ -128,7 +129,7 @@ let get_current_goal_context () = let current_proof_statement () = match Proof_global.V82.get_current_initial_conclusions () with | (id,([concl],strength,hook)) -> id,strength,concl,hook - | _ -> Util.anomaly "Pfedit.current_proof_statement: more than one statement" + | _ -> Errors.anomaly "Pfedit.current_proof_statement: more than one statement" let solve_nth ?(with_end_tac=false) gi tac = try @@ -140,10 +141,10 @@ let solve_nth ?(with_end_tac=false) gi tac = in Proof_global.run_tactic (Proofview.tclFOCUS gi gi tac) with - | Proof_global.NoCurrentProof -> Util.error "No focused proof" + | Proof_global.NoCurrentProof -> Errors.error "No focused proof" | Proofview.IndexOutOfRange | Failure "list_chop" -> let msg = str "No such goal: " ++ int gi ++ str "." in - Util.errorlabstrm "" msg + Errors.errorlabstrm "" msg let by = solve_nth 1 diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 7297b975f..e8b004200 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Pp open Names diff --git a/proofs/proof.ml b/proofs/proof.ml index 871e68acf..42a522b7c 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -102,7 +102,7 @@ end exception CannotUnfocusThisWay let _ = Errors.register_handler begin function | CannotUnfocusThisWay -> - Util.error "This proof is focused, but cannot be unfocused this way" + Errors.error "This proof is focused, but cannot be unfocused this way" | _ -> raise Errors.Unhandled end @@ -184,7 +184,7 @@ let push_focus cond inf context pr = exception FullyUnfocused let _ = Errors.register_handler begin function - | FullyUnfocused -> Util.error "The proof is not focused" + | FullyUnfocused -> Errors.error "The proof is not focused" | _ -> raise Errors.Unhandled end (* An auxiliary function to read the kind of the next focusing step *) @@ -211,7 +211,7 @@ let push_undo save pr = (* Auxiliary function to pop and read a [save_state] from the undo stack. *) exception EmptyUndoStack let _ = Errors.register_handler begin function - | EmptyUndoStack -> Util.error "Cannot undo: no more undo information" + | EmptyUndoStack -> Errors.error "Cannot undo: no more undo information" | _ -> raise Errors.Unhandled end let pop_undo pr = @@ -387,8 +387,8 @@ let start goals = exception UnfinishedProof exception HasUnresolvedEvar let _ = Errors.register_handler begin function - | UnfinishedProof -> Util.error "Some goals have not been solved." - | HasUnresolvedEvar -> Util.error "Some existential variables are uninstantiated." + | UnfinishedProof -> Errors.error "Some goals have not been solved." + | HasUnresolvedEvar -> Errors.error "Some existential variables are uninstantiated." | _ -> raise Errors.Unhandled end let return p = diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 9d5ba230e..63bc4a708 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -32,7 +32,7 @@ let proof_modes = Hashtbl.create 6 let find_proof_mode n = try Hashtbl.find proof_modes n with Not_found -> - Util.error (Format.sprintf "No proof mode named \"%s\"." n) + Errors.error (Format.sprintf "No proof mode named \"%s\"." n) let register_proof_mode ({ name = n } as m) = Hashtbl.add proof_modes n m (* initial mode: standard mode *) @@ -48,10 +48,10 @@ let _ = optdepr = false; optname = "default proof mode" ; optkey = ["Default";"Proof";"Mode"] ; - optread = begin fun () -> - let { name = name } = !default_proof_mode in name + optread = begin fun () -> + let { name = name } = !default_proof_mode in name end; - optwrite = begin fun n -> + optwrite = begin fun n -> default_proof_mode := find_proof_mode n end } @@ -63,14 +63,14 @@ type nproof = identifier*Proof.proof (* Extra info on proofs. *) type lemma_possible_guards = int list list -type proof_info = { +type proof_info = { strength : Decl_kinds.goal_kind ; - compute_guard : lemma_possible_guards; + compute_guard : lemma_possible_guards; hook :Tacexpr.declaration_hook ; mode : proof_mode } -(* Invariant: a proof is at most in one of current_proof and suspended. And the +(* Invariant: a proof is at most in one of current_proof and suspended. And the domain of proof_info is the union of that of current_proof and suspended.*) (* The head of [!current_proof] is the actual current proof, the other ones are to be resumed when the current proof is closed, aborted or suspended. *) @@ -82,15 +82,15 @@ let proof_info = ref (Idmap.empty : proof_info Idmap.t) let current_proof_mode = ref !default_proof_mode (* combinators for proof modes *) -let update_proof_mode () = +let update_proof_mode () = match !current_proof with - | (id,_)::_ -> + | (id,_)::_ -> let { mode = m } = Idmap.find id !proof_info in !current_proof_mode.reset (); current_proof_mode := m; !current_proof_mode.set () - | _ -> - !current_proof_mode.reset (); + | _ -> + !current_proof_mode.reset (); current_proof_mode := standard (* combinators for the current_proof and suspended lists *) @@ -99,10 +99,10 @@ let push a l = l := a::!l; exception NoSuchProof let _ = Errors.register_handler begin function - | NoSuchProof -> Util.error "No such proof." + | NoSuchProof -> Errors.error "No such proof." | _ -> raise Errors.Unhandled end -let rec extract id l = +let rec extract id l = let rec aux = function | ((id',_) as np)::l when id_ord id id' = 0 -> (np,l) | np::l -> let (np', l) = aux l in (np' , np::l) @@ -115,13 +115,13 @@ let rec extract id l = exception NoCurrentProof let _ = Errors.register_handler begin function - | NoCurrentProof -> Util.error "No focused proof (No proof-editing in progress)." + | NoCurrentProof -> Errors.error "No focused proof (No proof-editing in progress)." | _ -> raise Errors.Unhandled end let extract_top l = match !l with | np::l' -> l := l' ; update_proof_mode (); np - | [] -> raise NoCurrentProof + | [] -> raise NoCurrentProof let find_top l = match !l with | np::_ -> np @@ -134,7 +134,7 @@ let rotate_top l1 l2 = let rotate_find id l1 l2 = let np = extract id l1 in push np l2 - + (* combinators for the proof_info map *) let add id info m = @@ -148,7 +148,7 @@ let get_all_proof_names () = List.map fst !current_proof @ List.map fst !suspended -let give_me_the_proof () = +let give_me_the_proof () = snd (find_top current_proof) let get_current_proof_name () = @@ -157,14 +157,14 @@ let get_current_proof_name () = (* spiwack: it might be considered to move error messages away. Or else to remove special exceptions from Proof_global. Arguments for the former: there is no reason Proof_global is only - accessed directly through vernacular commands. Error message should be + accessed directly through vernacular commands. Error message should be pushed to external layers, and so we should be able to have a finer control on error message on complex actions. *) let msg_proofs use_resume = match get_all_proof_names () with | [] -> (spc () ++ str"(No proof-editing in progress).") | l -> (str"." ++ fnl () ++ str"Proofs currently edited:" ++ spc () ++ - (Util.prlist_with_sep Util.pr_spc Nameops.pr_id l) ++ + (pr_sequence Nameops.pr_id l) ++ str"." ++ (if use_resume then (fnl () ++ str"Use \"Resume\" first.") else (mt ())) @@ -173,14 +173,14 @@ let msg_proofs use_resume = let there_is_a_proof () = !current_proof <> [] let there_are_suspended_proofs () = !suspended <> [] -let there_are_pending_proofs () = - there_is_a_proof () || +let there_are_pending_proofs () = + there_is_a_proof () || there_are_suspended_proofs () -let check_no_pending_proof () = +let check_no_pending_proof () = if not (there_are_pending_proofs ()) then () else begin - Util.error (Pp.string_of_ppcmds + Errors.error (Pp.string_of_ppcmds (str"Proof editing in progress" ++ (msg_proofs false) ++ fnl() ++ str"Use \"Abort All\" first or complete proof(s).")) end @@ -196,24 +196,24 @@ let resume id = rotate_find id suspended current_proof let discard_gen id = - try + try ignore (extract id current_proof); remove id proof_info with NoSuchProof -> ignore (extract id suspended) -let discard (loc,id) = +let discard (loc,id) = try discard_gen id with NoSuchProof -> - Util.user_err_loc + Errors.user_err_loc (loc,"Pfedit.delete_proof",str"No such proof" ++ msg_proofs false) let discard_current () = let (id,_) = extract_top current_proof in remove id proof_info - + let discard_all () = - current_proof := []; + current_proof := []; suspended := []; proof_info := Idmap.empty @@ -222,7 +222,7 @@ let discard_all () = (* Core component. No undo handling. Applies to proof [id], and proof mode [m]. *) -let set_proof_mode m id = +let set_proof_mode m id = let info = Idmap.find id !proof_info in let info = { info with mode = m } in proof_info := Idmap.add id info !proof_info; @@ -241,7 +241,7 @@ let set_proof_mode mn = exception AlreadyExists let _ = Errors.register_handler begin function - | AlreadyExists -> Util.error "Already editing something of that name." + | AlreadyExists -> Errors.error "Already editing something of that name." | _ -> raise Errors.Unhandled end (* [start_proof s str env t hook tac] starts a proof of name [s] and @@ -259,14 +259,14 @@ let start_proof id str goals ?(compute_guard=[]) hook = end !current_proof end; let p = Proof.start goals in - add id { strength=str ; - compute_guard=compute_guard ; + add id { strength=str ; + compute_guard=compute_guard ; hook=hook ; mode = ! default_proof_mode } proof_info ; push (id,p) current_proof (* arnaud: à enlever *) -let run_tactic tac = +let run_tactic tac = let p = give_me_the_proof () in let env = Global.env () in Proof.run_tactic env tac p @@ -293,7 +293,7 @@ let with_end_tac tac = let close_proof () = (* spiwack: for now close_proof doesn't actually discard the proof, it is done by [Command.save]. *) - try + try let id = get_current_proof_name () in let p = give_me_the_proof () in let proofs_and_types = Proof.return p in @@ -309,11 +309,11 @@ let close_proof () = Idmap.find id !proof_info in (id, (entries,cg,str,hook)) - with + with | Proof.UnfinishedProof -> - Util.error "Attempt to save an incomplete proof" + Errors.error "Attempt to save an incomplete proof" | Proof.HasUnresolvedEvar -> - Util.error "Attempt to save a proof with existential variables still non-instantiated" + Errors.error "Attempt to save a proof with existential variables still non-instantiated" (**********************************************************) @@ -392,7 +392,7 @@ module Bullet = struct while bul <> pop p do () done; push bul p end - else + else push bul p let strict = { @@ -404,7 +404,7 @@ module Bullet = struct (* Current bullet behavior, controled by the option *) let current_behavior = ref Strict.strict - + let _ = Goptions.declare_string_option {Goptions. optsync = true; @@ -428,7 +428,7 @@ module V82 = struct let get_current_initial_conclusions () = let p = give_me_the_proof () in let id = get_current_proof_name () in - let { strength=str ; hook=hook } = + let { strength=str ; hook=hook } = Idmap.find id !proof_info in (id,(Proof.V82.get_initial_conclusions p, str, hook)) diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index ed6a60c71..8e09ab9c1 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -35,7 +35,7 @@ val check_no_pending_proof : unit -> unit val get_current_proof_name : unit -> Names.identifier val get_all_proof_names : unit -> Names.identifier list -val discard : Names.identifier Util.located -> unit +val discard : Names.identifier Pp.located -> unit val discard_current : unit -> unit val discard_all : unit -> unit diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index e256794a7..876982407 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -12,7 +12,7 @@ open Evd open Names open Libnames open Term -open Util +open Pp open Tacexpr (* open Decl_expr *) open Glob_term diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index 2b0a10ba3..10e2ad323 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -11,7 +11,7 @@ open Evd open Names open Libnames open Term -open Util +open Pp open Tacexpr open Glob_term open Genarg diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 4246cc9c7..ff0e8de41 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -111,7 +111,7 @@ let focus_sublist i j l = try Util.list_chop (j-i+1) sub_right with Failure "list_chop" -> - Util.errorlabstrm "nth_unproven" (Pp.str"No such unproven subgoal") + Errors.errorlabstrm "nth_unproven" (Pp.str"No such unproven subgoal") in (sub, (left,right)) @@ -280,7 +280,7 @@ let tclFOCUS i j t env = { go = fun sk fk step -> is used otherwise. *) exception SizeMismatch let _ = Errors.register_handler begin function - | SizeMismatch -> Util.error "Incorrect number of goals." + | SizeMismatch -> Errors.error "Incorrect number of goals." | _ -> raise Errors.Unhandled end (* spiwack: we use an parametrised function to generate the dispatch tacticals. @@ -316,7 +316,7 @@ let rec tclDISPATCHGEN null join tacs env = { go = fun sk fk step -> on with these exceptions. Does not catch anomalies. *) let purify t = let t' env = { go = fun sk fk step -> try (t env).go (fun x -> sk (Util.Inl x)) fk step - with Util.Anomaly _ as e -> raise e + with Errors.Anomaly _ as e -> raise e | e -> sk (Util.Inr e) fk step } in @@ -400,7 +400,7 @@ let rec tclGOALBINDU s k = open Pretype_errors let rec catchable_exception = function | Loc.Exc_located(_,e) -> catchable_exception e - | Util.UserError _ + | Errors.UserError _ | Type_errors.TypeError _ | PretypeError (_,_,TypingError _) | Indrec.RecursionSchemeError _ | Nametab.GlobalizationError _ | PretypeError (_,_,VarNotFound _) @@ -505,9 +505,9 @@ module V82 = struct let (evk,_) = let evl = Evarutil.non_instantiated pv.solution in if (n <= 0) then - Util.error "incorrect existential variable index" + Errors.error "incorrect existential variable index" else if List.length evl < n then - Util.error "not so many uninstantiated existential variables" + Errors.error "not so many uninstantiated existential variables" else List.nth evl (n-1) in diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 10e1e66cb..bddf77d1f 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -7,6 +7,7 @@ (************************************************************************) open Pp +open Errors open Util open Names open Term diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 5cd855476..19c09571f 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -8,6 +8,7 @@ open Compat open Pp +open Errors open Util open Term open Termops diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml index b8279b8f9..90dddb748 100644 --- a/proofs/tacexpr.ml +++ b/proofs/tacexpr.ml @@ -11,6 +11,8 @@ open Topconstr open Libnames open Nametab open Glob_term +open Errors +open Pp open Util open Genarg open Pattern diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 5475daa89..75e9cdf62 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -7,6 +7,7 @@ (************************************************************************) open Pp +open Errors open Util open Names open Namegen @@ -217,5 +218,5 @@ let pr_gls gls = let pr_glls glls = hov 0 (pr_evar_map (Some 2) (sig_sig glls) ++ fnl () ++ - prlist_with_sep pr_fnl (db_pr_goal (project glls)) (sig_it glls)) + prlist_with_sep fnl (db_pr_goal (project glls)) (sig_it glls)) diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli index 62c2359b6..74c831487 100644 --- a/proofs/tactic_debug.mli +++ b/proofs/tactic_debug.mli @@ -78,4 +78,4 @@ val db_logic_failure : debug_info -> exn -> unit (** Prints a logic failure message for a rule *) val db_breakpoint : debug_info -> - identifier Util.located message_token list -> unit + identifier Pp.located message_token list -> unit diff --git a/scripts/coqc.ml b/scripts/coqc.ml index bc4b1321e..ce92b9118 100644 --- a/scripts/coqc.ml +++ b/scripts/coqc.ml @@ -151,7 +151,7 @@ let parse_args () = | ("-where") :: _ -> (try print_endline (Envars.coqlib ()) - with Util.UserError(_,pps) -> Pp.msgerrnl (Pp.hov 0 pps)); + with Errors.UserError(_,pps) -> Pp.msgerrnl (Pp.hov 0 pps)); exit 0 | ("-config" | "--config") :: _ -> Usage.print_config (); exit 0 diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml index 7dcfbab16..d0132763a 100644 --- a/scripts/coqmktop.ml +++ b/scripts/coqmktop.ml @@ -223,7 +223,7 @@ let declare_loading_string () = \n let ppf = Format.std_formatter;;\ \n Mltop.set_top\ \n {Mltop.load_obj=\ -\n (fun f -> if not (Topdirs.load_file ppf f) then Util.error (\"Could not load plugin \"^f));\ +\n (fun f -> if not (Topdirs.load_file ppf f) then Errors.error (\"Could not load plugin \"^f));\ \n Mltop.use_file=Topdirs.dir_use ppf;\ \n Mltop.add_dir=Topdirs.dir_directory;\ \n Mltop.ml_loop=(fun () -> Toploop.loop ppf) };;\ diff --git a/tactics/auto.ml b/tactics/auto.ml index 93ca89f47..c650565c0 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -7,6 +7,7 @@ (************************************************************************) open Pp +open Errors open Util open Names open Nameops @@ -268,7 +269,7 @@ let path_derivate hp hint = normalize_path (path_derivate hp hint) let rec pp_hints_path = function | PathAtom (PathAny) -> str"." - | PathAtom (PathHints grs) -> prlist_with_sep pr_spc pr_global grs + | PathAtom (PathHints grs) -> pr_sequence pr_global grs | PathStar p -> str "(" ++ pp_hints_path p ++ str")*" | PathSeq (p, p') -> pp_hints_path p ++ str" ; " ++ pp_hints_path p' | PathOr (p, p') -> @@ -960,7 +961,7 @@ let print_applicable_hint () = let pts = get_pftreestate () in let glss = Proof.V82.subgoals pts in match glss.Evd.it with - | [] -> Util.error "No focused goal." + | [] -> Errors.error "No focused goal." | g::_ -> let gl = { Evd.it = g; sigma = glss.Evd.sigma } in print_hint_term (pf_concl gl) diff --git a/tactics/auto.mli b/tactics/auto.mli index 521c5ed24..bd425c1de 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Names open Term diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index a974c76a0..990da9306 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -16,6 +16,7 @@ open Tacinterp open Tactics open Term open Termops +open Errors open Util open Glob_term open Vernacinterp @@ -203,7 +204,7 @@ let auto_multi_rewrite_with ?(conds=Naive) tac_main lbas cl gl = *) gen_auto_multi_rewrite conds tac_main lbas cl gl | _ -> - Util.errorlabstrm "autorewrite" + Errors.errorlabstrm "autorewrite" (strbrk "autorewrite .. in .. using can only be used either with a unique hypothesis or on the conclusion.") (* Functions necessary to the library object declaration *) diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli index 3205b0418..6481217b6 100644 --- a/tactics/autorewrite.mli +++ b/tactics/autorewrite.mli @@ -12,7 +12,7 @@ open Tacmach open Equality (** Rewriting rules before tactic interpretation *) -type raw_rew_rule = Util.loc * Term.constr * bool * Tacexpr.raw_tactic_expr +type raw_rew_rule = Pp.loc * Term.constr * bool * Tacexpr.raw_tactic_expr (** To add rewriting rules to a base *) val add_rew_rules : string -> raw_rew_rule list -> unit @@ -56,6 +56,6 @@ type hypinfo = { } val find_applied_relation : bool -> - Util.loc -> + Pp.loc -> Environ.env -> Evd.evar_map -> Term.constr -> bool -> hypinfo diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index 42df244de..4a850db66 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -9,6 +9,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) open Pp +open Errors open Util open Names open Nameops @@ -212,7 +213,7 @@ let nb_empty_evars s = let pr_ev evs ev = Printer.pr_constr_env (Goal.V82.env evs ev) (Evarutil.nf_evar evs (Goal.V82.concl evs ev)) -let pr_depth l = prlist_with_sep (fun () -> str ".") pr_int (List.rev l) +let pr_depth l = prlist_with_sep (fun () -> str ".") int (List.rev l) type autoinfo = { hints : Auto.hint_db; is_evar: existential_key option; only_classes: bool; auto_depth: int list; auto_last_tac: std_ppcmds Lazy.t; @@ -744,7 +745,7 @@ ARGUMENT EXTEND debug TYPED AS bool PRINTED BY pr_debug END let pr_depth _prc _prlc _prt = function - Some i -> Util.pr_int i + Some i -> Pp.int i | None -> Pp.mt() ARGUMENT EXTEND depth TYPED AS int option PRINTED BY pr_depth diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index a3d43623e..f8cca076f 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -6,7 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Util +open Pp +open Errors open Term open Proof_type open Hipattern diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml index fd924707c..e7c4e0676 100644 --- a/tactics/dhyp.ml +++ b/tactics/dhyp.ml @@ -110,6 +110,7 @@ Qed. *) open Pp +open Errors open Util open Names open Term diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index 9966fb772..4923aa720 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -9,6 +9,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) open Pp +open Errors open Util open Names open Nameops @@ -505,7 +506,7 @@ let pr_hints_path_atom prc _ _ a = match a with | PathAny -> str"." | PathHints grs -> - prlist_with_sep pr_spc Printer.pr_global grs + pr_sequence Printer.pr_global grs ARGUMENT EXTEND hints_path_atom TYPED AS hints_path_atom diff --git a/tactics/elim.ml b/tactics/elim.ml index 1ff8800f1..aa13d27b1 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -7,6 +7,7 @@ (************************************************************************) open Pp +open Errors open Util open Names open Term diff --git a/tactics/elim.mli b/tactics/elim.mli index 48a7ca68c..c40d1cbbc 100644 --- a/tactics/elim.mli +++ b/tactics/elim.mli @@ -19,7 +19,7 @@ val introElimAssumsThen : (branch_assumptions -> tactic) -> branch_args -> tactic val introCaseAssumsThen : - (intro_pattern_expr Util.located list -> branch_assumptions -> tactic) -> + (intro_pattern_expr Pp.located list -> branch_assumptions -> tactic) -> branch_args -> tactic val general_decompose : (identifier * constr -> bool) -> constr -> tactic diff --git a/tactics/eqdecide.ml4 b/tactics/eqdecide.ml4 index 6d40b2daf..1a65f6278 100644 --- a/tactics/eqdecide.ml4 +++ b/tactics/eqdecide.ml4 @@ -14,6 +14,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) +open Errors open Util open Names open Namegen diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index 779fe265b..fe380db7c 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -44,6 +44,7 @@ natural expectation of the user. *) +open Errors open Util open Names open Term diff --git a/tactics/equality.ml b/tactics/equality.ml index 10fd0fef9..e3b62e496 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -7,6 +7,7 @@ (************************************************************************) open Pp +open Errors open Util open Names open Nameops diff --git a/tactics/equality.mli b/tactics/equality.mli index 790594699..12deb7d32 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -7,6 +7,7 @@ (************************************************************************) (*i*) +open Pp open Util open Names open Term diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml index 992fdc915..f1341762a 100644 --- a/tactics/evar_tactics.ml +++ b/tactics/evar_tactics.ml @@ -7,7 +7,8 @@ (************************************************************************) open Term -open Util +open Pp +open Errors open Evar_refiner open Tacmach open Tacexpr diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4 index 6a13ac2a9..0496d758b 100644 --- a/tactics/extraargs.ml4 +++ b/tactics/extraargs.ml4 @@ -127,7 +127,7 @@ END type 'id gen_place= ('id * hyp_location_flag,unit) location -type loc_place = identifier Util.located gen_place +type loc_place = identifier Pp.located gen_place type place = identifier gen_place let pr_gen_place pr_id = function @@ -166,11 +166,11 @@ ARGUMENT EXTEND hloc | [ "in" "|-" "*" ] -> [ ConclLocation () ] | [ "in" ident(id) ] -> - [ HypLocation ((Util.dummy_loc,id),InHyp) ] + [ HypLocation ((Pp.dummy_loc,id),InHyp) ] | [ "in" "(" "Type" "of" ident(id) ")" ] -> - [ HypLocation ((Util.dummy_loc,id),InHypTypeOnly) ] + [ HypLocation ((Pp.dummy_loc,id),InHypTypeOnly) ] | [ "in" "(" "Value" "of" ident(id) ")" ] -> - [ HypLocation ((Util.dummy_loc,id),InHypValueOnly) ] + [ HypLocation ((Pp.dummy_loc,id),InHypValueOnly) ] END @@ -203,7 +203,7 @@ let pr_in_hyp pr_id (lo,concl) : Pp.std_ppcmds = | None,false -> str "in" ++ spc () ++ str "*" ++ spc () ++ str "|-" | Some l,_ -> str "in" ++ - Util.prlist (fun id -> spc () ++ pr_id id) l ++ + pr_sequence pr_id l ++ match concl with | true -> spc () ++ str "|-" ++ spc () ++ str "*" | _ -> mt () @@ -214,7 +214,7 @@ let pr_in_arg_hyp _ _ _ = pr_in_hyp (fun (_,id) -> Ppconstr.pr_id id) let pr_in_arg_hyp_typed _ _ _ = pr_in_hyp Ppconstr.pr_id -let pr_var_list_gen pr_id = Util.prlist_with_sep (fun () -> str ",") pr_id +let pr_var_list_gen pr_id = Pp.prlist_with_sep (fun () -> str ",") pr_id let pr_var_list_typed _ _ _ = pr_var_list_gen Ppconstr.pr_id diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli index 2abca40eb..a682af04f 100644 --- a/tactics/extraargs.mli +++ b/tactics/extraargs.mli @@ -30,7 +30,7 @@ val glob : constr_expr Pcoq.Gram.entry type 'id gen_place= ('id * hyp_location_flag,unit) location -type loc_place = identifier Util.located gen_place +type loc_place = identifier Pp.located gen_place type place = identifier gen_place val rawwit_hloc : loc_place raw_abstract_argument_type @@ -38,10 +38,10 @@ val wit_hloc : place typed_abstract_argument_type val hloc : loc_place Pcoq.Gram.entry val pr_hloc : loc_place -> Pp.std_ppcmds -val in_arg_hyp: (Names.identifier Util.located list option * bool) Pcoq.Gram.entry -val rawwit_in_arg_hyp : (Names.identifier Util.located list option * bool) raw_abstract_argument_type +val in_arg_hyp: (Names.identifier Pp.located list option * bool) Pcoq.Gram.entry +val rawwit_in_arg_hyp : (Names.identifier Pp.located list option * bool) raw_abstract_argument_type val wit_in_arg_hyp : (Names.identifier list option * bool) typed_abstract_argument_type -val raw_in_arg_hyp_to_clause : (Names.identifier Util.located list option * bool) -> Tacticals.clause +val raw_in_arg_hyp_to_clause : (Names.identifier Pp.located list option * bool) -> Tacticals.clause val glob_in_arg_hyp_to_clause : (Names.identifier list option * bool) -> Tacticals.clause val pr_in_arg_hyp : (Names.identifier list option * bool) -> Pp.std_ppcmds diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 44a3b0173..9c0d5db2c 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -17,6 +17,7 @@ open Names open Tacexpr open Glob_term open Tactics +open Errors open Util open Evd open Equality @@ -60,7 +61,7 @@ END let induction_arg_of_quantified_hyp = function | AnonHyp n -> ElimOnAnonHyp n - | NamedHyp id -> ElimOnIdent (Util.dummy_loc,id) + | NamedHyp id -> ElimOnIdent (Pp.dummy_loc,id) (* Versions *_main must come first!! so that "1" is interpreted as a ElimOnAnonHyp and not as a "constr", and "id" is interpreted as a diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml index fafc681ae..302bde6e6 100644 --- a/tactics/hiddentac.ml +++ b/tactics/hiddentac.ml @@ -62,10 +62,10 @@ let h_generalize cl = let h_generalize_dep c = abstract_tactic (TacGeneralizeDep c) (generalize_dep c) let h_let_tac b na c cl = - let with_eq = if b then None else Some (true,(dummy_loc,IntroAnonymous)) in + let with_eq = if b then None else Some (true,(Pp.dummy_loc,IntroAnonymous)) in abstract_tactic (TacLetTac (na,c,cl,b)) (letin_tac with_eq na c None cl) let h_let_pat_tac b na c cl = - let with_eq = if b then None else Some (true,(dummy_loc,IntroAnonymous)) in + let with_eq = if b then None else Some (true,(Pp.dummy_loc,IntroAnonymous)) in abstract_tactic (TacLetTac (na,snd c,cl,b)) (letin_pat_tac with_eq na c None cl) @@ -130,8 +130,8 @@ let h_transitivity c = abstract_tactic (TacTransitivity c) (intros_transitivity c) -let h_simplest_apply c = h_apply false false [dummy_loc,(c,NoBindings)] -let h_simplest_eapply c = h_apply false true [dummy_loc,(c,NoBindings)] +let h_simplest_apply c = h_apply false false [Pp.dummy_loc,(c,NoBindings)] +let h_simplest_eapply c = h_apply false true [Pp.dummy_loc,(c,NoBindings)] let h_simplest_elim c = h_elim false (c,NoBindings) None let h_simplest_case c = h_case false (c,NoBindings) diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli index 96e7e3f03..ca683cc24 100644 --- a/tactics/hiddentac.mli +++ b/tactics/hiddentac.mli @@ -7,7 +7,7 @@ (************************************************************************) open Names -open Util +open Pp open Term open Proof_type open Tacmach diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4 index 9057c60d3..6f07eed70 100644 --- a/tactics/hipattern.ml4 +++ b/tactics/hipattern.ml4 @@ -9,6 +9,7 @@ (*i camlp4deps: "parsing/grammar.cma parsing/q_constr.cmo" i*) open Pp +open Errors open Util open Names open Nameops diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli index aa3863649..82e9e3b8e 100644 --- a/tactics/hipattern.mli +++ b/tactics/hipattern.mli @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Names open Term diff --git a/tactics/inv.ml b/tactics/inv.ml index 2ae4e22e5..47e50d832 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -7,6 +7,7 @@ (************************************************************************) open Pp +open Errors open Util open Names open Nameops diff --git a/tactics/inv.mli b/tactics/inv.mli index ef828d882..a7e70dd0d 100644 --- a/tactics/inv.mli +++ b/tactics/inv.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Util +open Pp open Names open Term open Tacmach diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 1697c1465..33f8c9eef 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -7,6 +7,7 @@ (************************************************************************) open Pp +open Errors open Util open Names open Nameops diff --git a/tactics/leminv.mli b/tactics/leminv.mli index 233aeba3a..d5deff1f5 100644 --- a/tactics/leminv.mli +++ b/tactics/leminv.mli @@ -1,4 +1,4 @@ -open Util +open Pp open Names open Term open Glob_term diff --git a/tactics/nbtermdn.ml b/tactics/nbtermdn.ml index 4e34fae84..dce518f87 100644 --- a/tactics/nbtermdn.ml +++ b/tactics/nbtermdn.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Names open Term diff --git a/tactics/refine.ml b/tactics/refine.ml index e7f3998aa..fa023e78e 100644 --- a/tactics/refine.ml +++ b/tactics/refine.ml @@ -47,6 +47,7 @@ *) open Pp +open Errors open Util open Names open Term diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index ef3ec1470..b8bd166b9 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -9,6 +9,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) open Pp +open Errors open Util open Names open Nameops diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index e2a99707f..d4a7be4ec 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -18,6 +18,7 @@ open Pp open Glob_term open Sign open Tacred +open Errors open Util open Names open Nameops diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index d9dc8094f..4d01e5ad9 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -7,6 +7,7 @@ (************************************************************************) open Pp +open Errors open Util open Names open Proof_type @@ -102,7 +103,7 @@ val intern_constr_with_bindings : glob_constr_and_expr * glob_constr_and_expr Glob_term.bindings val intern_hyp : - glob_sign -> identifier Util.located -> identifier Util.located + glob_sign -> identifier Pp.located -> identifier Pp.located val subst_genarg : substitution -> glob_generic_argument -> glob_generic_argument diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 11625cbdf..2bb9c1cbe 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -7,6 +7,7 @@ (************************************************************************) open Pp +open Errors open Util open Names open Term diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index db9ab0c9b..42c70eef4 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -7,6 +7,7 @@ (************************************************************************) open Pp +open Errors open Util open Names open Term @@ -170,7 +171,7 @@ type branch_assumptions = { (** [check_disjunctive_pattern_size loc pats n] returns an appropriate error message if |pats| <> n *) val check_or_and_pattern_size : - Util.loc -> or_and_intro_pattern_expr -> int -> unit + Pp.loc -> or_and_intro_pattern_expr -> int -> unit (** Tolerate "[]" to mean a disjunctive pattern of any length *) val fix_empty_or_and_pattern : int -> or_and_intro_pattern_expr -> diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 11b0b9b81..0f23d512f 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -8,6 +8,7 @@ open Compat open Pp +open Errors open Util open Names open Nameops diff --git a/tactics/tactics.mli b/tactics/tactics.mli index f8f32b792..6e3c2cff4 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Pp open Util open Names open Term diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4 index b7a58be45..c953bedcb 100644 --- a/tactics/tauto.ml4 +++ b/tactics/tauto.ml4 @@ -17,6 +17,7 @@ open Proof_type open Tacticals open Tacinterp open Tactics +open Errors open Util open Genarg diff --git a/tactics/termdn.ml b/tactics/termdn.ml index 443acc6f5..5f6e5580e 100644 --- a/tactics/termdn.ml +++ b/tactics/termdn.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Names open Nameops diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out index 7c9b1e27c..f5636fbf9 100644 --- a/test-suite/output/Arguments.out +++ b/test-suite/output/Arguments.out @@ -22,16 +22,15 @@ Expands to: Constant Coq.Init.Peano.minus minus : nat -> nat -> nat Argument scopes are [nat_scope nat_scope] -The simpl tactic unfolds minus - when the 1st and 2nd arguments evaluate to a constructor and - when applied to 2 arguments +The simpl tactic unfolds minus when the 1st and + 2nd arguments evaluate to a constructor and when applied to 2 arguments minus is transparent Expands to: Constant Coq.Init.Peano.minus minus : nat -> nat -> nat Argument scopes are [nat_scope nat_scope] -The simpl tactic unfolds minus - when the 1st and 2nd arguments evaluate to a constructor +The simpl tactic unfolds minus when the 1st and + 2nd arguments evaluate to a constructor minus is transparent Expands to: Constant Coq.Init.Peano.minus pf : @@ -65,30 +64,30 @@ Expands to: Constant Top.S1.S2.f f : T1 -> T2 -> nat -> unit -> nat -> nat Argument scopes are [_ _ nat_scope _ nat_scope] -The simpl tactic unfolds f - when the 3rd, 4th and 5th arguments evaluate to a constructor +The simpl tactic unfolds f when the 3rd, 4th and + 5th arguments evaluate to a constructor f is transparent Expands to: Constant Top.S1.S2.f f : forall T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat Argument T2 is implicit Argument scopes are [type_scope _ _ nat_scope _ nat_scope] -The simpl tactic unfolds f - when the 4th, 5th and 6th arguments evaluate to a constructor +The simpl tactic unfolds f when the 4th, 5th and + 6th arguments evaluate to a constructor f is transparent Expands to: Constant Top.S1.f f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat Arguments T1, T2 are implicit Argument scopes are [type_scope type_scope _ _ nat_scope _ nat_scope] -The simpl tactic unfolds f - when the 5th, 6th and 7th arguments evaluate to a constructor +The simpl tactic unfolds f when the 5th, 6th and + 7th arguments evaluate to a constructor f is transparent Expands to: Constant Top.f f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat -The simpl tactic unfolds f - when the 5th, 6th and 7th arguments evaluate to a constructor +The simpl tactic unfolds f when the 5th, 6th and + 7th arguments evaluate to a constructor f is transparent Expands to: Constant Top.f forall w : r, w 3 true = tt diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index e443115cb..20042a5ed 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -53,8 +53,8 @@ myplus : forall T : Type, T -> nat -> nat -> nat Arguments are renamed to Z, t, n, m Argument Z is implicit and maximally inserted Argument scopes are [type_scope _ nat_scope nat_scope] -The simpl tactic unfolds myplus - when the 2nd and 3rd arguments evaluate to a constructor +The simpl tactic unfolds myplus when the 2nd and + 3rd arguments evaluate to a constructor myplus is transparent Expands to: Constant Top.Test1.myplus myplus @@ -90,8 +90,8 @@ myplus : forall T : Type, T -> nat -> nat -> nat Arguments are renamed to Z, t, n, m Argument Z is implicit and maximally inserted Argument scopes are [type_scope _ nat_scope nat_scope] -The simpl tactic unfolds myplus - when the 2nd and 3rd arguments evaluate to a constructor +The simpl tactic unfolds myplus when the 2nd and + 3rd arguments evaluate to a constructor myplus is transparent Expands to: Constant Top.myplus myplus diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index f4dab15f0..0357fc8a3 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -10,6 +10,7 @@ decidable equality, created by Vincent Siles, Oct 2007 *) open Tacmach +open Errors open Util open Flags open Decl_kinds diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml index 9258a39fc..1795336f4 100644 --- a/toplevel/autoinstance.ml +++ b/toplevel/autoinstance.ml @@ -53,7 +53,7 @@ let subst_evar_in_evm evar def evm = let rec safe_define evm ev c = if not (closedn (-1) c) then raise Termops.CannotFilter else -(* msgnl(str"safe_define "++pr_evar_map evm++spc()++str" |- ?"++Util.pr_int ev++str" := "++pr_constr c);*) +(* msgnl(str"safe_define "++pr_evar_map evm++spc()++str" |- ?"++Pp.int ev++str" := "++pr_constr c);*) let evi = (Evd.find evm ev) in let define_subst evm sigma = Util.Intmap.fold @@ -99,7 +99,7 @@ module SubstSet : Set.S with type elt = Termops.subst let complete_evar (cl,gen,evm:signature) (ev,evi) (k:signature -> unit) = let ev_typ = Libtypes.reduce (evar_concl evi) in let sort_is_prop = is_Prop (Typing.type_of (Global.env()) evm (evar_concl evi)) in -(* msgnl(str"cherche "++pr_constr ev_typ++str" pour "++Util.pr_int ev);*) +(* msgnl(str"cherche "++pr_constr ev_typ++str" pour "++Pp.int ev);*) let substs = ref SubstSet.empty in try List.iter ( fun (gr,(pat,_),s) -> @@ -107,7 +107,7 @@ let complete_evar (cl,gen,evm:signature) (ev,evi) (k:signature -> unit) = let genl = List.map (fun (_,_,t) -> t) genl in let ((cl,gen,evm),argl) = add_gen_ctx (cl,gen,evm) genl in let def = applistc (Libnames.constr_of_global gr) argl in -(* msgnl(str"essayons ?"++Util.pr_int ev++spc()++str":="++spc() +(* msgnl(str"essayons ?"++Pp.int ev++spc()++str":="++spc() ++pr_constr def++spc()++str":"++spc()++pr_constr (Global.type_of_global gr)*) (*++spc()++str"dans"++spc()++pr_evar_map evm++spc());*) try @@ -145,7 +145,7 @@ let complete_with_evars_permut (cl,gen,evm:signature) evl c (k:signature -> unit let tyl = List.map (fun (_,_,t) -> t) ctx in let ((cl,gen,evm),argl) = add_gen_ctx (cl,gen,evm) tyl in let def = applistc c argl in -(* msgnl(str"trouvé def ?"++Util.pr_int ev++str" := "++pr_constr def++str " dans "++pr_evar_map evm);*) +(* msgnl(str"trouvé def ?"++Pp.int ev++str" := "++pr_constr def++str " dans "++pr_evar_map evm);*) try if not (Evd.is_defined evm ev) then let evm = safe_define evm ev def in @@ -222,7 +222,7 @@ let complete_signature_with_def gr deftyp (k:instance_decl_function -> signature ( fun ctx typ -> List.iter (fun ((cl,ev,evm),_,_) -> -(* msgnl(pr_global gr++str" : "++pr_constr typ++str" matche ?"++Util.pr_int ev++str " dans "++pr_evar_map evm);*) +(* msgnl(pr_global gr++str" : "++pr_constr typ++str" matche ?"++Pp.int ev++str " dans "++pr_evar_map evm);*) smap := Gmapl.add (cl,evm) (ctx,ev) !smap) (Recordops.methods_matching typ) ) [] deftyp; @@ -265,7 +265,7 @@ let declare_instance (k:global_reference -> rel_context -> constr list -> unit) then Evd.remove evm ev,gen else evm,(ev::gen)) gen (evm,[]) in -(* msgnl(str"instance complète : ["++Util.prlist_with_sep (fun _ -> str";") Util.pr_int gen++str"] : "++spc()++pr_evar_map evm);*) +(* msgnl(str"instance complète : ["++Util.prlist_with_sep (fun _ -> str";") Pp.int gen++str"] : "++spc()++pr_evar_map evm);*) let ngen = List.length gen in let (_,ctx,evm) = List.fold_left ( fun (i,ctx,evm) ev -> diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index 5f2c3dbbe..281ae784e 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/cerrors.ml @@ -8,6 +8,7 @@ open Compat open Pp +open Errors open Util open Indtypes open Type_errors diff --git a/toplevel/cerrors.mli b/toplevel/cerrors.mli index da9d3590f..1d686b5da 100644 --- a/toplevel/cerrors.mli +++ b/toplevel/cerrors.mli @@ -7,6 +7,7 @@ (************************************************************************) open Pp +open Errors open Util (** Error report. *) diff --git a/toplevel/class.ml b/toplevel/class.ml index ebaa19b66..79d7a99fd 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Pp open Names diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 1e83e4b81..b513f2e2e 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -16,6 +16,8 @@ open Evd open Environ open Nametab open Mod_subst +open Errors +open Pp open Util open Typeclasses_errors open Typeclasses @@ -132,7 +134,7 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props (fun avoid (clname, (id, _, t)) -> match clname with | Some (cl, b) -> - let t = CHole (Util.dummy_loc, None) in + let t = CHole (Pp.dummy_loc, None) in t, avoid | None -> failwith ("new instance: under-applied typeclass")) cl @@ -224,7 +226,7 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props k.cl_projs; c :: props, rest' with Not_found -> - (CHole (Util.dummy_loc, None) :: props), rest + (CHole (Pp.dummy_loc, None) :: props), rest else props, rest) ([], props) k.cl_props in diff --git a/toplevel/classes.mli b/toplevel/classes.mli index 68a93a742..424645fe8 100644 --- a/toplevel/classes.mli +++ b/toplevel/classes.mli @@ -15,6 +15,7 @@ open Environ open Nametab open Mod_subst open Topconstr +open Errors open Util open Typeclasses open Implicit_quantifiers diff --git a/toplevel/command.ml b/toplevel/command.ml index eca53ae71..33a521d6f 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -7,6 +7,7 @@ (************************************************************************) open Pp +open Errors open Util open Flags open Term diff --git a/toplevel/command.mli b/toplevel/command.mli index 8ffdbdec4..76f6dd011 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Util +open Pp open Names open Term open Entries diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 0fc6d02c1..d17d07300 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -7,6 +7,7 @@ (************************************************************************) open Pp +open Errors open Util open System open Flags diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index bab711ea4..b24ac8e7d 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -7,6 +7,7 @@ (************************************************************************) open Names +open Errors open Util open Sign open Term diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 22568ee88..4306a9673 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -7,6 +7,7 @@ (************************************************************************) open Pp +open Errors open Util open Flags open Names @@ -176,8 +177,8 @@ let explain_cant_apply_bad_type env sigma (n,exptyp,actualtyp) rator randl = let pr,prt = pr_ljudge_env env rator in let term_string1 = str (plural nargs "term") in let term_string2 = - if nargs>1 then str "The " ++ nth n ++ str " term" else str "This term" in - let appl = prvect_with_sep pr_fnl + if nargs>1 then str "The " ++ pr_nth n ++ str " term" else str "This term" in + let appl = prvect_with_sep fnl (fun c -> let pc,pct = pr_ljudge_env env c in hov 2 (pc ++ spc () ++ str ": " ++ pct)) randl @@ -199,7 +200,7 @@ let explain_cant_apply_not_functional env sigma rator randl = (* let pe = pr_ne_context_of (str "in environment") env in*) let pr = pr_lconstr_env env rator.uj_val in let prt = pr_lconstr_env env rator.uj_type in - let appl = prvect_with_sep pr_fnl + let appl = prvect_with_sep fnl (fun c -> let pc = pr_lconstr_env env c.uj_val in let pct = pr_lconstr_env env c.uj_type in @@ -233,7 +234,7 @@ let explain_ill_formed_rec_body env err names i fixenv vdefj = let prt_name i = match names.(i) with Name id -> str "Recursive definition of " ++ pr_id id - | Anonymous -> str "The " ++ nth i ++ str " definition" in + | Anonymous -> str "The " ++ pr_nth i ++ str " definition" in let st = match err with @@ -248,18 +249,18 @@ let explain_ill_formed_rec_body env err names i fixenv vdefj = let called = match names.(j) with Name id -> pr_id id - | Anonymous -> str "the " ++ nth i ++ str " definition" in + | Anonymous -> str "the " ++ pr_nth i ++ str " definition" in let pr_db x = quote (pr_db env x) in let vars = match (lt,le) with ([],[]) -> assert false | ([],[x]) -> str "a subterm of " ++ pr_db x | ([],_) -> str "a subterm of the following variables: " ++ - prlist_with_sep pr_spc pr_db le + pr_sequence pr_db le | ([x],_) -> pr_db x | _ -> str "one of the following variables: " ++ - prlist_with_sep pr_spc pr_db lt in + pr_sequence pr_db lt in str "Recursive call to " ++ called ++ spc () ++ strbrk "has principal argument equal to" ++ spc () ++ pr_lconstr_env arg_env arg ++ strbrk " instead of " ++ vars @@ -268,7 +269,7 @@ let explain_ill_formed_rec_body env err names i fixenv vdefj = let called = match names.(j) with Name id -> pr_id id - | Anonymous -> str "the " ++ nth i ++ str " definition" in + | Anonymous -> str "the " ++ pr_nth i ++ str " definition" in str "Recursive call to " ++ called ++ str " has not enough arguments" (* CoFixpoint guard errors *) @@ -317,7 +318,7 @@ let explain_ill_typed_rec_body env sigma i names vdefj vargs = let pvd,pvdt = pr_ljudge_env env (vdefj.(i)) in let pv = pr_lconstr_env env vargs.(i) in str "The " ++ - (if Array.length vdefj = 1 then mt () else nth (i+1) ++ spc ()) ++ + (if Array.length vdefj = 1 then mt () else pr_nth (i+1) ++ spc ()) ++ str "recursive definition" ++ spc () ++ pvd ++ spc () ++ str "has type" ++ spc () ++ pvdt ++ spc () ++ str "while it should be" ++ spc () ++ pv ++ str "." @@ -363,7 +364,7 @@ let explain_hole_kind env evi = function pr_ne_context_of (str " in environment:"++ fnl ()) (mt ()) env) (mt ()) evi | TomatchTypeParameter (tyi,n) -> - str "the " ++ nth n ++ + str "the " ++ pr_nth n ++ str " argument of the inductive type (" ++ pr_inductive env tyi ++ str ") of this term" | GoalEvar -> @@ -694,7 +695,7 @@ let pr_constr_exprs exprs = let explain_no_instance env (_,id) l = str "No instance found for class " ++ Nameops.pr_id id ++ spc () ++ str "applied to arguments" ++ spc () ++ - prlist_with_sep pr_spc (pr_lconstr_env env) l + pr_sequence (pr_lconstr_env env) l let is_goal_evar evi = match evi.evar_source with (_, GoalEvar) -> true | _ -> false @@ -830,7 +831,7 @@ let error_bad_ind_parameters env c n v1 v2 = let pv1 = pr_lconstr_env env v1 in let pv2 = pr_lconstr_env env v2 in str "Last occurrence of " ++ pv2 ++ str " must have " ++ pv1 ++ - str " as " ++ nth n ++ str " argument in " ++ brk(1,1) ++ pc ++ str "." + str " as " ++ pr_nth n ++ str " argument in " ++ brk(1,1) ++ pc ++ str "." let error_same_names_types id = str "The name" ++ spc () ++ pr_id id ++ spc () ++ @@ -944,14 +945,14 @@ let explain_unused_clause env pats = (* Without localisation let s = if List.length pats > 1 then "s" else "" in (str ("Unused clause with pattern"^s) ++ spc () ++ - hov 0 (prlist_with_sep pr_spc pr_cases_pattern pats) ++ str ")") + hov 0 (pr_sequence pr_cases_pattern pats) ++ str ")") *) str "This clause is redundant." let explain_non_exhaustive env pats = str "Non exhaustive pattern-matching: no clause found for " ++ str (plural (List.length pats) "pattern") ++ - spc () ++ hov 0 (prlist_with_sep pr_spc pr_cases_pattern pats) + spc () ++ hov 0 (pr_sequence pr_cases_pattern pats) let explain_cannot_infer_predicate env typs = let env = make_all_name_different env in @@ -960,7 +961,7 @@ let explain_cannot_infer_predicate env typs = str "For " ++ pr_lconstr_env env cstr ++ str ": " ++ pr_lconstr_env env typ in str "Unable to unify the types found in the branches:" ++ - spc () ++ hov 0 (prlist_with_sep pr_fnl pr_branch (Array.to_list typs)) + spc () ++ hov 0 (prlist_with_sep fnl pr_branch (Array.to_list typs)) let explain_pattern_matching_error env = function | BadPattern (c,t) -> diff --git a/toplevel/himsg.mli b/toplevel/himsg.mli index a763472b9..7607bda42 100644 --- a/toplevel/himsg.mli +++ b/toplevel/himsg.mli @@ -38,7 +38,7 @@ val explain_reduction_tactic_error : Tacred.reduction_tactic_error -> std_ppcmds val explain_ltac_call_trace : - int * Proof_type.ltac_call_kind * Proof_type.ltac_trace * Util.loc -> + int * Proof_type.ltac_call_kind * Proof_type.ltac_trace * Pp.loc -> std_ppcmds val explain_module_error : Modops.module_typing_error -> std_ppcmds diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml index 158441190..4f365ebcf 100644 --- a/toplevel/ide_slave.ml +++ b/toplevel/ide_slave.ml @@ -9,6 +9,7 @@ open Vernacexpr open Names open Compat +open Errors open Util open Pp open Printer @@ -274,7 +275,7 @@ let compute_reset_info () = let coqide_cmd_checks (loc,ast) = let user_error s = - raise (Loc.Exc_located (loc, Util.UserError ("CoqIde", str s))) + raise (Loc.Exc_located (loc, Errors.UserError ("CoqIde", str s))) in if is_vernac_debug_command ast then user_error "Debug mode not available within CoqIDE"; @@ -504,7 +505,7 @@ let eval_call c = | Vernac.DuringCommandInterp (_,inner) -> handle_exn inner | Error_in_file (_,_,inner) -> None, pr_exn inner | Loc.Exc_located (loc, inner) when loc = dummy_loc -> None, pr_exn inner - | Loc.Exc_located (loc, inner) -> Some (Util.unloc loc), pr_exn inner + | Loc.Exc_located (loc, inner) -> Some (Pp.unloc loc), pr_exn inner | e -> None, pr_exn e in let interruptible f x = diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml index de3b62f82..d8b503f95 100644 --- a/toplevel/ind_tables.ml +++ b/toplevel/ind_tables.ml @@ -18,6 +18,7 @@ open Libobject open Nameops open Declarations open Term +open Errors open Util open Declare open Entries diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index 51eddbae9..640ef4ab5 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -16,6 +16,7 @@ open Pp open Flags +open Errors open Util open Names open Declarations diff --git a/toplevel/indschemes.mli b/toplevel/indschemes.mli index 87aedc7be..21e39e0ca 100644 --- a/toplevel/indschemes.mli +++ b/toplevel/indschemes.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Util +open Pp open Names open Term open Environ diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml index 7704449f5..2d4633427 100644 --- a/toplevel/lemmas.ml +++ b/toplevel/lemmas.ml @@ -9,6 +9,7 @@ (* Created by Hugo Herbelin from contents related to lemma proofs in file command.ml, Aug 2009 *) +open Errors open Util open Flags open Pp diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 6a4d72516..76326f51f 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -9,6 +9,7 @@ open Pp open Flags open Compat +open Errors open Util open Names open Topconstr diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli index 4ee1310a0..74a8e0fe9 100644 --- a/toplevel/metasyntax.mli +++ b/toplevel/metasyntax.mli @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Names open Libnames diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4 index 025c972fe..da9575ca6 100644 --- a/toplevel/mltop.ml4 +++ b/toplevel/mltop.ml4 @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Pp open Flags @@ -326,10 +327,10 @@ let declare_ml_modules local l = let print_ml_path () = let l = !coq_mlpath_copy in ppnl (str"ML Load Path:" ++ fnl () ++ str" " ++ - hv 0 (prlist_with_sep pr_fnl pr_str l)) + hv 0 (prlist_with_sep fnl str l)) (* Printing of loaded ML modules *) let print_ml_modules () = let l = get_loaded_modules () in - pp (str"Loaded ML Modules: " ++ pr_vertical_list pr_str l) + pp (str"Loaded ML Modules: " ++ pr_vertical_list str l) diff --git a/toplevel/record.ml b/toplevel/record.ml index 64942a5d2..0ddc59c50 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -7,6 +7,7 @@ (************************************************************************) open Pp +open Errors open Util open Names open Libnames @@ -148,7 +149,7 @@ let subst_projection fid l c = | NoProjection (Name id) -> bad_projs := id :: !bad_projs; mkRel k | NoProjection Anonymous -> errorlabstrm "" (str "Field " ++ pr_id fid ++ - str " depends on the " ++ str (ordinal (k-depth-1)) ++ str + str " depends on the " ++ pr_nth (k-depth-1) ++ str " field which has no name.") else mkRel (k-lv) diff --git a/toplevel/search.ml b/toplevel/search.ml index 33e8e51db..2213d25f9 100644 --- a/toplevel/search.ml +++ b/toplevel/search.ml @@ -7,6 +7,7 @@ (************************************************************************) open Pp +open Errors open Util open Names open Nameops @@ -170,7 +171,7 @@ let raw_search_rewrite extra_filter display_function pattern = display_function gref_eq let raw_search_by_head extra_filter display_function pattern = - Util.todo "raw_search_by_head" + Errors.todo "raw_search_by_head" let name_of_reference ref = string_of_id (basename_of_global ref) diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index 699fd12f9..5187b3a28 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -7,6 +7,7 @@ (************************************************************************) open Pp +open Errors open Util open Flags open Cerrors diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index cbd95a4fb..60354f4cf 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -10,6 +10,7 @@ open Pp open Lexer +open Errors open Util open Flags open System @@ -22,7 +23,7 @@ open Compat Use the module Coqtoplevel, which catches these exceptions (the exceptions are explained only at the toplevel). *) -exception DuringCommandInterp of Util.loc * exn +exception DuringCommandInterp of Pp.loc * exn exception HasNotFailed diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli index d89e90d0c..1cfd94e05 100644 --- a/toplevel/vernac.mli +++ b/toplevel/vernac.mli @@ -12,16 +12,16 @@ Raises [End_of_file] if EOF (or Ctrl-D) is reached. *) val parse_sentence : Pcoq.Gram.parsable * in_channel option -> - Util.loc * Vernacexpr.vernac_expr + Pp.loc * Vernacexpr.vernac_expr (** Reads and executes vernac commands from a stream. The boolean [just_parsing] disables interpretation of commands. *) -exception DuringCommandInterp of Util.loc * exn +exception DuringCommandInterp of Pp.loc * exn exception End_of_input val just_parsing : bool ref -val eval_expr : Util.loc * Vernacexpr.vernac_expr -> unit +val eval_expr : Pp.loc * Vernacexpr.vernac_expr -> unit val raw_do_vernac : Pcoq.Gram.parsable -> unit (** Set XML hooks *) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index f7466d037..a7b4a175f 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -9,6 +9,7 @@ (* Concrete syntax of the mathematical vernacular MV V2.6 *) open Pp +open Errors open Util open Flags open Names @@ -65,7 +66,7 @@ let show_proof () = (* spiwack: this would probably be cooler with a bit of polishing. *) let p = Proof_global.give_me_the_proof () in let pprf = Proof.partial_proof p in - msgnl (Util.prlist_with_sep Pp.fnl Printer.pr_constr pprf) + msgnl (Pp.prlist_with_sep Pp.fnl Printer.pr_constr pprf) let show_node () = (* spiwack: I'm have little clue what this function used to do. I deactivated it, @@ -163,7 +164,7 @@ let print_loadpath dir = | Some dir -> List.filter (fun (s,l) -> is_dirpath_prefix_of dir l) l in msgnl (Pp.t (str "Logical Path: " ++ tab () ++ str "Physical path:" ++ fnl () ++ - prlist_with_sep pr_fnl print_path_entry l)) + prlist_with_sep fnl print_path_entry l)) let print_modules () = let opened = Library.opened_libraries () @@ -419,14 +420,14 @@ let vernac_inductive finite infer indl = (((coe', AssumExpr ((loc, Name id), ce)), None), []) in vernac_record (Class true) finite infer id bl c None [f] | [ ( id , bl , c , Class true, _), _ ] -> - Util.error "Definitional classes must have a single method" + Errors.error "Definitional classes must have a single method" | [ ( id , bl , c , Class false, Constructors _), _ ] -> - Util.error "Inductive classes not supported" + Errors.error "Inductive classes not supported" | [ ( _ , _ , _ , _, RecordDecl _ ) , _ ] -> - Util.error "where clause not supported for (co)inductive records" + Errors.error "where clause not supported for (co)inductive records" | _ -> let unpack = function | ( (_, id) , bl , c , _ , Constructors l ) , ntn -> ( id , bl , c , l ) , ntn - | _ -> Util.error "Cannot handle mutually (co)inductive records." + | _ -> Errors.error "Cannot handle mutually (co)inductive records." in let indl = List.map unpack indl in do_mutual_inductive indl (recursivity_flag_of_kind finite) @@ -1416,7 +1417,7 @@ let vernac_show = function | ShowExistentials -> show_top_evars () | ShowTree -> show_prooftree () | ShowProofNames -> - msgnl (prlist_with_sep pr_spc pr_id (Pfedit.get_all_proof_names())) + msgnl (pr_sequence pr_id (Pfedit.get_all_proof_names())) | ShowIntros all -> show_intro all | ShowMatch id -> show_match id | ShowThesis -> show_thesis () diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli index 8fb6f4668..2b6a881d4 100644 --- a/toplevel/vernacentries.mli +++ b/toplevel/vernacentries.mli @@ -51,7 +51,7 @@ val abort_refine : ('a -> unit) -> 'a -> unit;; val interp : Vernacexpr.vernac_expr -> unit -val vernac_reset_name : identifier Util.located -> unit +val vernac_reset_name : identifier Pp.located -> unit val vernac_backtrack : int -> int -> int -> unit diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 78207f6a2..155feaf62 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -7,6 +7,8 @@ (************************************************************************) open Compat +open Errors +open Pp open Util open Names open Tacexpr diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml index 10c5a00f6..c8d6d87ff 100644 --- a/toplevel/vernacinterp.ml +++ b/toplevel/vernacinterp.ml @@ -7,6 +7,7 @@ (************************************************************************) open Pp +open Errors open Util open Names open Libnames diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4 index aa38e9e9f..332d30536 100644 --- a/toplevel/whelp.ml4 +++ b/toplevel/whelp.ml4 @@ -10,7 +10,7 @@ open Flags open Pp -open Util +open Errors open System open Names open Term |