diff options
140 files changed, 34 insertions, 1112 deletions
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4 index a02b7babc..cc378ceda 100644 --- a/grammar/argextend.ml4 +++ b/grammar/argextend.ml4 @@ -11,7 +11,6 @@ open Genarg open Q_util open Egramml -open Pcoq open Compat let loc = Loc.ghost @@ -264,7 +263,6 @@ let declare_vernac_argument loc s pr cl = ($wit$, fun _ _ _ _ -> Errors.anomaly "vernac argument needs not wit printer") } >> ] -open Vernacexpr open Pcoq open Pcaml open PcamlSig diff --git a/grammar/q_constr.ml4 b/grammar/q_constr.ml4 index f4d3c41f6..8943b2b63 100644 --- a/grammar/q_constr.ml4 +++ b/grammar/q_constr.ml4 @@ -8,16 +8,10 @@ (*i camlp4deps: "tools/compat5b.cmo" i*) -open Glob_term -open Term -open Names -open Pattern open Q_util -open Pp open Compat open Pcaml open PcamlSig -open Misctypes let loc = Loc.ghost let dloc = <:expr< Loc.ghost >> @@ -34,9 +28,9 @@ EXTEND <:expr< snd (Patternops.pattern_of_glob_constr $c$) >> ] ] ; sort: - [ [ "Set" -> GSet - | "Prop" -> GProp - | "Type" -> GType None ] ] + [ [ "Set" -> Misctypes.GSet + | "Prop" -> Misctypes.GProp + | "Type" -> Misctypes.GType None ] ] ; ident: [ [ s = string -> <:expr< Names.id_of_string $str:s$ >> ] ] diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4 index aae1d9de2..3d39d13d7 100644 --- a/grammar/q_coqast.ml4 +++ b/grammar/q_coqast.ml4 @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp open Names open Q_util open Compat diff --git a/grammar/q_util.ml4 b/grammar/q_util.ml4 index be021467b..895584703 100644 --- a/grammar/q_util.ml4 +++ b/grammar/q_util.ml4 @@ -8,9 +8,7 @@ (* This file defines standard combinators to build ml expressions *) -open Extrawit open Compat -open Pp let mlexpr_of_list f l = List.fold_right @@ -51,9 +49,6 @@ let mlexpr_of_option f = function | None -> <:expr< None >> | Some e -> <:expr< Some $f e$ >> -open Vernacexpr -open Genarg - let rec mlexpr_of_prod_entry_key = function | Pcoq.Alist1 s -> <:expr< Pcoq.Alist1 $mlexpr_of_prod_entry_key s$ >> | Pcoq.Alist1sep (s,sep) -> <:expr< Pcoq.Alist1sep $mlexpr_of_prod_entry_key s$ $str:sep$ >> diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4 index 3074337f6..db8c51386 100644 --- a/grammar/vernacextend.ml4 +++ b/grammar/vernacextend.ml4 @@ -10,9 +10,7 @@ open Pp open Util -open Genarg open Q_util -open Q_coqast open Argextend open Tacextend open Pcoq diff --git a/interp/constrintern.ml b/interp/constrintern.ml index a2be41700..c204db0e0 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -110,13 +110,11 @@ let global_reference_in_absolute_module dir id = type internalization_error = | VariableCapture of identifier * identifier - | WrongExplicitImplicit | IllegalMetavariable | NotAConstructor of reference | UnboundFixName of bool * identifier | NonLinearPattern of identifier | BadPatternsNumber of int * int - | BadExplicitationNumber of explicitation * int option exception InternalizationError of Loc.t * internalization_error @@ -124,10 +122,6 @@ let explain_variable_capture id id' = pr_id id ++ str " is dependent in the type of " ++ pr_id id' ++ strbrk ": cannot interpret both of them with the same type" -let explain_wrong_explicit_implicit = - str "Found an explicitly given implicit argument but was expecting" ++ - fnl () ++ str "a regular one" - let explain_illegal_metavariable = str "Metavariables allowed only in patterns" @@ -146,32 +140,15 @@ let explain_bad_patterns_number n1 n2 = str "Expecting " ++ int n1 ++ str (plural n1 " pattern") ++ str " but found " ++ int n2 -let explain_bad_explicitation_number n po = - match n with - | ExplByPos (n,_id) -> - let s = match po with - | None -> str "a regular argument" - | Some p -> int p in - str "Bad explicitation number: found " ++ int n ++ - str" but was expecting " ++ s - | ExplByName id -> - let s = match po with - | None -> str "a regular argument" - | Some p -> (*pr_id (name_of_position p) in*) failwith "" in - str "Bad explicitation name: found " ++ pr_id id ++ - str" but was expecting " ++ s - let explain_internalization_error e = let pp = match e with | VariableCapture (id,id') -> explain_variable_capture id id' - | WrongExplicitImplicit -> explain_wrong_explicit_implicit | IllegalMetavariable -> explain_illegal_metavariable | NotAConstructor ref -> explain_not_a_constructor ref | UnboundFixName (iscofix,id) -> explain_unbound_fix_name iscofix id | NonLinearPattern id -> explain_non_linear_pattern id | BadPatternsNumber (n1,n2) -> explain_bad_patterns_number n1 n2 - | BadExplicitationNumber (n,po) -> explain_bad_explicitation_number n po in - pp ++ str "." + in pp ++ str "." let error_bad_inductive_type loc = user_err_loc (loc,"",str @@ -283,10 +260,6 @@ let error_inconsistent_scope loc id scopes1 scopes2 = pr_scope_stack scopes2 ++ strbrk " while it was elsewhere used in " ++ pr_scope_stack scopes1) -let error_expect_constr_notation_type loc id = - user_err_loc (loc,"", - pr_id id ++ str " is bound in the notation to a term variable.") - let error_expect_binder_notation_type loc id = user_err_loc (loc,"", pr_id id ++ @@ -786,12 +759,6 @@ let product_of_cases_patterns ids idspl = List.map (fun (subst',ptail) -> (subst@subst',p::ptail)) ptaill) pl))) idspl (ids,[[],[]]) -let simple_product_of_cases_patterns pl = - List.fold_right (fun pl ptaill -> - List.flatten (List.map (fun (subst,p) -> - List.map (fun (subst',ptail) -> (subst@subst',p::ptail)) ptaill) pl)) - pl [[],[]] - (* @return the first variable that occurs twice in a pattern naive n2 algo *) @@ -1769,8 +1736,6 @@ open Environ let my_intern_constr sigma env lvar acc c = internalize sigma env acc false lvar c -let my_intern_type sigma env lvar acc c = my_intern_constr sigma env lvar (set_type_scope acc) c - let intern_context global_level sigma env impl_env params = try let lvar = (([],[]), []) in diff --git a/interp/modintern.ml b/interp/modintern.ml index 0f386ec04..f91d9ff22 100644 --- a/interp/modintern.ml +++ b/interp/modintern.ml @@ -6,9 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors -open Util -open Names open Entries open Libnames open Constrexpr @@ -28,8 +25,6 @@ val error_not_a_functor : module_struct_entry -> 'a val error_not_equal : module_path -> module_path -> 'a -val error_result_must_be_signature : unit -> 'a - oval error_not_a_modtype_loc : loc -> string -> 'a val error_not_a_module_loc : loc -> string -> 'a @@ -41,9 +36,6 @@ val error_with_in_module : unit -> 'a val error_application_to_module_type : unit -> 'a *) -let error_result_must_be_signature () = - error "The result module type must be a signature." - let error_not_a_modtype_loc loc s = Loc.raise loc (Modops.ModuleTypingError (Modops.NotAModuleType s)) @@ -60,53 +52,6 @@ let error_application_to_module_type loc = Loc.raise loc (ModuleInternalizationError IncorrectModuleApplication) - - -let rec make_mp mp = function - [] -> mp - | h::tl -> make_mp (MPdot(mp, label_of_id h)) tl - -(* -(* Since module components are not put in the nametab we try to locate -the module prefix *) -exception BadRef - -let lookup_qualid (modtype:bool) qid = - let rec make_mp mp = function - [] -> mp - | h::tl -> make_mp (MPdot(mp, label_of_id h)) tl - in - let rec find_module_prefix dir n = - if n<0 then raise Not_found; - let dir',dir'' = List.chop n dir in - let id',dir''' = - match dir'' with - | hd::tl -> hd,tl - | _ -> anomaly "This list should not be empty!" - in - let qid' = make_qualid dir' id' in - try - match Nametab.locate qid' with - | ModRef mp -> mp,dir''' - | _ -> raise BadRef - with - Not_found -> find_module_prefix dir (pred n) - in - try Nametab.locate qid - with Not_found -> - let (dir,id) = repr_qualid qid in - let pref_mp,dir' = find_module_prefix dir (List.length dir - 1) in - let mp = - List.fold_left (fun mp id -> MPdot (mp, label_of_id id)) pref_mp dir' - in - if modtype then - ModTypeRef (make_ln mp (label_of_id id)) - else - ModRef (MPdot (mp,label_of_id id)) - -*) - - (* Search for the head of [qid] in [binders]. If found, returns the module_path/kernel_name created from the dirpath and the basename. Searches Nametab otherwise. diff --git a/interp/notation.ml b/interp/notation.ml index 46a06b700..d7f539f2f 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -399,8 +399,6 @@ let interp_notation loc ntn local_scopes = user_err_loc (loc,"",str ("Unknown interpretation for notation \""^ntn^"\".")) -let isGApp = function GApp _ -> true | _ -> false - let uninterp_notations c = List.map_append (fun key -> Gmapl.find key !notations_key_table) (glob_constr_keys c) diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml index b38177d48..adf611b56 100644 --- a/interp/smartlocate.ml +++ b/interp/smartlocate.ml @@ -14,7 +14,6 @@ (* *) open Pp open Errors -open Util open Libnames open Globnames open Misctypes diff --git a/interp/topconstr.ml b/interp/topconstr.ml index abdde1f54..dd656d479 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -20,7 +20,7 @@ open Constrexpr_ops let oldfashion_patterns = ref (true) -let write_oldfashion_patterns = Goptions.declare_bool_option { +let _ = Goptions.declare_bool_option { Goptions.optsync = true; Goptions.optdepr = false; Goptions.optname = "Constructors in patterns require all their arguments but no parameters instead of explicit parameters and arguments"; @@ -244,18 +244,6 @@ let rec replace_vars_constr_expr l = function | c -> map_constr_expr_with_binders List.remove_assoc replace_vars_constr_expr l c -(**********************************************************************) -(* Concrete syntax for modules and modules types *) - -type with_declaration_ast = - | CWith_Module of identifier list Loc.located * qualid Loc.located - | CWith_Definition of identifier list Loc.located * constr_expr - -type module_ast = - | CMident of qualid Loc.located - | CMapply of Loc.t * module_ast * module_ast - | CMwith of Loc.t * module_ast * with_declaration_ast - (* Returns the ranges of locs of the notation that are not occupied by args *) (* and which are then occupied by proper symbols of the notation (or spaces) *) diff --git a/intf/misctypes.mli b/intf/misctypes.mli index 97b4b45fe..f46ada445 100644 --- a/intf/misctypes.mli +++ b/intf/misctypes.mli @@ -7,7 +7,6 @@ (************************************************************************) open Names -open Libnames (** Basic types used both in [constr_expr] and in [glob_constr] *) @@ -60,7 +59,6 @@ type 'a cast_type = | CastVM of 'a | CastCoerce (** Cast to a base type (eg, an underlying inductive type) *) - (** Bindings *) type quantified_hypothesis = AnonHyp of int | NamedHyp of identifier diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index 8d09cbd7e..82250badb 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -94,7 +94,6 @@ let annot_tbl = Hashtbl.create 31 exception NotEvaluated -open Pp let key rk = match !rk with | Some k -> (*Pp.msgnl (str"found at: "++int k);*) k diff --git a/kernel/modops.ml b/kernel/modops.ml index 2f7d480af..1bef6bf50 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -98,9 +98,6 @@ let error_no_module_to_end _ = let error_no_modtype_to_end _ = raise (ModuleTypingError NoModuleTypeToEnd) -let error_not_a_modtype s = - raise (ModuleTypingError (NotAModuleType s)) - let error_not_a_module s = raise (ModuleTypingError (NotAModule s)) diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml index ffa1d304e..6e5a45b9c 100644 --- a/kernel/pre_env.ml +++ b/kernel/pre_env.ml @@ -106,8 +106,6 @@ let push_named_context_val d (ctxt,vals) = let rval = ref VKnone in Sign.add_named_decl d ctxt, (id,rval)::vals -exception ASSERT of rel_context - let push_named d env = (* if not (env.env_rel_context = []) then raise (ASSERT env.env_rel_context); assert (env.env_rel_context = []); *) diff --git a/kernel/term.ml b/kernel/term.ml index 42309c37e..0937fc16b 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -828,7 +828,6 @@ let subst1 lam = substl [lam] let substnl_decl laml k = map_rel_declaration (substnl laml k) let substl_decl laml = substnl_decl laml 0 let subst1_decl lam = substl_decl [lam] -let substnl_named laml k = map_named_declaration (substnl laml k) let substl_named_decl = substl_decl let subst1_named_decl = subst1_decl diff --git a/kernel/univ.ml b/kernel/univ.ml index faadb1081..f1fc8bda5 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -29,8 +29,6 @@ open Util union-find algorithm. The assertions $<$ and $\le$ are represented by adjacency lists *) -let compare_ints (x:int) (y:int) = Pervasives.compare x y - module UniverseLevel = struct type t = diff --git a/lib/cList.ml b/lib/cList.ml index 2bf8d3597..62d1ec3c1 100644 --- a/lib/cList.ml +++ b/lib/cList.ml @@ -550,13 +550,6 @@ let rec sep_last = function | hd::[] -> (hd,[]) | hd::tl -> let (l,tl) = sep_last tl in (l,hd::tl) -let try_find_i f = - let rec try_find_f n = function - | [] -> failwith "try_find_i" - | h::t -> try f n h with Failure _ -> try_find_f (n+1) t - in - try_find_f - let rec find_map f = function | [] -> raise Not_found | x :: l -> @@ -670,11 +663,6 @@ let rec split3 = function | (x,y,z)::l -> let (rx, ry, rz) = split3 l in (x::rx, y::ry, z::rz) -let rec insert_in_class f a = function - | [] -> [[a]] - | (b::_ as l)::classes when f a b -> (a::l)::classes - | l::classes -> l :: insert_in_class f a classes - let firstn n l = let rec aux acc = function | (0, l) -> List.rev acc diff --git a/lib/dyn.ml b/lib/dyn.ml index 13d1ec060..de5158b14 100644 --- a/lib/dyn.ml +++ b/lib/dyn.ml @@ -7,7 +7,6 @@ (************************************************************************) open Errors -open Util (* Dynamics, programmed with DANGER !!! *) diff --git a/lib/gmapl.ml b/lib/gmapl.ml index 5e8f27dc7..4be8f4baf 100644 --- a/lib/gmapl.ml +++ b/lib/gmapl.ml @@ -6,7 +6,6 @@ (* * 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/serialize.ml b/lib/serialize.ml index 3ad508d74..76a8b2c06 100644 --- a/lib/serialize.ml +++ b/lib/serialize.ml @@ -67,7 +67,6 @@ let goals : goals option call = Goal let evars : evar list option call = Evars let hints : (hint list * hint) option call = Hints let status : status call = Status -let search flags : string coq_object list call = Search flags let get_options : (option_name * option_state) list call = GetOptions let set_options l : unit call = SetOptions l let inloadpath s : bool call = InLoadPath s @@ -125,10 +124,6 @@ let do_match constr t mf = match constr with else raise Marshal_error | _ -> raise Marshal_error -let pcdata = function -| PCData s -> s -| _ -> raise Marshal_error - let singleton = function | [x] -> x | _ -> raise Marshal_error diff --git a/lib/store.ml b/lib/store.ml index bc1b335fd..ad6595ade 100644 --- a/lib/store.ml +++ b/lib/store.ml @@ -11,16 +11,6 @@ (* We give a short implementation of a universal type. This is mostly equivalent to what is proposed by module Dyn.ml, except that it requires no explicit tag. *) -module type Universal = sig - type t - - type 'a etype = { - put : 'a -> t ; - get : t -> 'a option - } - - val embed : unit -> 'a etype -end (* We use a dynamic "name" allocator. But if we needed to serialise stores, we might want something static to avoid troubles with plugins order. *) diff --git a/lib/system.ml b/lib/system.ml index cf650d6ab..6076217b3 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -92,8 +92,6 @@ let is_in_path lpath filename = try ignore (where_in_path ~warn:false lpath filename); true with Not_found -> false -let path_separator = if Sys.os_type = "Unix" then ':' else ';' - let is_in_system_path filename = let path = try Sys.getenv "PATH" with Not_found -> error "system variable PATH not found" in diff --git a/lib/util.ml b/lib/util.ml index 624075956..af3b13fa7 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -24,11 +24,6 @@ let pi1 (a,_,_) = a let pi2 (_,a,_) = a let pi3 (_,_,a) = a -(* Projection operator *) - -let down_fst f x = f (fst x) -let down_snd f x = f (snd x) - (* Characters *) let is_letter c = (c >= 'a' && c <= 'z') or (c >= 'A' && c <= 'Z') diff --git a/lib/xml_parser.ml b/lib/xml_parser.ml index 6207763cd..783f5c91b 100644 --- a/lib/xml_parser.ml +++ b/lib/xml_parser.ml @@ -98,7 +98,6 @@ let make source = } let check_eof p v = p.check_eof <- v -let concat_pcdata p v = p.concat_pcdata <- v let pop s = try diff --git a/library/declaremods.ml b/library/declaremods.ml index a61e59d6d..fef95bc61 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -15,7 +15,6 @@ open Entries open Libnames open Libobject open Lib -open Nametab open Mod_subst (** Rigid / flexible signature *) diff --git a/library/dischargedhypsmap.ml b/library/dischargedhypsmap.ml index 9dbbc947d..c26f652df 100644 --- a/library/dischargedhypsmap.ml +++ b/library/dischargedhypsmap.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Util open Libnames type discharged_hyps = full_path list diff --git a/library/global.ml b/library/global.ml index 2d958f799..c2bd55128 100644 --- a/library/global.ml +++ b/library/global.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Util open Names open Term open Environ diff --git a/library/globnames.ml b/library/globnames.ml index 27683278b..8d298bc94 100644 --- a/library/globnames.ml +++ b/library/globnames.ml @@ -7,7 +7,6 @@ (************************************************************************) open Errors -open Util open Names open Term open Mod_subst diff --git a/library/goptions.ml b/library/goptions.ml index a78ca750d..2a97f6149 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -199,8 +199,6 @@ type 'a option_sig = { optread : unit -> 'a; optwrite : 'a -> unit } -type option_type = bool * (unit -> option_value) -> (option_value -> unit) - module OptionMap = Map.Make (struct type t = option_name let compare = compare end) diff --git a/library/impargs.ml b/library/impargs.ml index cc4a4e45e..767e0e73a 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -377,8 +377,6 @@ let compute_semi_auto_implicits env f manual t = let _,autoimpls = compute_auto_implicits env f f.auto t in [DefaultImpArgs, set_manual_implicits env f f.auto autoimpls manual] -let compute_implicits env t = compute_semi_auto_implicits env !implicit_args [] t - (*s Constants. *) let compute_constant_implicits flags manual cst = diff --git a/library/lib.ml b/library/lib.ml index a8a9f0c26..688df5a0e 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -166,13 +166,6 @@ let find_entry_p p = in find !lib_stk -let find_split_p p = - let rec find = function - | [] -> raise Not_found - | ent::l -> if p ent then ent,l else find l - in - find !lib_stk - let split_lib_gen test = let rec collect after equal = function | hd::before when test hd -> collect after (hd::equal) before @@ -571,12 +564,10 @@ let set_lib_stk new_lib_stk = with | Not_found -> error "Tried to set environment to an incoherent state." -let reset_to_gen test = +let reset_to test = let (_,_,before) = split_lib_gen test in set_lib_stk before -let reset_to sp = reset_to_gen (fun x -> fst x = sp) - let first_command_label = 1 let mark_end_of_command, current_command_label, reset_command_label = @@ -599,7 +590,7 @@ let is_label_n n x = let reset_label n = if n >= current_command_label () then error "Cannot backtrack to the current label or a future one"; - reset_to_gen (is_label_n n); + reset_to (is_label_n n); (* forget state numbers after n only if reset succeeded *) reset_command_label n diff --git a/library/libobject.ml b/library/libobject.ml index 18b4c0c65..ffd87ce80 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -7,7 +7,6 @@ (************************************************************************) open Errors -open Util open Libnames open Mod_subst diff --git a/library/library.ml b/library/library.ml index 9c881e515..7dfde63a7 100644 --- a/library/library.ml +++ b/library/library.ml @@ -496,8 +496,6 @@ let rec_intern_library_from_file idopt f = which recursively loads its dependencies) *) -type library_reference = dir_path list * bool option - let register_library m = Declaremods.register_library m.library_name diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index 880d4b8ce..ade579c69 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -272,9 +272,9 @@ let recover_notation_grammar ntn prec = (* Summary functions: the state of the lexer is included in that of the parser. Because the grammar affects the set of keywords when adding or removing grammar rules. *) -type frozen_t = all_grammar_command list * Lexer.frozen_t +type frozen_t = (int * all_grammar_command) list * Lexer.frozen_t -let freeze () = (!grammar_state, Lexer.freeze ()) +let freeze () : frozen_t = (!grammar_state, Lexer.freeze ()) (* We compare the current state of the grammar and the state to unfreeze, by computing the longest common suffixes *) diff --git a/parsing/extrawit.ml b/parsing/extrawit.ml index 75205c964..be584b5c8 100644 --- a/parsing/extrawit.ml +++ b/parsing/extrawit.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors -open Util open Genarg (* This file defines extra argument types *) @@ -30,7 +28,7 @@ let wit_tactic = function | 3 -> wit_tactic3 | 4 -> wit_tactic4 | 5 -> wit_tactic5 - | n -> anomaly ("Unavailable tactic level: "^string_of_int n) + | n -> Errors.anomaly ("Unavailable tactic level: "^string_of_int n) let globwit_tactic = function | 0 -> globwit_tactic0 @@ -39,7 +37,7 @@ let globwit_tactic = function | 3 -> globwit_tactic3 | 4 -> globwit_tactic4 | 5 -> globwit_tactic5 - | n -> anomaly ("Unavailable tactic level: "^string_of_int n) + | n -> Errors.anomaly ("Unavailable tactic level: "^string_of_int n) let rawwit_tactic = function | 0 -> rawwit_tactic0 @@ -48,7 +46,7 @@ let rawwit_tactic = function | 3 -> rawwit_tactic3 | 4 -> rawwit_tactic4 | 5 -> rawwit_tactic5 - | n -> anomaly ("Unavailable tactic level: "^string_of_int n) + | n -> Errors.anomaly ("Unavailable tactic level: "^string_of_int n) let tactic_genarg_level s = if String.length s = 7 && String.sub s 0 6 = "tactic" then diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index bc2803ae5..6506af0a1 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -6,10 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp open Constrexpr open Tacexpr -open Vernacexpr open Misctypes open Genredexpr open Tok diff --git a/parsing/g_obligations.ml4 b/parsing/g_obligations.ml4 index 2e83f7163..a0ea5c6de 100644 --- a/parsing/g_obligations.ml4 +++ b/parsing/g_obligations.ml4 @@ -13,12 +13,6 @@ Elaborated from correctness/psyntax.ml4 by Jean-Christophe Filliâtre *) -open Flags -open Util -open Names -open Nameops -open Reduction -open Term open Libnames open Constrexpr open Constrexpr_ops @@ -38,13 +32,8 @@ struct let withtac : Tacexpr.raw_tactic_expr option Gram.entry = gec "withtac" end -open Glob_term open ObligationsGram -open Util -open Tok open Pcoq -open Prim -open Constr let sigref = mkRefC (Qualid (Loc.ghost, Libnames.qualid_of_string "Coq.Init.Specif.sig")) diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index e9b91dbbf..6d82a6504 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -18,8 +18,6 @@ open Extend open Vernacexpr open Locality open Decl_kinds -open Genarg -open Goptions open Declaremods open Misctypes diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4 index 1527fa64b..37d2b332d 100644 --- a/parsing/g_xml.ml4 +++ b/parsing/g_xml.ml4 @@ -10,10 +10,8 @@ open Pp open Errors open Util open Names -open Term open Pcoq open Glob_term -open Genarg open Tacexpr open Libnames open Globnames diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index 3a0840a7e..04b5e4673 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -11,11 +11,7 @@ open Compat open Tok open Errors open Util -open Names open Extend -open Libnames -open Glob_term -open Topconstr open Genarg open Tacexpr open Extrawit @@ -111,7 +107,6 @@ let weaken_entry x = Gramobj.weaken_entry x module type Gramtypes = sig - open Decl_kinds val inGramObj : 'a raw_abstract_argument_type -> 'a G.entry -> typed_entry val outGramObj : 'a raw_abstract_argument_type -> typed_entry -> 'a G.entry end @@ -475,7 +470,6 @@ let level_stack = (* At a same level, LeftA takes precedence over RightA and NoneA *) (* In case, several associativity exists for a level, we make two levels, *) (* first LeftA, then RightA and NoneA together *) -open Ppextend let admissible_assoc = function | LeftA, Some (RightA | NonA) -> false diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index 40599b827..89e30a8ee 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -58,8 +58,6 @@ module ST=struct let query sign st=Hashtbl.find st.toterm sign - let rev_query term st=Hashtbl.find st.tosign term - let delete st t= try let sign=Hashtbl.find st.tosign t in Hashtbl.remove st.toterm sign; diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml index d5eab32c4..25c01f2bd 100644 --- a/plugins/cc/ccproof.ml +++ b/plugins/cc/ccproof.ml @@ -10,7 +10,6 @@ (* proof-trees that will be transformed into proof-terms in cctac.ml4 *) open Errors -open Util open Names open Term open Ccalgo diff --git a/plugins/cc/g_congruence.ml4 b/plugins/cc/g_congruence.ml4 index 78273dabc..c2c437c80 100644 --- a/plugins/cc/g_congruence.ml4 +++ b/plugins/cc/g_congruence.ml4 @@ -9,8 +9,6 @@ (*i camlp4deps: "grammar/grammar.cma" i*) open Cctac -open Tactics -open Tacticals (* Tactic registration *) diff --git a/plugins/decl_mode/decl_mode.ml b/plugins/decl_mode/decl_mode.ml index f29964c69..1f55257e5 100644 --- a/plugins/decl_mode/decl_mode.ml +++ b/plugins/decl_mode/decl_mode.ml @@ -12,7 +12,6 @@ open Evd open Errors open Util - let daimon_flag = ref false let set_daimon_flag () = daimon_flag:=true diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index 1a0d05047..367e02bf8 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -11,7 +11,6 @@ open Util open Pp open Evd -open Proof_type open Tacmach open Tacinterp open Decl_expr @@ -129,22 +128,6 @@ let daimon_tac gls = set_daimon_flag (); {it=[];sigma=sig_sig gls} - -(* marking closed blocks *) - -let rec is_focussing_instr = function - Pthus i | Pthen i | Phence i -> is_focussing_instr i - | Pescape | Pper _ | Pclaim _ | Pfocus _ - | Psuppose _ | Pcase (_,_,_) -> true - | _ -> false - -let mark_rule_as_done = function - Decl_proof true -> Decl_proof false - | Decl_proof false -> - anomaly "already marked as done" - | _ -> anomaly "mark_rule_as_done" - - (* post-instruction focus management *) (* spiwack: This used to fail if there was no focusing command diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4 index 3eaf81d2b..e8e81c472 100644 --- a/plugins/decl_mode/g_decl_mode.ml4 +++ b/plugins/decl_mode/g_decl_mode.ml4 @@ -14,13 +14,10 @@ open Pp open Tok open Decl_expr open Names -open Term -open Genarg open Pcoq open Pcoq.Constr open Pcoq.Tactic -open Pcoq.Vernac_ let pr_goal gs = let (g,sigma) = Goal.V82.nf_evar (Tacmach.project gs) (Evd.sig_it gs) in diff --git a/plugins/decl_mode/ppdecl_proof.ml b/plugins/decl_mode/ppdecl_proof.ml index b72476a75..01f32e4a3 100644 --- a/plugins/decl_mode/ppdecl_proof.ml +++ b/plugins/decl_mode/ppdecl_proof.ml @@ -7,7 +7,6 @@ (************************************************************************) open Errors -open Util open Pp open Decl_expr open Names diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 2baea11a3..f49b1f375 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -70,16 +70,12 @@ module type VISIT = sig (* Reset the dependencies by emptying the visit lists *) val reset : unit -> unit - (* Add the module_path and all its prefixes to the mp visit list *) - val add_mp : module_path -> unit - - (* Same, but we'll keep all fields of these modules *) + (* Add the module_path and all its prefixes to the mp visit list. + We'll keep all fields of these modules. *) val add_mp_all : module_path -> unit - (* Add kernel_name / constant / reference / ... in the visit lists. + (* Add reference / ... in the visit lists. These functions silently add the mp of their arg in the mp list *) - val add_ind : mutual_inductive -> unit - val add_con : constant -> unit val add_ref : global_reference -> unit val add_decl_deps : ml_decl -> unit val add_spec_deps : ml_spec -> unit diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4 index 58e9a5220..bdb102b18 100644 --- a/plugins/extraction/g_extraction.ml4 +++ b/plugins/extraction/g_extraction.ml4 @@ -10,8 +10,6 @@ (* ML names *) -open Vernacexpr -open Pcoq open Genarg open Pp open Names diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml index 4fd9f17ee..33da06f01 100644 --- a/plugins/extraction/haskell.ml +++ b/plugins/extraction/haskell.ml @@ -13,7 +13,6 @@ open Errors open Util open Names open Nameops -open Libnames open Globnames open Table open Miniml @@ -82,10 +81,6 @@ let pp_global k r = (*s Pretty-printing of types. [par] is a boolean indicating whether parentheses are needed or not. *) -let kn_sig = - let specif = MPfile (dirpath_of_string "Coq.Init.Specif") in - make_mind specif empty_dirpath (mk_label "sig") - let rec pp_type par vl t = let rec pp_rec par = function | Tmeta _ | Tvar' _ -> assert false diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index e3abab82b..b53fec23e 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -224,21 +224,6 @@ let type_maxvar t = | _ -> n in parse 0 t -(*s What are the type variables occurring in [t]. *) - -let intset_union_map_list f l = - List.fold_left (fun s t -> Intset.union s (f t)) Intset.empty l - -let intset_union_map_array f a = - Array.fold_left (fun s t -> Intset.union s (f t)) Intset.empty a - -let rec type_listvar = function - | Tmeta {contents = Some t} -> type_listvar t - | Tvar i | Tvar' i -> Intset.singleton i - | Tarr (a,b) -> Intset.union (type_listvar a) (type_listvar b) - | Tglob (_,l) -> intset_union_map_list type_listvar l - | _ -> Intset.empty - (*s From [a -> b -> c] to [[a;b],c]. *) let rec type_decomp = function diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index 9247baba2..4a390128a 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -289,8 +289,6 @@ and optim_me to_appear s = function For non-library extraction, we recompute a minimal set of dependencies for first-level objects *) -exception NoDepCheck - let base_r = function | ConstRef c as r -> r | IndRef (kn,_) -> IndRef (kn,0) diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index 59a820bc0..303932484 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -12,11 +12,8 @@ open Formula open Sequent open Ground open Goptions -open Tactics open Tacticals open Tacinterp -open Term -open Names open Libnames (* declaring search depth as a global option *) diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index c648939bb..238813e39 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -48,8 +48,6 @@ let priority = (* pure heuristics, <=0 for non reversible *) | LLexists (_,_) -> 50 | LLarrow (_,_,_) -> -10 -let left_reversible lpat=(priority lpat)>0 - module OrderedFormula= struct type t=Formula.t @@ -163,8 +161,6 @@ let find_left t seq=List.hd (CM.find t seq.context) left_reversible lpat with Heap.EmptyHeap -> false *) -let no_formula seq= - seq.redexes=HP.empty let rec take_formula seq= let hd=HP.maximum seq.redexes diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index b45932e57..429a0a4a8 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -14,7 +14,6 @@ des inéquations et équations sont entiers. En attendant la tactique Field. open Term open Tactics -open Clenv open Names open Libnames open Globnames @@ -76,7 +75,6 @@ let flin_emult a f = ;; (*****************************************************************************) -open Vernacexpr type ineq = Rlt | Rle | Rgt | Rge diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 3505c4d9b..52b4d881a 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -134,19 +134,6 @@ let refine c = let thin l = Tacmach.thin_no_check l - -let cut_replacing id t tac :tactic= - tclTHENS (cut t) - [ tclTHEN (thin_no_check [id]) (introduction_no_check id); - tac - ] - -let intro_erasing id = tclTHEN (thin [id]) (introduction id) - - - -let rec_hyp_id = id_of_string "rec_hyp" - let is_trivial_eq t = let res = try begin @@ -367,7 +354,7 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type = new_ctxt,new_end_of_type,simpl_eq_tac -let is_property ptes_info t_x full_type_of_hyp = +let is_property (ptes_info:ptes_info) t_x full_type_of_hyp = if isApp t_x then let pte,args = destApp t_x in @@ -563,7 +550,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = thin [hyp_id],[] -let clean_goal_with_heq ptes_infos continue_tac dyn_infos = +let clean_goal_with_heq ptes_infos continue_tac (dyn_infos:body_info) = fun g -> let env = pf_env g and sigma = project g @@ -894,13 +881,6 @@ let build_proof (* Proof of principles from structural functions *) -let is_pte_type t = - isSort ((strip_prod t)) - -let is_pte (_,_,t) = is_pte_type t - - - type static_fix_info = { @@ -932,9 +912,6 @@ let prove_rec_hyp fix_info = is_valid = fun _ -> true } - -exception Not_Rec - let generalize_non_dep hyp g = (* observe (str "rec id := " ++ Ppconstr.pr_id hyp); *) let hyps = [hyp] in @@ -1427,17 +1404,6 @@ let backtrack_eqs_until_hrec hrec eqs : tactic = backtrack gls - -let build_clause eqs = - { - Locus.onhyps = - Some (List.map - (fun id -> (Locus.AllOccurrences, id), Locus.InHyp) - eqs - ); - Locus.concl_occs = Locus.NoOccurrences - } - let rec rewrite_eqs_in_eqs eqs = match eqs with | [] -> tclIDTAC diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index b97fc48f1..a14b47393 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -289,22 +289,6 @@ let change_property_sort toSort princ princName = let pp_dur time time' = str (string_of_float (System.time_difference time time')) -(* let qed () = save_named true *) -let defined () = - try - Lemmas.save_named false - with - | UserError("extract_proof",msg) -> - Errors.errorlabstrm - "defined" - ((try - str "On goal : " ++ fnl () ++ pr_open_subgoals () ++ fnl () - with _ -> mt () - ) ++msg) - | e -> raise e - - - let build_functional_principle interactive_proof old_princ_type sorts funs i proof_tac hook = (* First we get the type of the old graph principle *) let mutr_nparams = (compute_elim_sig old_princ_type).nparams in diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index dccbfa3b5..77c6dc493 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -14,9 +14,7 @@ open Constrexpr open Indfun_common open Indfun open Genarg -open Pcoq open Tacticals -open Constr open Misctypes open Miscops diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index b820489f5..61390bb1a 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -288,10 +288,6 @@ let make_discr_match brl = make_discr_match_el el, make_discr_match_brl i brl) -let pr_name = function - | Name id -> Ppconstr.pr_id id - | Anonymous -> str "_" - (**********************************************************************) (* functions used to build case expression from lettuple and if ones *) (**********************************************************************) @@ -326,40 +322,6 @@ let build_constructors_of_type ind' argl = ) ind.Declarations.mind_consnames -(* [find_type_of] very naive attempts to discover the type of an if or a letin *) -let rec find_type_of nb b = - let f,_ = glob_decompose_app b in - match f with - | GRef(_,ref) -> - begin - let ind_type = - match ref with - | VarRef _ | ConstRef _ -> - let constr_of_ref = constr_of_global ref in - let type_of_ref = Typing.type_of (Global.env ()) Evd.empty constr_of_ref in - let (_,ret_type) = Reduction.dest_prod (Global.env ()) type_of_ref in - let ret_type,_ = decompose_app ret_type in - if not (isInd ret_type) then - begin -(* Pp.msgnl (str "not an inductive" ++ pr_lconstr ret_type); *) - raise (Invalid_argument "not an inductive") - end; - destInd ret_type - | IndRef ind -> ind - | ConstructRef c -> fst c - in - let _,ind_type_info = Inductive.lookup_mind_specif (Global.env()) ind_type in - if not (Array.length ind_type_info.Declarations.mind_consnames = nb ) - then raise (Invalid_argument "find_type_of : not a valid inductive"); - ind_type - end - | GCast(_,b,_) -> find_type_of nb b - | GApp _ -> assert false (* we have decomposed any application via glob_decompose_app *) - | _ -> raise (Invalid_argument "not a ref") - - - - (******************) (* Main functions *) (******************) diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index edc727a48..48ed14473 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -21,7 +21,7 @@ let is_rec_info scheme_info = Util.Intset.exists (fun i -> i >= min && i< max) free_rels_in_br ) in - Util.List.fold_left_i test_branche 1 false (List.rev scheme_info.Tactics.branches) + List.fold_left_i test_branche 1 false (List.rev scheme_info.Tactics.branches) let choose_dest_or_ind scheme_info = if is_rec_info scheme_info @@ -496,64 +496,6 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas let map_option f = function | None -> None | Some v -> Some (f v) - -let decompose_lambda_n_assum_constr_expr = - let rec decompose_lambda_n_assum_constr_expr acc n e = - if n = 0 then (List.rev acc,e) - else - match e with - | Constrexpr.CLambdaN(_, [],e') -> decompose_lambda_n_assum_constr_expr acc n e' - | Constrexpr.CLambdaN(lambda_loc,(nal,bk,nal_type)::bl,e') -> - let nal_length = List.length nal in - if nal_length <= n - then - decompose_lambda_n_assum_constr_expr - (Constrexpr.LocalRawAssum(nal,bk,nal_type)::acc) - (n - nal_length) - (Constrexpr.CLambdaN(lambda_loc,bl,e')) - else - let nal_keep,nal_expr = List.chop n nal in - (List.rev (Constrexpr.LocalRawAssum(nal_keep,bk,nal_type)::acc), - Constrexpr.CLambdaN(lambda_loc,(nal_expr,bk,nal_type)::bl,e') - ) - | Constrexpr.CLetIn(_, na,nav,e') -> - decompose_lambda_n_assum_constr_expr - (Constrexpr.LocalRawDef(na,nav)::acc) (pred n) e' - | _ -> error "Not enough product or assumption" - in - decompose_lambda_n_assum_constr_expr [] - -let decompose_prod_n_assum_constr_expr = - let rec decompose_prod_n_assum_constr_expr acc n e = - (* Pp.msgnl (str "n := " ++ int n ++ fnl ()++ *) - (* str "e := " ++ Ppconstr.pr_lconstr_expr e); *) - if n = 0 then - (* let _ = Pp.msgnl (str "return_type := " ++ Ppconstr.pr_lconstr_expr e) in *) - (List.rev acc,e) - else - match e with - | Constrexpr.CProdN(_, [],e') -> decompose_prod_n_assum_constr_expr acc n e' - | Constrexpr.CProdN(lambda_loc,(nal,bk,nal_type)::bl,e') -> - let nal_length = List.length nal in - if nal_length <= n - then - (* let _ = Pp.msgnl (str "first case") in *) - decompose_prod_n_assum_constr_expr - (Constrexpr.LocalRawAssum(nal,bk,nal_type)::acc) - (n - nal_length) - (if bl = [] then e' else (Constrexpr.CLambdaN(lambda_loc,bl,e'))) - else - (* let _ = Pp.msgnl (str "second case") in *) - let nal_keep,nal_expr = List.chop n nal in - (List.rev (Constrexpr.LocalRawAssum(nal_keep,bk,nal_type)::acc), - Constrexpr.CLambdaN(lambda_loc,(nal_expr,bk,nal_type)::bl,e') - ) - | Constrexpr.CLetIn(_, na,nav,e') -> - decompose_prod_n_assum_constr_expr - (Constrexpr.LocalRawDef(na,nav)::acc) (pred n) e' - | _ -> error "Not enough product or assumption" - in - decompose_prod_n_assum_constr_expr [] open Constrexpr open Topconstr diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 2817c549d..fb9116cc2 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -131,12 +131,6 @@ let coq_constant s = Coqlib.gen_constant_in_modules "RecursiveDefinition" Coqlib.init_modules s;; -let constant sl s = - constr_of_global - (Nametab.locate (make_qualid(Names.make_dirpath - (List.map id_of_string (List.rev sl))) - (id_of_string s)));; - let find_reference sl s = (Nametab.locate (make_qualid(Names.make_dirpath (List.map id_of_string (List.rev sl))) @@ -277,7 +271,6 @@ let cache_Function (_,finfos) = let load_Function _ = cache_Function -let open_Function _ = cache_Function let subst_Function (subst,finfos) = let do_subst_con c = fst (Mod_subst.subst_con subst c) and do_subst_ind (kn,i) = (Mod_subst.subst_ind subst kn,i) @@ -508,12 +501,6 @@ let jmeq () = init_constant ["Logic";"JMeq"] "JMeq") with e -> raise (ToShow e) -let jmeq_rec () = - try - Coqlib.check_required_library ["Coq";"Logic";"JMeq"]; - init_constant ["Logic";"JMeq"] "JMeq_rec" - with e -> raise (ToShow e) - let jmeq_refl () = try Coqlib.check_required_library ["Coq";"Logic";"JMeq"]; diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 5410e724a..a811b29b8 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -853,17 +853,6 @@ let glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift lident , bindlist , Some cstr_expr , lcstor_expr - -let mkProd_reldecl (rdecl:rel_declaration) (t2:glob_constr) = - match rdecl with - | (nme,None,t) -> - let traw = Detyping.detype false [] [] t in - GProd (Loc.ghost,nme,Explicit,traw,t2) - | (_,Some _,_) -> assert false - - - - let mkProd_reldecl (rdecl:rel_declaration) (t2:glob_constr) = match rdecl with | (nme,None,t) -> diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index ec1994cd0..a2f16dc6d 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -18,7 +18,6 @@ open Globnames open Nameops open Errors open Util -open Closure open Tacticals open Tacmach open Tactics @@ -50,10 +49,6 @@ let coq_base_constant s = Coqlib.gen_constant_in_modules "RecursiveDefinition" (Coqlib.init_modules @ [["Coq";"Arith";"Le"];["Coq";"Arith";"Lt"]]) s;; -let coq_constant s = - Coqlib.gen_constant_in_modules "RecursiveDefinition" - (Coqlib.init_modules @ Coqlib.arith_modules) s;; - let find_reference sl s = (locate (make_qualid(Names.make_dirpath (List.map id_of_string (List.rev sl))) @@ -126,7 +121,6 @@ let compute_renamed_type gls c = rename_bound_vars_as_displayed (*no avoid*) [] (*no rels*) [] (pf_type_of gls c) let h'_id = id_of_string "h'" -let heq_id = id_of_string "Heq" let teq_id = id_of_string "teq" let ano_id = id_of_string "anonymous" let x_id = id_of_string "x" @@ -154,18 +148,12 @@ let le_n = function () -> (coq_base_constant "le_n") let coq_sig_ref = function () -> (find_reference ["Coq";"Init";"Specif"] "sig") let coq_O = function () -> (coq_base_constant "O") let coq_S = function () -> (coq_base_constant "S") -let gt_antirefl = function () -> (coq_constant "gt_irrefl") let lt_n_O = function () -> (coq_base_constant "lt_n_O") -let lt_n_Sn = function () -> (coq_base_constant "lt_n_Sn") -let f_equal = function () -> (coq_constant "f_equal") -let well_founded_induction = function () -> (coq_constant "well_founded_induction") let max_ref = function () -> (find_reference ["Recdef"] "max") let max_constr = function () -> (constr_of_global (delayed_force max_ref)) let coq_conj = function () -> find_reference ["Coq";"Init";"Logic"] "conj" let f_S t = mkApp(delayed_force coq_S, [|t|]);; -let make_refl_eq constructor type_of_t t = - mkApp(constructor,[|type_of_t;t|]) let rec n_x_id ids n = if n = 0 then [] @@ -960,10 +948,6 @@ let equation_others _ expr_info continuation_tac infos = (intros_values_eq expr_info []) else continuation_tac infos -let equation_letin (na,b,t,e) expr_info continuation_tac info = - let new_e = subst1 info.info e in - continuation_tac {info with info = new_e;} - let equation_app f_and_args expr_info continuation_tac infos = if expr_info.is_final && expr_info.is_main_branch then intros_values_eq expr_info [] diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml index e40a8a273..99eadd65d 100644 --- a/plugins/micromega/certificate.ml +++ b/plugins/micromega/certificate.ml @@ -405,9 +405,7 @@ let pplus x y = Mc.PEadd(x,y) let pmult x y = Mc.PEmul(x,y) let pconst x = Mc.PEc x let popp x = Mc.PEopp x - -let debug = false - + (* keep track of enumerated vectors *) let rec mem p x l = match l with [] -> false | e::l -> if p x e then true else mem p x l diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4 index 6722008de..eb713f251 100644 --- a/plugins/micromega/g_micromega.ml4 +++ b/plugins/micromega/g_micromega.ml4 @@ -16,9 +16,6 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open Quote -open Mutils -open Glob_term open Errors open Misctypes diff --git a/plugins/nsatz/nsatz.ml4 b/plugins/nsatz/nsatz.ml4 index 4cac90713..34be7244d 100644 --- a/plugins/nsatz/nsatz.ml4 +++ b/plugins/nsatz/nsatz.ml4 @@ -8,34 +8,13 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open Pp open Errors open Util -open Names open Term -open Closure -open Environ -open Libnames open Tactics -open Glob_term -open Tacticals -open Tacexpr -open Pcoq -open Tactic -open Constr -open Proof_type open Coqlib -open Tacmach -open Mod_subst -open Tacinterp -open Libobject -open Printer -open Declare -open Decl_kinds -open Entries open Num -open Unix open Utile (*********************************************************************** diff --git a/plugins/nsatz/polynom.ml b/plugins/nsatz/polynom.ml index 071df5cf7..a610c8461 100644 --- a/plugins/nsatz/polynom.ml +++ b/plugins/nsatz/polynom.ml @@ -7,9 +7,8 @@ (************************************************************************) (* Recursive polynomials: R[x1]...[xn]. *) -open Utile -open Errors open Util +open Utile (* 1. Coefficients: R *) diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index ccf397eda..9bfebe348 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -15,21 +15,12 @@ open Errors open Util -open Pp -open Reduction -open Proof_type open Names open Nameops open Term -open Declarations -open Environ -open Sign -open Inductive open Tacticals open Tacmach -open Evar_refiner open Tactics -open Clenv open Logic open Libnames open Globnames @@ -193,8 +184,6 @@ let coq_Zopp = lazy (zbase_constant "Z.opp") let coq_Zminus = lazy (zbase_constant "Z.sub") let coq_Zsucc = lazy (zbase_constant "Z.succ") let coq_Zpred = lazy (zbase_constant "Z.pred") -let coq_Zgt = lazy (zbase_constant "Z.gt") -let coq_Zle = lazy (zbase_constant "Z.le") let coq_Z_of_nat = lazy (zbase_constant "Z.of_nat") let coq_inj_plus = lazy (z_constant "Nat2Z.inj_add") let coq_inj_mult = lazy (z_constant "Nat2Z.inj_mul") @@ -326,7 +315,6 @@ let coq_iff = lazy (constant "iff") (* uses build_coq_and, build_coq_not, build_coq_or, build_coq_ex *) (* For unfold *) -open Closure let evaluable_ref_of_constr s c = match kind_of_term (Lazy.force c) with | Const kn when Tacred.is_evaluable (Global.env()) (EvalConstRef kn) -> EvalConstRef kn diff --git a/plugins/omega/omega.ml b/plugins/omega/omega.ml index 6abcc7b6f..800254671 100644 --- a/plugins/omega/omega.ml +++ b/plugins/omega/omega.ml @@ -17,8 +17,6 @@ (* the number of source of numbering. *) (**************************************************************************) -open Names - module type INT = sig type bigint val less_than : bigint -> bigint -> bool diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4 index 42cc6bb1d..abb13efd5 100644 --- a/plugins/quote/g_quote.ml4 +++ b/plugins/quote/g_quote.ml4 @@ -8,7 +8,6 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open Pp open Tacexpr open Quote diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index 311ab3081..61a464c1c 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -101,7 +101,6 @@ (*i*) -open Pp open Errors open Util open Names @@ -110,8 +109,6 @@ open Pattern open Patternops open Matching open Tacmach -open Tactics -open Tacexpr (*i*) (*s First, we need to access some Coq constants diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml index c1cea8aac..5b57a0d17 100644 --- a/plugins/romega/const_omega.ml +++ b/plugins/romega/const_omega.ml @@ -71,7 +71,6 @@ let z_constant = Coqlib.gen_constant_in_modules "Omega" z_module let bin_constant = Coqlib.gen_constant_in_modules "Omega" bin_module (* Logic *) -let coq_eq = lazy(init_constant "eq") let coq_refl_equal = lazy(init_constant "eq_refl") let coq_and = lazy(init_constant "and") let coq_not = lazy(init_constant "not") diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml index c6256b0c5..e573f2006 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -7,7 +7,6 @@ *************************************************************************) open Pp -open Errors open Util open Const_omega module OmegaSolver = Omega.MakeOmegaSolver (Bigint) diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml index d1ba173d3..20ec17269 100644 --- a/plugins/rtauto/proof_search.ml +++ b/plugins/rtauto/proof_search.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Term open Errors open Util open Goptions @@ -63,15 +62,6 @@ type form= | Conjunct of form * form | Disjunct of form * form -type tag=int - -let decomp_form=function - Atom i -> Some (i,[]) - | Arrow (f1,f2) -> Some (-1,[f1;f2]) - | Bot -> Some (-2,[]) - | Conjunct (f1,f2) -> Some (-3,[f1;f2]) - | Disjunct (f1,f2) -> Some (-4,[f1;f2]) - module Fmap=Map.Make(struct type t=form let compare=compare end) type sequent = diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index c10aece99..ceaf2a79b 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -11,8 +11,6 @@ module Search = Explore.Make(Proof_search) open Errors open Util open Term -open Names -open Evd open Tacmach open Proof_search @@ -29,13 +27,6 @@ let li_False = lazy (destInd (logic_constant "False")) let li_and = lazy (destInd (logic_constant "and")) let li_or = lazy (destInd (logic_constant "or")) -let data_constant = - Coqlib.gen_constant "refl_tauto" ["Init";"Datatypes"] - -let l_true_equals_true = - lazy (mkApp(logic_constant "eq_refl", - [|data_constant "bool";data_constant "true"|])) - let pos_constant = Coqlib.gen_constant "refl_tauto" ["Numbers";"BinNums"] diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index abf142e79..f30ab7e8b 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -17,14 +17,9 @@ open Closure open Environ open Libnames open Globnames -open Tactics open Glob_term open Tacticals open Tacexpr -open Pcoq -open Tactic -open Constr -open Proof_type open Coqlib open Tacmach open Mod_subst @@ -75,17 +70,6 @@ and mk_clos_app_but f_map subs f args n = (mkApp (mark_arg (-1) f', Array.mapi mark_arg args')) | None -> mk_clos_app_but f_map subs f args (n+1) - -let interp_map l c = - try - let (im,am) = List.assoc c l in - Some(fun i -> - if List.mem i im then Eval - else if List.mem i am then Prot - else if i = -1 then Eval - else Rec) - with Not_found -> None - let interp_map l t = try Some(List.assoc_f eq_constr t l) with Not_found -> None diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml index 88cc07c0e..03fbc7e98 100644 --- a/plugins/syntax/ascii_syntax.ml +++ b/plugins/syntax/ascii_syntax.ml @@ -10,13 +10,9 @@ open Pp open Errors open Util open Names -open Pcoq open Glob_term -open Topconstr -open Libnames open Globnames open Coqlib -open Bigint exception Non_closed_ascii diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml index 5219124cd..8f34ec495 100644 --- a/plugins/syntax/nat_syntax.ml +++ b/plugins/syntax/nat_syntax.ml @@ -9,13 +9,11 @@ (* This file defines the printer for natural numbers in [nat] *) (*i*) -open Util open Glob_term open Bigint open Coqlib open Pp open Errors -open Util (*i*) (**********************************************************************) diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml index cdcdc6e62..94d4e0713 100644 --- a/plugins/syntax/numbers_syntax.ml +++ b/plugins/syntax/numbers_syntax.ml @@ -9,7 +9,6 @@ (* digit-based syntax for int31, bigN bigZ and bigQ *) open Bigint -open Libnames open Globnames open Glob_term diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml index d36851ed9..a40c966fe 100644 --- a/plugins/syntax/r_syntax.ml +++ b/plugins/syntax/r_syntax.ml @@ -6,13 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp -open Errors open Util open Names -open Pcoq -open Topconstr -open Libnames open Globnames exception Non_closed_number @@ -21,7 +16,6 @@ exception Non_closed_number (* Parsing R via scopes *) (**********************************************************************) -open Libnames open Glob_term open Bigint diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml index 7474a8b0e..c9767a975 100644 --- a/plugins/syntax/string_syntax.ml +++ b/plugins/syntax/string_syntax.ml @@ -6,14 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -open Pp -open Errors -open Util -open Names -open Pcoq -open Libnames open Globnames -open Topconstr open Ascii_syntax open Glob_term open Coqlib diff --git a/plugins/xml/doubleTypeInference.ml b/plugins/xml/doubleTypeInference.ml index b1838f4a4..8f1d97d3b 100644 --- a/plugins/xml/doubleTypeInference.ml +++ b/plugins/xml/doubleTypeInference.ml @@ -15,8 +15,6 @@ (*CSC: tutto da rifare!!! Basarsi su Retyping che e' meno costoso! *) type types = {synthesized : Term.types ; expected : Term.types option};; -let prerr_endline _ = ();; - let cprop = let module N = Names in N.make_con diff --git a/plugins/xml/dumptree.ml4 b/plugins/xml/dumptree.ml4 index 4fc1fc2b7..623d7c804 100644 --- a/plugins/xml/dumptree.ml4 +++ b/plugins/xml/dumptree.ml4 @@ -13,13 +13,10 @@ (*i camlp4deps: "grammar/grammar.cma" i*) open Tacexpr;; -open Decl_mode;; open Printer;; open Pp;; open Environ;; -open Format;; open Proof_type;; -open Evd;; open Termops;; open Ppconstr;; open Names;; diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml index ee9bcb25d..2550e248a 100644 --- a/plugins/xml/xmlcommand.ml +++ b/plugins/xml/xmlcommand.ml @@ -35,50 +35,8 @@ let print_proof_tree, set_print_proof_tree = let print_if_verbose s = if !verbose then print_string s;; -(* Next exception is used only inside print_coq_object and tag_of_string_tag *) -exception Uninteresting;; - -(* NOT USED anymore, we back to the V6 point of view with global parameters - -(* Internally, for Coq V7, params of inductive types are associated *) -(* not to the whole block of mutual inductive (as it was in V6) but to *) -(* each member of the block; but externally, all params are required *) -(* to be the same; the following function checks that the parameters *) -(* of each inductive of a same block are all the same, then returns *) -(* this number; it fails otherwise *) -let extract_nparams pack = - let module D = Declarations in - let module U = Util in - let module S = Sign in - - let {D.mind_nparams=nparams0} = pack.(0) in - let arity0 = pack.(0).D.mind_user_arity in - let params0, _ = S.decompose_prod_n_assum nparams0 arity0 in - for i = 1 to Array.length pack - 1 do - let {D.mind_nparams=nparamsi} = pack.(i) in - let arityi = pack.(i).D.mind_user_arity in - let paramsi, _ = S.decompose_prod_n_assum nparamsi arityi in - if params0 <> paramsi then U.error "Cannot convert a block of inductive definitions with parameters specific to each inductive to a block of mutual inductive definitions with parameters global to the whole block" - done; - nparams0 - -*) - open Decl_kinds -(* could_have_namesakes sp = true iff o is an object that could be cooked and *) -(* than that could exists in cooked form with the same name in a super *) -(* section of the actual section *) -let could_have_namesakes o sp = (* namesake = omonimo in italian *) - let tag = Libobject.object_tag o in - print_if_verbose ("Object tag: " ^ tag ^ "\n") ; - match tag with - "CONSTANT" -> true (* constants/parameters are non global *) - | "INDUCTIVE" -> true (* mutual inductive types are never local *) - | "VARIABLE" -> false (* variables are local, so no namesakes *) - | _ -> false (* uninteresting thing that won't be printed*) -;; - (* filter_params pvars hyps *) (* filters out from pvars (which is a list of lists) all the variables *) (* that does not belong to hyps (which is a simple list) *) @@ -295,54 +253,6 @@ let mk_variable_obj id body typ = (Names.string_of_id id, unsharedbody, Unshare.unshare typ, params) ;; -(* Unsharing is not performed on the body, that must be already unshared. *) -(* The evar map and the type, instead, are unshared by this function. *) -let mk_current_proof_obj is_a_variable id bo ty evar_map env = - let unshared_ty = Unshare.unshare ty in - let metasenv = - List.map - (function - (n, {Evd.evar_concl = evar_concl ; - Evd.evar_hyps = evar_hyps} - ) -> - (* We map the named context to a rel context and every Var to a Rel *) - let final_var_ids,context = - let rec aux var_ids = - function - [] -> var_ids,[] - | (n,None,t)::tl -> - let final_var_ids,tl' = aux (n::var_ids) tl in - let t' = Term.subst_vars var_ids t in - final_var_ids,(n, Acic.Decl (Unshare.unshare t'))::tl' - | (n,Some b,t)::tl -> - let final_var_ids,tl' = aux (n::var_ids) tl in - let b' = Term.subst_vars var_ids b in - (* t will not be exported to XML. Thus no unsharing performed *) - final_var_ids,(n, Acic.Def (Unshare.unshare b',t))::tl' - in - aux [] (List.rev (Environ.named_context_of_val evar_hyps)) - in - (* We map the named context to a rel context and every Var to a Rel *) - (n,context,Unshare.unshare (Term.subst_vars final_var_ids evar_concl)) - ) (Evarutil.non_instantiated evar_map) - in - let id' = Names.string_of_id id in - if metasenv = [] then - let ids = - Names.Idset.union - (Environ.global_vars_set env bo) (Environ.global_vars_set env ty) in - let hyps0 = Environ.keep_hyps env ids in - let hyps = string_list_of_named_context_list hyps0 in - (* Variables are the identifiers of the variables in scope *) - let variables = search_variables () in - let params = filter_params variables hyps in - if is_a_variable then - Acic.Variable (id',Some bo,unshared_ty,params) - else - Acic.Constant (id',Some bo,unshared_ty,params) - else - Acic.CurrentProof (id',metasenv,bo,unshared_ty) -;; let mk_constant_obj id bo ty variables hyps = let hyps = string_list_of_named_context_list hyps in @@ -395,11 +305,6 @@ let theory_output_string ?(do_not_quote = false) s = Buffer.add_string theory_buffer s ;; -let kind_of_global_goal = function - | Global, DefinitionBody _ -> "DEFINITION","InteractiveDefinition" - | Global, (Proof k) -> "THEOREM",Kindops.string_of_theorem_kind k - | Local, _ -> assert false - let kind_of_inductive isrecord kn = "DEFINITION", if (fst (Global.lookup_inductive (kn,0))).Declarations.mind_finite diff --git a/plugins/xml/xmlentries.ml4 b/plugins/xml/xmlentries.ml4 index 597190d3e..5ca6e155b 100644 --- a/plugins/xml/xmlentries.ml4 +++ b/plugins/xml/xmlentries.ml4 @@ -14,13 +14,7 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open Util;; -open Vernacinterp;; - -open Extend;; -open Genarg;; -open Pp;; -open Pcoq;; +open Pp (* File name *) diff --git a/pretyping/cases.ml b/pretyping/cases.ml index b6b8f8dba..7b6be410b 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -62,15 +62,6 @@ let error_wrong_predicate_arity_loc loc env c n1 n2 = let error_needs_inversion env x t = raise (PatternMatchingError (env, NeedsInversion (x,t))) -module type S = sig - val compile_cases : - Loc.t -> case_style -> - (type_constraint -> env -> evar_map ref -> glob_constr -> unsafe_judgment) * evar_map ref -> - type_constraint -> - env -> glob_constr option * tomatch_tuples * cases_clauses -> - unsafe_judgment -end - let rec list_try_compile f = function | [a] -> f a | [] -> anomaly "try_find_f" @@ -396,10 +387,6 @@ let type_of_tomatch = function | IsInd (t,_,_) -> t | NotInd (_,t) -> t -let mkDeclTomatch na = function - | IsInd (t,_,_) -> (na,None,t) - | NotInd (c,t) -> (na,c,t) - let map_tomatch_type f = function | IsInd (t,ind,names) -> IsInd (f t,map_inductive_type f ind,names) | NotInd (c,t) -> NotInd (Option.map f c, f t) @@ -1800,8 +1787,6 @@ let string_of_name name = | Anonymous -> "anonymous" | Name n -> string_of_id n -let id_of_name n = id_of_string (string_of_name n) - let make_prime_id name = let str = string_of_name name in id_of_string str, id_of_string (str ^ "'") @@ -1981,22 +1966,6 @@ let build_ineqs prevpatterns pats liftsign = in match diffs with [] -> None | _ -> Some (mk_coq_and diffs) -let subst_rel_context k ctx subst = - let (_, ctx') = - List.fold_right - (fun (n, b, t) (k, acc) -> - (succ k, (n, Option.map (substnl subst k) b, substnl subst k t) :: acc)) - ctx (k, []) - in ctx' - -let lift_rel_contextn n k sign = - let rec liftrec k = function - | (na,c,t)::sign -> - (na,Option.map (liftn n k) c,liftn n k t)::(liftrec (k-1) sign) - | [] -> [] - in - liftrec (rel_context_length sign + k) sign - let constrs_of_pats typing_fun env isevars eqns tomatchs sign neqs arity = let i = ref 0 in let (x, y, z) = @@ -2111,10 +2080,6 @@ let abstract_tomatch env tomatchs tycon = ([], [], [], tycon) tomatchs in List.rev prev, ctx, tycon -let is_dependent_ind = function - IsInd (_, IndType (indf, args), _) when List.length args > 0 -> true - | _ -> false - let build_dependent_signature env evars avoid tomatchs arsign = let avoid = ref avoid in let arsign = List.rev arsign in diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 14476354b..52ec8d1d1 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -406,10 +406,7 @@ let discharge_coercion (_,(coe,stre,isid,cls,clt,ps)) = let classify_coercion (coe,stre,isid,cls,clt,ps as obj) = if stre = Local then Dispose else Substitute obj -type coercion_obj = - coe_typ * Decl_kinds.locality * bool * cl_typ * cl_typ * int - -let inCoercion : coercion_obj -> obj = +let inCoercion : coercion -> obj = declare_object {(default_object "COERCION") with open_function = open_coercion; load_function = load_coercion; diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index f931d723f..30f6de5c2 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -582,10 +582,6 @@ let filter_possible_projections c ty ctxt args = Idset.mem id tyvars) ctxt args -let initial_evar_data evi = - let ids = List.map pi1 (evar_context evi) in - (evar_filter evi, List.map mkVar ids) - let solve_evars = ref (fun _ -> failwith "solve_evars not installed") let set_solve_evars f = solve_evars := f diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index e51415abb..45df12e46 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -1126,16 +1126,6 @@ let invert_arg evd aliases k evk subst_in_env_extended_with_k_binders c_in_env_e | _ -> res -let effective_projections = - List.map_filter (function Invertible c -> Some c | _ -> None) - -let instance_of_projection f env t evd projs = - let ty = lazy (nf_evar evd (Retyping.get_type_of env evd t)) in - match projs with - | NoUniqueProjection -> raise NotUnique - | UniqueProjection (c,effects) -> - (List.fold_left (do_projection_effects f env ty) evd effects, c) - exception NotEnoughInformationToInvert let extract_unique_projections projs = @@ -1157,8 +1147,6 @@ let extract_candidates sols = with Exit -> None -let filter_of_projection = function Invertible _ -> true | _ -> false - let invert_invertible_arg evd aliases k (evk,argsv) args' = let evi = Evd.find_undefined evd evk in let subst,_ = make_projectable_subst aliases evd evi argsv in @@ -1899,7 +1887,6 @@ let check_evars env initial_sigma sigma c = | _ -> iter_constr proc_rec c in proc_rec c - (****************************************) (* Operations on value/type constraints *) (****************************************) diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 1394f3ba8..cc6bd6150 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -672,10 +672,6 @@ let retract_coercible_metas evd = evd.metas ([],Metamap.empty) in mc, { evd with metas = ml } -let rec list_assoc_in_triple x = function - [] -> raise Not_found - | (a,b,_)::l -> if compare a x = 0 then b else list_assoc_in_triple x l - let subst_defined_metas bl c = let rec substrec c = match kind_of_term c with | Meta i -> substrec (List.assoc_snd_in_triple i bl) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index ed65cc9ea..8c216d99b 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -158,13 +158,6 @@ let evd_comb2 f evdref x y = evdref := evd'; z -let evd_comb3 f evdref x y z = - let (evd',t) = f !evdref x y z in - evdref := evd'; - t - -let mt_evd = Evd.empty - (* Utilisé pour inférer le prédicat des Cases *) (* Semble exagérement fort *) (* Faudra préférer une unification entre les types de toutes les clauses *) @@ -256,8 +249,6 @@ let pretype_sort evdref = function | GSet -> judge_of_set | GType _ -> evd_comb0 judge_of_new_Type evdref -exception Found of fixpoint - let new_type_evar evdref env loc = evd_comb0 (fun evd -> Evarutil.new_type_evar evd env ~src:(loc,Evar_kinds.InternalHole)) evdref diff --git a/pretyping/program.ml b/pretyping/program.ml index db821f176..a8e91856b 100644 --- a/pretyping/program.ml +++ b/pretyping/program.ml @@ -11,8 +11,6 @@ open Util open Names open Term -type message = string - let make_dir l = make_dirpath (List.map id_of_string (List.rev l)) let find_reference locstr dir s = @@ -63,10 +61,3 @@ let mk_coq_and l = (fun c conj -> mkApp (and_typ, [| c ; conj |])) l - -let with_program f c = - let mode = !Flags.program_mode in - Flags.program_mode := true; - let res = f c in - Flags.program_mode := mode; - res diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index f20c0dd83..b417dc1d4 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -907,8 +907,6 @@ let whd_programs_stack env sigma = let whd_programs env sigma x = zip (whd_programs_stack env sigma (x, empty_stack)) -exception IsType - let find_conclusion env sigma = let rec decrec env c = let t = whd_betadeltaiota env sigma c in diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 3563e9ca2..97ce40a77 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -124,9 +124,9 @@ type constant_evaluation = (* We use a cache registered as a global table *) -let eval_table = ref Cmap.empty +type frozen = constant_evaluation Cmap.t -type frozen = (int * constant_evaluation) Cmap.t +let eval_table = ref (Cmap.empty : frozen) let init () = eval_table := Cmap.empty diff --git a/pretyping/term_dnet.ml b/pretyping/term_dnet.ml index 451dde11f..8372d31da 100644 --- a/pretyping/term_dnet.ml +++ b/pretyping/term_dnet.ml @@ -48,8 +48,6 @@ struct | DCons of ('t * 't option) * 't | DNil - type dconstr = dconstr t - (* debug *) let pr_dconstr f : 'a t -> std_ppcmds = function | DRel -> str "*" @@ -203,11 +201,6 @@ struct type ident = TDnet.ident - type 'a pattern = 'a TDnet.pattern - type term_pattern = term_pattern DTerm.t pattern - - type idset = TDnet.Idset.t - type result = ident * (constr*existential_key) * Termops.subst open DTerm @@ -268,10 +261,6 @@ struct let c = empty_ctx (pat_of_constr c) in TDnet.add dn c id - let new_meta_no = - let ctr = ref 0 in - fun () -> decr ctr; !ctr - let new_meta_no = Evarutil.new_untyped_evar let neutral_meta = new_meta_no() diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 426197af2..2749538c0 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -44,7 +44,6 @@ let solve_instanciation_problem = ref (fun _ _ _ -> assert false) let resolve_one_typeclass env evm t = !solve_instanciation_problem env evm t -type rels = constr list type direction = Forward | Backward (* This module defines type-classes *) @@ -327,11 +326,6 @@ let classify_instance (action, inst) = if is_local inst then Dispose else Substitute (action, inst) -let load_instance (_, (action, inst) as ai) = - cache_instance ai; - if action = AddInstance then - add_instance_hint (constr_of_global inst.is_impl) (is_local inst) inst.is_pri - let instance_input : instance_action * instance -> obj = declare_object { (default_object "type classes instances state") with diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml index 053c1cd7b..4a0b66a7b 100644 --- a/pretyping/typeclasses_errors.ml +++ b/pretyping/typeclasses_errors.ml @@ -12,7 +12,6 @@ open Term open Evd open Environ open Constrexpr -open Util open Globnames (*i*) diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 8955cc64c..886c4a3aa 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -313,9 +313,6 @@ let elim_no_delta_flags = { allow_K_in_toplevel_higher_order_unification = true } -let set_no_head_reduction flags = - { flags with restrict_conv_on_strict_subterms = true } - let use_evars_pattern_unification flags = !global_evars_pattern_unification_flag && flags.use_pattern_unification && Flags.version_strictly_greater Flags.V8_2 diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 190181c23..1d03716d0 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -17,7 +17,6 @@ open Ppextend open Constrexpr open Constrexpr_ops open Topconstr -open Term open Decl_kinds open Misctypes open Locus @@ -34,7 +33,6 @@ let lif = 200 let lletin = 200 let lletpattern = 200 let lfix = 200 -let larrow = 90 let lcast = 100 let larg = 9 let lapp = 10 @@ -612,7 +610,6 @@ let pr_red_flag pr r = pr_arg str "delta " ++ (if r.rDelta then str "-" else mt ()) ++ hov 0 (str "[" ++ prlist_with_sep spc pr r.rConst ++ str "]")) - let pr_metaid id = str"?" ++ pr_id id let pr_red_expr (pr_constr,pr_lconstr,pr_ref,pr_pattern) = function diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 8bdea1356..d16035fba 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -220,7 +220,6 @@ let rec pr_glob_generic prc prlc prtac prpat x = try pi2 (Stringmap.find s !genarg_pprule) prc prlc prtac x with Not_found -> str "[no printer for " ++ str s ++ str "]" - 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") @@ -549,7 +548,6 @@ let linfo = 5 let level_of (n,p) = match p with E -> n | L -> n-1 | Prec n -> n | Any -> lseq - (** A printer for tactics that polymorphically works on the three "raw", "glob" and "typed" levels; in practice, the environment is used only at the glob and typed level: it is used to feed the diff --git a/printing/printer.ml b/printing/printer.ml index 374b5d597..74c5a02d5 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -22,7 +22,6 @@ open Pfedit open Constrextern open Ppconstr - let emacs_str s = if !Flags.print_emacs then s else "" let delayed_emacs_cmd s = diff --git a/printing/tactic_printer.ml b/printing/tactic_printer.ml index e347b6c89..87bb89e8d 100644 --- a/printing/tactic_printer.ml +++ b/printing/tactic_printer.ml @@ -51,8 +51,6 @@ let pr_rule_dot_fnl = function | Prim Change_evars -> mt () | r -> pr_rule_dot r ++ fnl () -exception Different - let rec print_proof sigma osign pf = (* spiwack: [osign] is currently ignored, not sure if this function is even used. *) let hyps = Environ.named_context_of_val (Goal.V82.hyps sigma pf.goal) in diff --git a/printing/tactic_printer.mli b/printing/tactic_printer.mli index 1c045e624..e94a2a771 100644 --- a/printing/tactic_printer.mli +++ b/printing/tactic_printer.mli @@ -6,18 +6,16 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp open Sign open Evd -open Tacexpr open Proof_type (** These are the entry points for tactics, proof trees, ... *) -val print_proof : evar_map -> named_context -> proof_tree -> std_ppcmds -val pr_rule : rule -> std_ppcmds -val pr_tactic : tactic_expr -> std_ppcmds +val print_proof : evar_map -> named_context -> proof_tree -> Pp.std_ppcmds +val pr_rule : rule -> Pp.std_ppcmds +val pr_tactic : tactic_expr -> Pp.std_ppcmds val print_script : - ?nochange:bool -> evar_map -> proof_tree -> std_ppcmds + ?nochange:bool -> evar_map -> proof_tree -> Pp.std_ppcmds val print_treescript : - ?nochange:bool -> evar_map -> proof_tree -> std_ppcmds + ?nochange:bool -> evar_map -> proof_tree -> Pp.std_ppcmds diff --git a/proofs/logic.ml b/proofs/logic.ml index 5be9df317..5437d2ba1 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -683,21 +683,3 @@ let prim_refiner r sigma goal = (* Normalises evars in goals. Used by instantiate. *) let (goal,sigma) = Goal.V82.nf_evar sigma goal in ([goal],sigma) - -(************************************************************************) -(************************************************************************) -(* Extracting a proof term from the proof tree *) - -(* Util *) - -type variable_proof_status = ProofVar | SectionVar of identifier - -type proof_variable = name * variable_proof_status - -let proof_variable_index x = - let rec aux n = function - | (Name id,ProofVar)::l when x = id -> n - | _::l -> aux (n+1) l - | [] -> raise Not_found - in - aux 1 diff --git a/proofs/logic.mli b/proofs/logic.mli index 696115a8a..75d9bd957 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -32,10 +32,6 @@ val with_check : tactic -> tactic val prim_refiner : prim_rule -> evar_map -> goal -> goal list * evar_map -type proof_variable - - -val proof_variable_index : identifier -> proof_variable list -> int (** {6 Refiner errors. } *) diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 3dbb2190b..cad700b84 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -30,7 +30,7 @@ let undo n = let p = Proof_global.give_me_the_proof () in let d = Proof.V82.depth p in if n >= d then raise Proof.EmptyUndoStack; - for i = 1 to n do + for _i = 1 to n do Proof.undo p done @@ -47,10 +47,6 @@ let undo_todepth n = undo ((current_proof_depth ()) - n ) with Proof_global.NoCurrentProof when n=0 -> () -let set_undo _ = () -let get_undo _ = None - - let start_proof id str hyps c ?init_tac ?compute_guard hook = let goals = [ (Global.env_of_context hyps , c) ] in let init_tac = Option.map Proofview.V82.tactic init_tac in diff --git a/proofs/proof.ml b/proofs/proof.ml index a421ccd0b..71afae020 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -29,8 +29,6 @@ Therefore the undo stack stores action to be ran to undo. *) -open Term - type _focus_kind = int type 'a focus_kind = _focus_kind type focus_info = Obj.t diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index bedf058fc..178c2ab2d 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -314,8 +314,6 @@ let maximal_unfocus k p = module Bullet = struct - - type t = Vernacexpr.bullet type behavior = { diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index 4a404b6f3..1f5ef315b 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -11,7 +11,6 @@ open Evd open Names open Term open Tacexpr -(* open Decl_expr *) open Glob_term open Genarg open Nametab diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 79b5ae731..98e1acc42 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -372,7 +372,7 @@ let list_of_sensitive s k env = with e when catchable_exception e -> tclZERO e env -let tclGOALBIND s k = +let tclGOALBIND s k = (* spiwack: the first line ensures that the value returned by the tactic [k] will not "escape its scope". *) let k a = tclBIND (k a) here_s in @@ -380,7 +380,7 @@ let tclGOALBIND s k = tclDISPATCHGEN Goal.null Goal.plus tacs end -let tclGOALBINDU s k = +let tclGOALBINDU s k = tclBIND (list_of_sensitive s k) begin fun tacs -> tclDISPATCHGEN () unitK tacs end diff --git a/proofs/refiner.ml b/proofs/refiner.ml index ac8de601e..4f75ffa52 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -117,9 +117,6 @@ let thens3parts_tac tacfi tac tacli (sigr,gs) = (* Apply [taci.(i)] on the first n subgoals and [tac] on the others *) let thensf_tac taci tac = thens3parts_tac taci tac [||] -(* Apply [taci.(i)] on the last n subgoals and [tac] on the others *) -let thensl_tac tac taci = thens3parts_tac [||] tac taci - (* Apply [tac i] on the ith subgoal (no subgoals number check) *) let thensi_tac tac (sigr,gs) = let gll = @@ -128,22 +125,6 @@ let thensi_tac tac (sigr,gs) = let then_tac tac = thensf_tac [||] tac -let non_existent_goal n = - errorlabstrm ("No such goal: "^(string_of_int n)) - (str"Trying to apply a tactic to a non existent goal") - -(* Apply tac on the i-th goal (if i>0). If i<0, then start counting from - the last goal (i=-1). *) -let theni_tac i tac ((_,gl) as subgoals) = - let nsg = List.length gl in - let k = if i < 0 then nsg + i + 1 else i in - if nsg < 1 then errorlabstrm "theni_tac" (str"No more subgoals.") - else if k >= 1 & k <= nsg then - thensf_tac - (Array.init k (fun i -> if i+1 = k then tac else tclIDTAC)) tclIDTAC - subgoals - else non_existent_goal k - (* [tclTHENS3PARTS tac1 [|t1 ; ... ; tn|] tac2 [|t'1 ; ... ; t'm|] gls] applies the tactic [tac1] to [gls] then, applies [t1], ..., [tn] to the first [n] resulting subgoals, [t'1], ..., [t'm] to the last [m] diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index cab124d93..4524fe6a1 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -109,8 +109,6 @@ let pf_matches = pf_apply Matching.matches_conv (* Tactics handling a list of goals *) (************************************) -type transformation_tactic = proof_tree -> goal list - type validation_list = proof_tree list -> proof_tree list type tactic_list = Refiner.tactic_list diff --git a/tactics/auto.ml b/tactics/auto.ml index d88a6a6b0..748b608b4 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -22,7 +22,6 @@ open Pattern open Patternops open Matching open Tacmach -open Proof_type open Pfedit open Genredexpr open Tacred @@ -108,18 +107,6 @@ let insert v l = type stored_data = int * pri_auto_tactic (* First component is the index of insertion in the table, to keep most recent first semantics. *) -let auto_tactic_ord code1 code2 = - match code1, code2 with - | Res_pf (c1, _), Res_pf (c2, _) - | ERes_pf (c1, _), ERes_pf (c2, _) - | Give_exact c1, Give_exact c2 - | Res_pf_THEN_trivial_fail (c1, _), Res_pf_THEN_trivial_fail (c2, _) -> constr_ord c1 c2 - | Unfold_nth (EvalVarRef i1), Unfold_nth (EvalVarRef i2) -> Pervasives.compare i1 i2 - | Unfold_nth (EvalConstRef c1), Unfold_nth (EvalConstRef c2) -> - kn_ord (canonical_con c1) (canonical_con c2) - | Extern t1, Extern t2 -> Pervasives.compare t1 t2 - | _ -> Pervasives.compare code1 code2 - module Bounded_net = Btermdn.Make(struct type t = stored_data let compare = pri_order_int @@ -436,8 +423,6 @@ module Hintdbmap = Gmap type hint_db = Hint_db.t -type frozen_hint_db_table = (string,hint_db) Hintdbmap.t - type hint_db_table = (string,hint_db) Hintdbmap.t ref type hint_db_name = string @@ -484,8 +469,6 @@ let try_head_pattern c = try head_pattern_bound c with BoundPattern -> error "Bound head variable." -let name_of_constr c = try Some (global_of_constr c) with Not_found -> None - let make_exact_entry sigma pri ?(name=PathAny) (c,cty) = let cty = strip_outer_cast cty in match kind_of_term cty with @@ -1393,22 +1376,6 @@ let possible_resolve dbg mod_delta db_list local_db cl = let dbg_case dbg id = tclLOG dbg (fun () -> str "case " ++ pr_id id) (simplest_case (mkVar id)) -let decomp_unary_term_then dbg (id,_,typc) kont1 kont2 gl = - try - let ccl = applist (head_constr typc) in - match Hipattern.match_with_conjunction ccl with - | Some (_,args) -> - tclTHEN (dbg_case dbg id) (kont1 (List.length args)) gl - | None -> - kont2 gl - with UserError _ -> kont2 gl - -let decomp_empty_term dbg (id,_,typc) gl = - if Hipattern.is_empty_type typc then - dbg_case dbg id gl - else - errorlabstrm "Auto.decomp_empty_term" (str "Not an empty type.") - let extend_local_db gl decl db = Hint_db.add_list (make_resolve_hyp (pf_env gl) (project gl) decl) db @@ -1422,8 +1389,6 @@ let intro_register dbg kont db = (* n is the max depth of search *) (* local_db contains the local Hypotheses *) -exception Uplift of tactic list - let search d n mod_delta db_list local_db = let rec search d n local_db = if n=0 then (fun gl -> error "BOUND 2") else diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index dfa94102d..dd02475dd 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -242,12 +242,6 @@ type hypinfo = { hyp_right : constr; } -let evd_convertible env evd x y = - try - ignore(Unification.w_unify ~flags:Unification.elim_flags env evd Reduction.CONV x y); true - (* try ignore(Evarconv.the_conv_x env x y evd); true *) - with _ -> false - let decompose_applied_relation metas env sigma c ctype left2right = let find_rel ty = let eqclause = Clenv.mk_clenv_from_env env sigma None (c,ty) in diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index 933bb6619..d411a28c4 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -12,29 +12,16 @@ open Pp open Errors open Util open Names -open Nameops open Term open Termops -open Sign open Reduction open Proof_type -open Declarations open Tacticals open Tacmach -open Evar_refiner open Tactics -open Pattern open Patternops open Clenv -open Auto -open Glob_term -open Hiddentac open Typeclasses -open Typeclasses_errors -open Classes -open Topconstr -open Pfedit -open Command open Globnames open Evd open Locus @@ -750,7 +737,6 @@ VERNAC COMMAND EXTEND Typeclasses_Rigid_Settings END open Genarg -open Extraargs let pr_debug _prc _prlc _prt b = if b then Pp.str "debug" else Pp.mt() diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index 02d99d707..2bbb3ac5a 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -15,15 +15,10 @@ open Names open Nameops open Term open Termops -open Sign -open Reduction open Proof_type -open Declarations open Tacticals open Tacmach -open Evar_refiner open Tactics -open Pattern open Patternops open Clenv open Auto @@ -353,8 +348,6 @@ let e_search_auto debug (in_depth,p) lems db_list gl = pr_info_nop d; error "eauto: search failed" -open Evd - let eauto_with_bases ?(debug=Off) np lems db_list = tclTRY (e_search_auto debug np lems db_list) diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml index fd21d84b0..62d13c0a6 100644 --- a/tactics/elimschemes.ml +++ b/tactics/elimschemes.ml @@ -58,10 +58,6 @@ let rect_dep_scheme_kind_from_type = declare_individual_scheme_object "_rect" ~aux:"_rect_from_type" (build_induction_scheme_in_type true InType) -let rect_dep_scheme_kind_from_prop = - declare_individual_scheme_object "_rect_dep" - (build_induction_scheme_in_type true InType) - let ind_scheme_kind_from_type = declare_individual_scheme_object "_ind_nodep" (optimize_non_type_induction_scheme rect_scheme_kind_from_type false InProp) @@ -74,14 +70,6 @@ let ind_dep_scheme_kind_from_type = declare_individual_scheme_object "_ind" ~aux:"_ind_from_type" (optimize_non_type_induction_scheme rect_dep_scheme_kind_from_type true InProp) -let ind_dep_scheme_kind_from_prop = - declare_individual_scheme_object "_ind_dep" - (optimize_non_type_induction_scheme rect_dep_scheme_kind_from_prop true InProp) - -let rec_scheme_kind_from_type = - declare_individual_scheme_object "_rec_nodep" - (optimize_non_type_induction_scheme rect_scheme_kind_from_type false InSet) - let rec_scheme_kind_from_prop = declare_individual_scheme_object "_rec" ~aux:"_rec_from_prop" (optimize_non_type_induction_scheme rect_scheme_kind_from_prop false InSet) @@ -90,10 +78,6 @@ let rec_dep_scheme_kind_from_type = declare_individual_scheme_object "_rec" ~aux:"_rec_from_type" (optimize_non_type_induction_scheme rect_dep_scheme_kind_from_type true InSet) -let rec_dep_scheme_kind_from_prop = - declare_individual_scheme_object "_rec_dep" - (optimize_non_type_induction_scheme rect_dep_scheme_kind_from_prop true InSet) - (* Case analysis *) let build_case_analysis_scheme_in_type dep sort ind = diff --git a/tactics/eqdecide.ml4 b/tactics/eqdecide.ml4 index f26eb1024..5329029a8 100644 --- a/tactics/eqdecide.ml4 +++ b/tactics/eqdecide.ml4 @@ -23,12 +23,9 @@ open Declarations open Tactics open Tacticals open Hiddentac -open Equality open Auto -open Pattern open Matching open Hipattern -open Proof_type open Tacmach open Coqlib diff --git a/tactics/equality.ml b/tactics/equality.ml index 08b05746b..9827b6146 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -753,8 +753,6 @@ let discrimination_pf e (t,t1,t2) discriminator lbeq = let eq_elim = ind_scheme_of_eq lbeq in (applist (eq_elim, [t;t1;mkNamedLambda e t discriminator;i;t2]), absurd_term) -exception NotDiscriminable - let eq_baseid = id_of_string "e" let apply_on_clause (f,t) clause = diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4 index 33cbf1b2d..e0ba730cd 100644 --- a/tactics/extraargs.ml4 +++ b/tactics/extraargs.ml4 @@ -9,12 +9,10 @@ (*i camlp4deps: "grammar/grammar.cma" i*) open Pp -open Pcoq open Genarg open Names open Tacexpr open Tacinterp -open Termops open Misctypes open Locus @@ -39,8 +37,6 @@ let pr_orient = pr_orient () () () let pr_int_list = Pp.pr_sequence Pp.int let pr_int_list_full _prc _prlc _prt l = pr_int_list l -open Glob_term - let pr_occurrences _prc _prlc _prt l = match l with | ArgArg x -> pr_int_list x diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 7f0e486ab..a3fa9956e 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -9,13 +9,11 @@ (*i camlp4deps: "grammar/grammar.cma" i*) open Pp -open Pcoq open Genarg open Extraargs open Mod_subst open Names open Tacexpr -open Glob_term open Glob_ops open Tactics open Errors @@ -338,7 +336,6 @@ VERNAC COMMAND EXTEND DeriveInversionClear END open Term -open Glob_term VERNAC COMMAND EXTEND DeriveInversion | [ "Derive" "Inversion" ident(na) "with" constr(c) "Sort" sort(s) ] @@ -389,7 +386,6 @@ TACTIC EXTEND evar | [ "evar" constr(typ) ] -> [ let_evar Anonymous typ ] END -open Tacexpr open Tacticals TACTIC EXTEND instantiate @@ -403,8 +399,6 @@ END (** Nijmegen "step" tactic for setoid rewriting *) open Tactics -open Tactics -open Libnames open Glob_term open Summary open Libobject @@ -623,9 +617,6 @@ END hget_evar *) -open Evar_refiner -open Sign - let hget_evar n gl = let sigma = project gl in let evl = evar_list sigma (pf_concl gl) in diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml index 77379cb74..b68b6c545 100644 --- a/tactics/hiddentac.ml +++ b/tactics/hiddentac.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) - open Refiner open Tacexpr open Tactics diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4 index 237c63a83..ec8bc5f7e 100644 --- a/tactics/hipattern.ml4 +++ b/tactics/hipattern.ml4 @@ -12,16 +12,9 @@ open Pp open Errors open Util open Names -open Nameops open Term -open Sign open Termops -open Reductionops open Inductiveops -open Evd -open Environ -open Clenv -open Pattern open Matching open Coqlib open Declarations @@ -359,7 +352,6 @@ let coq_eq_pattern_gen eq = lazy PATTERN [ %eq ?X1 ?X2 ?X3 ] let coq_eq_pattern = coq_eq_pattern_gen coq_eq_ref let coq_identity_pattern = coq_eq_pattern_gen coq_identity_ref let coq_jmeq_pattern = lazy PATTERN [ %coq_jmeq_ref ?X1 ?X2 ?X3 ?X4 ] -let coq_eq_true_pattern = lazy PATTERN [ %coq_eq_true_ref ?X1 ] let match_eq eqn eq_pat = let pat = try Lazy.force eq_pat with _ -> raise PatternMatchingFailure in @@ -392,12 +384,6 @@ let find_eq_data_decompose gl eqn = let (lbeq,eq_args) = find_eq_data eqn in (lbeq,extract_eq_args gl eq_args) -let inversible_equalities = - [coq_eq_pattern, build_coq_inversion_eq_data; - coq_jmeq_pattern, build_coq_inversion_jmeq_data; - coq_identity_pattern, build_coq_inversion_identity_data; - coq_eq_true_pattern, build_coq_inversion_eq_true_data] - let find_this_eq_data_decompose gl eqn = let (lbeq,eq_args) = try (*first_match (match_eq eqn) inversible_equalities*) @@ -411,7 +397,6 @@ let find_this_eq_data_decompose gl eqn = (lbeq,eq_args) open Tacmach -open Tacticals let match_eq_nf gls eqn eq_pat = match pf_matches gls (Lazy.force eq_pat) eqn with diff --git a/tactics/inv.ml b/tactics/inv.ml index 189c73a16..d598a97e6 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -198,7 +198,6 @@ let split_dep_and_nodep hyps gl = if var_occurs_in_pf gl id then (d::l1,l2) else (l1,d::l2)) hyps ([],[]) - (* Computation of dids is late; must have been done in rewrite_equations*) (* Will keep generalizing and introducing back and forth... *) (* Moreover, others hyps depending of dids should have been *) diff --git a/tactics/nbtermdn.ml b/tactics/nbtermdn.ml index 6459336b8..bafc85b12 100644 --- a/tactics/nbtermdn.ml +++ b/tactics/nbtermdn.ml @@ -104,19 +104,6 @@ let decomp = | Const _ -> Dn.Everything | _ -> Dn.Nothing -let constr_val_discr_st (idpred,cpred) t = - let c, l = decomp t in - match kind_of_term c with - | Const c -> if Cpred.mem c cpred then Dn.Everything else Dn.Label(Term_dn.GRLabel (ConstRef c),l) - | Ind ind_sp -> Dn.Label(Term_dn.GRLabel (IndRef ind_sp),l) - | Construct cstr_sp -> Dn.Label(Term_dn.GRLabel (ConstructRef cstr_sp),l) - | Var id when not (Idpred.mem id idpred) -> Dn.Label(Term_dn.GRLabel (VarRef id),l) - | Prod (n, d, c) -> Dn.Label(Term_dn.ProdLabel, [d; c]) - | Lambda (n, d, c) -> Dn.Label(Term_dn.LambdaLabel, [d; c] @ l) - | Sort _ -> Dn.Label(Term_dn.SortLabel, []) - | Evar _ -> Dn.Everything - | _ -> Dn.Nothing - let lookup dn valu = let hkey = match (constr_val_discr valu) with diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index db2abea35..f2075d07d 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -16,26 +16,17 @@ open Nameops open Namegen open Term open Termops -open Sign open Reduction -open Proof_type -open Declarations open Tacticals open Tacmach -open Evar_refiner open Tactics -open Pattern open Patternops open Clenv -open Auto open Glob_term -open Hiddentac open Typeclasses open Typeclasses_errors open Classes open Constrexpr -open Pfedit -open Command open Libnames open Globnames open Evd @@ -1345,9 +1336,7 @@ let cl_rewrite_clause l left2right occs clause gl = cl_rewrite_clause_strat (rewrite_with (general_rewrite_unif_flags ()) l left2right occs) clause gl open Pp -open Pcoq open Names -open Tacexpr open Tacinterp open Termops open Genarg @@ -1380,8 +1369,6 @@ let interp_glob_constr_list env sigma = let evd, c = Pretyping.understand_tcc sigma env c in (evd, (c, NoBindings)), true) -open Pcoq - (* Syntax for rewriting with strategies *) type constr_expr_with_bindings = constr_expr with_bindings diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 9bbb09589..0c7d6e0ca 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -7,7 +7,6 @@ (************************************************************************) open Constrintern -open Closure open Libobject open Pattern open Patternops @@ -147,14 +146,6 @@ let ((value_in : value -> Dyn.t), (value_out : Dyn.t -> value)) = Dyn.create "value" let valueIn t = TacDynamic (Loc.ghost,value_in t) -let valueOut = function - | TacDynamic (_,d) -> - if (Dyn.tag d) = "value" then - value_out d - else - anomalylabstrm "valueOut" (str "Dynamic tag should be value") - | ast -> - anomalylabstrm "valueOut" (str "Not a Dynamic ast: ") (* Table of "pervasives" macros tactics (e.g. auto, simpl, etc.) *) let atomic_mactab = ref Idmap.empty @@ -1291,9 +1282,6 @@ let interp_constr = interp_constr_gen (OfType None) let interp_type = interp_constr_gen IsType (* Interprets an open constr *) -let interp_open_constr_gen kind ist = - interp_gen kind ist false true false false - let interp_open_constr ccl ist = interp_gen (OfType ccl) ist false true false (ccl<>None) @@ -3192,16 +3180,6 @@ let tacticIn t = (str "Incorrect tactic expression. Received exception is:" ++ Errors.print e)) -let tacticOut = function - | TacArg (_,TacDynamic (_,d)) -> - if (Dyn.tag d) = "tactic" then - tactic_out d - else - anomalylabstrm "tacticOut" (str "Dynamic tag should be tactic") - | ast -> - anomalylabstrm "tacticOut" - (str "Not a Dynamic ast: " (* ++ print_ast ast*) ) - (***************************************************************************) (* Backwarding recursive needs of tactic glob/interp/eval functions *) diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 39f60e196..61b80b584 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -52,6 +52,7 @@ val tclAT_LEAST_ONCE : tactic -> tactic val tclFAIL : int -> std_ppcmds -> tactic val tclFAIL_lazy : int -> std_ppcmds Lazy.t -> tactic val tclDO : int -> tactic -> tactic +val tclTIMEOUT : int -> tactic -> tactic val tclWEAK_PROGRESS : tactic -> tactic val tclPROGRESS : tactic -> tactic val tclSHOWHYPS : tactic -> tactic diff --git a/tactics/tactics.ml b/tactics/tactics.ml index a29ab24ba..e55ba5d0e 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1910,8 +1910,6 @@ let re_intro_dependent_hypotheses (lstatus,rstatus) (_,tophyp) = (intros_move rstatus) (intros_move newlstatus) -let update destopt tophyp = if destopt = MoveLast then tophyp else destopt - let safe_dest_intros_patterns avoid thin dest pat tac gl = try intros_patterns true avoid [] thin dest tac pat gl with UserError ("move_hyp",_) -> @@ -2650,9 +2648,6 @@ let rebuild_elimtype_from_scheme (scheme:elim_scheme): types = paramconcl -exception NoLastArg -exception NoLastArgCcl - (* Builds an elim_scheme from its type and calling form (const+binding). We first separate branches. We obtain branches, hyps before (params + preds), hyps after (args <+ indarg if present>) and conclusion. Then we proceed as diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4 index fdfc2b783..afd0e7799 100644 --- a/tactics/tauto.ml4 +++ b/tactics/tauto.ml4 @@ -13,13 +13,11 @@ open Hipattern open Names open Globnames open Pp -open Proof_type open Tacticals open Tacinterp open Tactics open Errors open Util -open Genarg let assoc_var s ist = match List.assoc (Names.id_of_string s) ist.lfun with diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index 74e4701c0..d1e379cca 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/cerrors.ml @@ -8,7 +8,6 @@ open Pp open Errors -open Util open Indtypes open Type_errors open Pretype_errors diff --git a/toplevel/class.ml b/toplevel/class.ml index 7fe923954..ff0e9fcfb 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -33,7 +33,6 @@ type coercion_error_kind = | NoTarget | WrongTarget of cl_typ * cl_typ | NotAClass of global_reference - | NotEnoughClassArgs of cl_typ exception CoercionError of coercion_error_kind @@ -60,8 +59,6 @@ let explain_coercion_error g = function | NotAClass ref -> (str "Type of " ++ Printer.pr_global ref ++ str " does not end with a sort") - | NotEnoughClassArgs cl -> - (str"Wrong number of parameters for " ++ pr_class cl) (* Verifications pour l'ajout d'une classe *) diff --git a/toplevel/classes.ml b/toplevel/classes.ml index c4c017577..5fe3d3f12 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -67,7 +67,6 @@ type binder_list = (identifier Loc.located * bool * constr_expr) list (* Declare everything in the parameters as implicit, and the class instance as well *) - let type_ctx_instance evars env ctx inst subst = let rec aux (subst, instctx) l = function (na, b, t) :: ctx -> @@ -94,8 +93,6 @@ let id_of_class cl = open Pp -let ($$) g f = fun x -> g (f x) - let instance_hook k pri global imps ?hook cst = Impargs.maybe_declare_manual_implicits false cst ~enriching:false imps; Typeclasses.declare_instance pri (not global) cst; @@ -312,9 +309,6 @@ let named_of_rel_context l = l ([], []) in ctx -let string_of_global r = - string_of_qualid (Nametab.shortest_qualid_of_global Idset.empty r) - let context l = let env = Global.env() in let evars = ref Evd.empty in diff --git a/toplevel/command.ml b/toplevel/command.ml index 873cfb09e..edde7c652 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -32,7 +32,6 @@ open Decl_kinds open Pretyping open Evarutil open Evarconv -open Notation open Indschemes open Misctypes @@ -204,10 +203,6 @@ let declare_assumptions idl is_coe k c imps impl_is_on nl = (* 3b| Mutual inductive definitions *) -let push_named_types env idl tl = - List.fold_left2 (fun env id t -> Environ.push_named (id,None,t) env) - env idl tl - let push_types env idl tl = List.fold_left2 (fun env id t -> Environ.push_rel (Name id,None,t) env) env idl tl @@ -546,7 +541,6 @@ open Coqlib let contrib_name = "Program" let subtac_dir = [contrib_name] let fixsub_module = subtac_dir @ ["Wf"] -let utils_module = subtac_dir @ ["Utils"] let tactics_module = subtac_dir @ ["Tactics"] let init_reference dir s () = Coqlib.gen_reference "Command" dir s @@ -858,24 +852,6 @@ let extract_cofixpoint_components l = {fix_name = id; fix_annot = None; fix_binders = bl; fix_body = def; fix_type = typ}) fixl, List.flatten ntnl -let check_program_evars env initial_sigma evd c = - let sigma = evd in - let c = nf_evar sigma c in - let rec proc_rec c = - match kind_of_term c with - | Evar (evk,args) -> - assert (Evd.mem sigma evk); - if not (Evd.mem initial_sigma evk) then - let (loc,k) = Evd.evar_source evk evd in - (match k with - | Evar_kinds.QuestionMark _ - | Evar_kinds.ImplicitArg (_, _, false) -> () - | _ -> - let evi = nf_evar_info sigma (Evd.find sigma evk) in - Pretype_errors.error_unsolvable_implicit loc env sigma evi k None) - | _ -> iter_constr proc_rec c - in proc_rec c - let out_def = function | Some def -> def | None -> error "Program Fixpoint needs defined bodies." diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4 index ff6f00475..09dd2a67f 100644 --- a/toplevel/mltop.ml4 +++ b/toplevel/mltop.ml4 @@ -12,9 +12,7 @@ open Pp open Flags open CUnix open Libobject -open Library open System -open Vernacinterp (* Code to hook Coq into the ML toplevel -- depends on having the objective-caml compiler mostly visible. The functions implemented here are: diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index b4e6eb543..775212eda 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -3,7 +3,6 @@ open Globnames open Libobject open Entries open Decl_kinds -open Util open Declare (** @@ -201,18 +200,8 @@ let sort_dependencies evl = | [] -> List.rev list in aux evl Intset.empty [] -let map_evar_body f = function - | Evar_empty -> Evar_empty - | Evar_defined c -> Evar_defined (f c) - open Environ - -let map_evar_info f evi = - { evi with evar_hyps = - val_of_named_context (map_named_context f (named_context_of_val evi.evar_hyps)); - evar_concl = f evi.evar_concl; - evar_body = map_evar_body f evi.evar_body } - + let eterm_obligations env name evm fs ?status t ty = (* 'Serialize' the evars *) let nc = Environ.named_context env in @@ -287,7 +276,6 @@ let tactics_module = ["Program";"Tactics"] let safe_init_constant md name () = Coqlib.check_required_library ("Coq"::md); Coqlib.gen_constant "Obligations" md name -let fix_proto = safe_init_constant tactics_module "fix_proto" let hide_obligation = safe_init_constant tactics_module "obligation" let pperror cmd = Errors.errorlabstrm "Program" cmd @@ -477,8 +465,6 @@ let _ = Summary.unfreeze_function = unfreeze; Summary.init_function = init } -let progmap_union = ProgMap.fold ProgMap.add - let close sec = if not (ProgMap.is_empty !from_prg) then let keys = map_keys !from_prg in @@ -714,15 +700,10 @@ let dependencies obls n = obls; !res -let global_kind = Decl_kinds.IsDefinition Decl_kinds.Definition let goal_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Definition -let global_proof_kind = Decl_kinds.IsProof Decl_kinds.Lemma let goal_proof_kind = Decl_kinds.Global, Decl_kinds.Proof Decl_kinds.Lemma -let global_fix_kind = Decl_kinds.IsDefinition Decl_kinds.Fixpoint -let goal_fix_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Fixpoint - let kind_of_opacity o = match o with | Evar_kinds.Define false | Evar_kinds.Expand -> goal_kind @@ -983,8 +964,6 @@ let admit_obligations n = let prg = get_prog_err n in admit_prog prg -exception Found of int - let next_obligation n tac = let prg = match n with | None -> get_any_prog_err () diff --git a/toplevel/record.ml b/toplevel/record.ml index 487add316..3332558a8 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -288,13 +288,6 @@ let implicits_of_context ctx = in ExplByPos (i, explname), (true, true, true)) 1 (List.rev (Anonymous :: (List.map pi1 ctx))) -let declare_instance_cst glob con pri = - let instance = Typeops.type_of_constant (Global.env ()) con in - let _, r = decompose_prod_assum instance in - match class_of_constr r with - | Some (_, (tc, _)) -> add_instance (new_instance tc pri glob (ConstRef con)) - | None -> errorlabstrm "" (Pp.strbrk "Constant does not build instances of a declared type class.") - let declare_class finite def infer id idbuild paramimpls params arity fieldimpls fields ?(kind=StructureComponent) ?name is_coe coers priorities sign = let fieldimpls = diff --git a/toplevel/search.ml b/toplevel/search.ml index 81fdf84aa..d66260c60 100644 --- a/toplevel/search.ml +++ b/toplevel/search.ml @@ -96,8 +96,6 @@ let crible ref = gen_crible (Some ref) (* Fine Search. By Yves Bertot. *) -exception No_full_path - let rec head c = let c = strip_outer_cast c in match kind_of_term c with @@ -116,7 +114,6 @@ let format_display l = prlist_with_sep fnl (fun x -> x) (List.rev l) let filter_by_module (module_list:dir_path list) (accept:bool) (ref:global_reference) _ _ = - try let sp = path_of_global ref in let sl = dirpath sp in let rec filter_aux = function @@ -124,8 +121,6 @@ let filter_by_module (module_list:dir_path list) (accept:bool) | [] -> true in xor accept (filter_aux module_list) - with No_full_path -> - false let ref_eq = Globnames.encode_mind Coqlib.logic_module (id_of_string "eq"), 0 let c_eq = mkInd ref_eq diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml index 5b848e834..dca47f714 100644 --- a/toplevel/vernacinterp.ml +++ b/toplevel/vernacinterp.ml @@ -8,7 +8,6 @@ open Pp open Errors -open Util let disable_drop e = if e <> Drop then e diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4 index ff03362a1..6aade9479 100644 --- a/toplevel/whelp.ml4 +++ b/toplevel/whelp.ml4 @@ -11,10 +11,8 @@ open Flags open Pp open Errors -open System open Names open Term -open Environ open Glob_term open Libnames open Globnames @@ -22,11 +20,8 @@ open Nametab open Detyping open Constrintern open Dischargedhypsmap -open Command open Pfedit -open Refiner open Tacmach -open Syntax_def open Misctypes (* Coq interface to the Whelp query engine developed at |