aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--engine/proofview_monad.ml5
-rw-r--r--ide/coq.ml5
-rw-r--r--ide/document.ml6
-rw-r--r--ide/wg_ProofView.ml13
-rw-r--r--interp/constrextern.ml9
-rw-r--r--interp/constrintern.ml13
-rw-r--r--kernel/declareops.ml2
-rw-r--r--kernel/nativevalues.ml27
-rw-r--r--kernel/safe_typing.ml7
-rw-r--r--kernel/term.ml11
-rw-r--r--lib/heap.ml2
-rw-r--r--library/loadpath.ml4
-rw-r--r--pretyping/evarsolve.ml15
-rw-r--r--pretyping/pretyping.ml14
-rw-r--r--pretyping/tacred.ml6
-rw-r--r--printing/ppconstr.ml2
-rw-r--r--printing/pptactic.ml5
-rw-r--r--proofs/redexpr.ml2
-rw-r--r--stm/asyncTaskQueue.ml4
-rw-r--r--tactics/auto.ml3
-rw-r--r--tactics/class_tactics.ml8
-rw-r--r--tactics/hints.ml21
-rw-r--r--tactics/tacinterp.ml3
23 files changed, 1 insertions, 186 deletions
diff --git a/engine/proofview_monad.ml b/engine/proofview_monad.ml
index a9faf0a83..88c5925ce 100644
--- a/engine/proofview_monad.ml
+++ b/engine/proofview_monad.ml
@@ -108,11 +108,6 @@ module Info = struct
and compress f =
CList.map_filter compress_tree f
- let rec is_empty = let open Trace in function
- | Seq(Dispatch,brs) -> List.for_all is_empty brs
- | Seq(DBranch,br) -> List.for_all is_empty br
- | _ -> false
-
(** [with_sep] is [true] when [Tactic m] must be printed with a
trailing semi-colon. *)
let rec pr_tree with_sep = let open Trace in function
diff --git a/ide/coq.ml b/ide/coq.ml
index a60f327b4..268a95a33 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -99,9 +99,6 @@ let display_coqtop_answer cmd lines =
"Command was: "^cmd^"\n"^
"Answer was: "^(String.concat "\n " lines))
-let check_remaining_opt arg =
- if arg <> "" && arg.[0] = '-' then fatal_error_popup ("Illegal option: "^arg)
-
let rec filter_coq_opts args =
let argstr = String.concat " " (List.map Filename.quote args) in
let cmd = Filename.quote (coqtop_path ()) ^" -nois -filteropts " ^ argstr in
@@ -200,8 +197,6 @@ module GlibMainLoop = struct
let read_all = Ideutils.io_read_all
let async_chan_of_file fd = Glib.Io.channel_of_descr fd
let async_chan_of_socket s = !gio_channel_of_descr_socket s
- let add_timeout ~sec callback =
- ignore(Glib.Timeout.add ~ms:(sec * 1000) ~callback)
end
module CoqTop = Spawn.Async(GlibMainLoop)
diff --git a/ide/document.ml b/ide/document.ml
index 41d5a7564..bb431e791 100644
--- a/ide/document.ml
+++ b/ide/document.ml
@@ -124,12 +124,6 @@ let context d =
let pair _ x y = try Option.get x, y with Option.IsNone -> assert false in
List.map (flat pair true) top, List.map (flat pair true) bot
-let iter d f =
- let a, s, b = to_lists d in
- List.iter (flat f false) a;
- List.iter (flat f true) s;
- List.iter (flat f false) b
-
let stateid_opt_equal = Option.equal Stateid.equal
let is_in_focus d id =
diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml
index 148add6e9..642a57787 100644
--- a/ide/wg_ProofView.ml
+++ b/ide/wg_ProofView.ml
@@ -114,19 +114,6 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals hints = match goals with
(Some Tags.Proof.goal)));
ignore(proof#scroll_to_mark ~use_align:true ~yalign:0.95 `INSERT)
-let mode_cesar (proof : #GText.view_skel) = function
- | [] -> assert false
- | { Interface.goal_hyp = hyps; Interface.goal_ccl = cur_goal; } :: _ ->
- proof#buffer#insert " *** Declarative Mode ***\n";
- List.iter
- (fun hyp -> insert_xml proof#buffer hyp; proof#buffer#insert "\n")
- hyps;
- proof#buffer#insert "______________________________________\n";
- proof#buffer#insert "thesis := \n ";
- insert_xml proof#buffer cur_goal;
- proof#buffer#insert "\n";
- ignore (proof#scroll_to_iter (proof#buffer#get_iter_at_mark `INSERT))
-
let rec flatten = function
| [] -> []
| (lg, rg) :: l ->
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index ed85c38de..5c9e80df3 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -462,15 +462,6 @@ let is_needed_for_correct_partial_application tail imp =
exception Expl
-let params_implicit n impl =
- let rec aux n impl =
- if n == 0 then true
- else match impl with
- | [] -> false
- | imp :: impl when is_status_implicit imp -> aux (pred n) impl
- | _ -> false
- in aux n impl
-
(* Implicit args indexes are in ascending order *)
(* inctx is useful only if there is a last argument to be deduced from ctxt *)
let explicitize loc inctx impl (cf,f) args =
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index d4cb79775..f9de8c466 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -698,19 +698,6 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id =
(* [id] a goal variable *)
GVar (loc,id), [], [], []
-let proj_impls r impls =
- let env = Global.env () in
- let f (x, l) = x, projection_implicits env r l in
- List.map f impls
-
-let proj_scopes n scopes =
- List.skipn_at_least n scopes
-
-let proj_impls_scopes p impls scopes =
- match p with
- | Some (r, n) -> proj_impls r impls, proj_scopes n scopes
- | None -> impls, scopes
-
let find_appl_head_data c =
match c with
| GRef (loc,ref,_) as x ->
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 73cfd0122..803df7827 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -391,5 +391,3 @@ and hcons_module_body mb =
mod_delta = delta';
mod_retroknowledge = retroknowledge';
}
-
-and hcons_module_type_body mtb = hcons_module_body mtb
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index 40bef4bc6..6e097b613 100644
--- a/kernel/nativevalues.ml
+++ b/kernel/nativevalues.ml
@@ -78,8 +78,6 @@ let accumulate_code (k:accumulator) (x:t) =
let rec accumulate (x:t) =
accumulate_code (Obj.magic accumulate) x
-let raccumulate = ref accumulate
-
let mk_accu_gen rcode (a:atom) =
(* Format.eprintf "size rcode =%i\n" (Obj.size (Obj.magic rcode)); *)
let r = Obj.new_block 0 3 in
@@ -160,31 +158,6 @@ let is_accu x =
let o = Obj.repr x in
Obj.is_block o && Int.equal (Obj.tag o) accumulate_tag
-(*let accumulate_fix_code (k:accumulator) (a:t) =
- match atom_of_accu k with
- | Afix(frec,_,rec_pos,_,_) ->
- let nargs = accu_nargs k in
- if nargs <> rec_pos || is_accu a then
- accumulate_code k a
- else
- let r = ref frec in
- for i = 0 to nargs - 1 do
- r := !r (arg_of_accu k i)
- done;
- !r a
- | _ -> assert false
-
-
-let rec accumulate_fix (x:t) =
- accumulate_fix_code (Obj.magic accumulate_fix) x
-
-let raccumulate_fix = ref accumulate_fix *)
-
-let is_atom_fix (a:atom) =
- match a with
- | Afix _ -> true
- | _ -> false
-
let mk_fix_accu rec_pos pos types bodies =
mk_accu_gen accumulate (Afix(types,bodies,rec_pos, pos))
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index c7ab6491d..33aa2972b 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -222,13 +222,6 @@ let inline_private_constants_in_constr = Term_typing.inline_side_effects
let inline_private_constants_in_definition_entry = Term_typing.inline_entry_side_effects
let side_effects_of_private_constants x = Term_typing.uniq_seff (List.rev x)
-let constant_entry_of_private_constant = function
- | { Entries.eff = Entries.SEsubproof (kn, cb, eff_env) } ->
- [ kn, Term_typing.constant_entry_of_side_effect cb eff_env ]
- | { Entries.eff = Entries.SEscheme (l,_) } ->
- List.map (fun (_,kn,cb,eff_env) ->
- kn, Term_typing.constant_entry_of_side_effect cb eff_env) l
-
let private_con_of_con env c =
let cbo = Environ.lookup_constant c env.env in
{ Entries.from_env = Ephemeron.create env.revstruct;
diff --git a/kernel/term.ml b/kernel/term.ml
index 455248dd5..2060c7b6e 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -486,8 +486,6 @@ let lambda_applist c l =
let lambda_appvect c v = lambda_applist c (Array.to_list v)
-let lambda_app c a = lambda_applist c [a]
-
let lambda_applist_assum n c l =
let rec app n subst t l =
if Int.equal n 0 then
@@ -501,15 +499,6 @@ let lambda_applist_assum n c l =
let lambda_appvect_assum n c v = lambda_applist_assum n c (Array.to_list v)
-(* pseudo-reduction rule:
- * [prod_app s (Prod(_,B)) N --> B[N]
- * with an strip_outer_cast on the first argument to produce a product *)
-
-let prod_app t n =
- match kind_of_term (strip_outer_cast t) with
- | Prod (_,_,b) -> subst1 n b
- | _ -> anomaly (str"Needed a product, but didn't find one")
-
(* prod_applist T [ a1 ; ... ; an ] -> (T a1 ... an) *)
let prod_applist c l =
let rec app subst c l =
diff --git a/lib/heap.ml b/lib/heap.ml
index a19bc0d1c..5682b87bb 100644
--- a/lib/heap.ml
+++ b/lib/heap.ml
@@ -62,8 +62,6 @@ module Functional(X : Ordered) = struct
let empty = Leaf
- let is_empty t = t = Leaf
-
let rec add x = function
| Leaf ->
Node (Leaf, x, Leaf)
diff --git a/library/loadpath.ml b/library/loadpath.ml
index 16b419454..f77bd1ef5 100644
--- a/library/loadpath.ml
+++ b/library/loadpath.ml
@@ -84,10 +84,6 @@ let add_load_path phys_path coq_path ~implicit =
end
| _ -> anomaly_too_many_paths phys_path
-let extend_path_with_dirpath p dir =
- List.fold_left Filename.concat p
- (List.rev_map Id.to_string (DirPath.repr dir))
-
let filter_path f =
let rec aux = function
| [] -> []
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index fe26dcd28..69e8e9d98 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -1007,21 +1007,6 @@ let postpone_non_unique_projection env evd pbty (evk,argsv as ev) sols rhs =
* Note: argument f is the function used to instantiate evars.
*)
-let are_canonical_instances args1 args2 env =
- let n1 = Array.length args1 in
- let n2 = Array.length args2 in
- let rec aux n = function
- | (id,_,c)::sign
- when n < n1 && isVarId id args1.(n) && isVarId id args2.(n) ->
- aux (n+1) sign
- | [] ->
- let rec aux2 n =
- Int.equal n n1 ||
- (isRelN (n1-n) args1.(n) && isRelN (n1-n) args2.(n) && aux2 (n+1))
- in aux2 n
- | _ -> false in
- Int.equal n1 n2 && aux 0 (named_context env)
-
let filter_compatible_candidates conv_algo env evd evi args rhs c =
let c' = instantiate_evar_array evi c args in
match conv_algo env evd Reduction.CONV rhs c' with
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index f5b89e789..7d5496917 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -444,26 +444,12 @@ let new_type_evar env evdref loc =
univ_flexible_alg ~src:(loc,Evar_kinds.InternalHole)) evdref
in e
-let get_projection env cst =
- let cb = lookup_constant cst env in
- match cb.Declarations.const_proj with
- | Some {Declarations.proj_ind = mind; proj_npars = n;
- proj_arg = m; proj_type = ty} ->
- (cst,mind,n,m,ty)
- | None -> raise Not_found
-
let (f_genarg_interp, genarg_interp_hook) = Hook.make ()
(* [pretype tycon env evdref lvar lmeta cstr] attempts to type [cstr] *)
(* in environment [env], with existential variables [evdref] and *)
(* the type constraint tycon *)
-let is_GHole = function
- | GHole _ -> true
- | _ -> false
-
-let evars = ref Id.Map.empty
-
let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var_map) t =
let inh_conv_coerce_to_tycon = inh_conv_coerce_to_tycon resolve_tc in
let pretype_type = pretype_type k0 resolve_tc in
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 48911a5a9..31e75e550 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -940,8 +940,6 @@ let matches_head env sigma c t =
| Proj (p, _) -> Constr_matching.matches env sigma c (mkConst (Projection.constant p))
| _ -> raise Constr_matching.PatternMatchingFailure
-let is_pattern_meta = function Pattern.PMeta _ -> true | _ -> false
-
(** FIXME: Specific function to handle projections: it ignores what happens on the
parameters. This is a temporary fix while rewrite etc... are not up to equivalence
of the projection and its eta expanded form.
@@ -1055,10 +1053,6 @@ let unfold env sigma name =
else
error (string_of_evaluable_ref env name^" is opaque.")
-let is_projection env = function
- | EvalVarRef _ -> false
- | EvalConstRef c -> Environ.is_projection c env
-
(* [unfoldoccs : (readable_constraints -> (int list * full_path) -> constr -> constr)]
* Unfolds the constant name in a term c following a list of occurrences occl.
* at the occurrences of occ_list. If occ_list is empty, unfold all occurrences.
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index d15c3ee2f..c07057a09 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -136,8 +136,6 @@ end) = struct
let pr_sep_com sep f c = pr_with_comments (constr_loc c) (sep() ++ f c)
- let pr_in_comment pr x = str "(* " ++ pr x ++ str " *)"
-
let pr_univ l =
match l with
| [_,x] -> str x
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 7800f1edb..a5716279f 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -685,11 +685,6 @@ module Make
| l -> spc () ++
hov 2 (keyword "using" ++ spc () ++ prlist_with_sep pr_comma prc l)
- let string_of_debug = function
- | Off -> ""
- | Debug -> "debug "
- | Info -> "info_"
-
let pr_then () = str ";"
let ltop = (5,E)
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index be92f2b04..89ecdb0df 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -158,8 +158,6 @@ let make_flag env f =
f.rConst red
in red
-let is_reference = function PRef _ | PVar _ -> true | _ -> false
-
(* table of custom reductino fonctions, not synchronized,
filled via ML calls to [declare_reduction] *)
let reduction_tab = ref String.Map.empty
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index e525031e6..863bab7cc 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -60,9 +60,7 @@ module Make(T : Task) = struct
type more_data =
| MoreDataUnivLevel of Univ.universe_level list
-
- let request_expiry_of_task (t, c) = T.request_of_task t, c
-
+
let slave_respond (Request r) =
let res = T.perform r in
Response res
diff --git a/tactics/auto.ml b/tactics/auto.ml
index e6263f92c..d6552920f 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -67,9 +67,6 @@ let auto_unif_flags_of st1 st2 useeager =
let auto_unif_flags =
auto_unif_flags_of full_transparent_state empty_transparent_state false
-let auto_flags_of_state st =
- auto_unif_flags_of full_transparent_state st false
-
(* Try unification with the precompiled clause, then use registered Apply *)
let connect_hint_clenv poly (c, _, ctx) clenv gl =
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 4f0ffa024..8cd7b1ad6 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -569,14 +569,6 @@ let rec fix_limit limit (t : 'a tac) : 'a tac =
if Int.equal limit 0 then fail_tac ReachedLimit
else then_tac t { skft = fun sk fk -> (fix_limit (pred limit) t).skft sk fk }
-let fix_iterative' t =
- let rec aux depth =
- { skft = fun sk fk gls ->
- (fix_limit depth t).skft sk
- (function NotApplicable as e -> fk e
- | ReachedLimit -> (aux (succ depth)).skft sk fk gls) gls }
- in aux 1
-
let fix_iterative t =
let rec aux depth =
or_else_tac (fix_limit depth t)
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 6d623f1c3..8d8b5fcc6 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -154,27 +154,6 @@ let fresh_key =
in
KerName.make mp dir (Label.of_id lbl)
-let eq_hints_path_atom p1 p2 = match p1, p2 with
-| PathHints gr1, PathHints gr2 -> List.equal eq_gr gr1 gr2
-| PathAny, PathAny -> true
-| (PathHints _ | PathAny), _ -> false
-
-let eq_auto_tactic t1 t2 = match t1, t2 with
-| Res_pf (c1, _), Res_pf (c2, _) -> Constr.equal c1 c2
-| ERes_pf (c1, _), ERes_pf (c2, _) -> Constr.equal c1 c2
-| Give_exact (c1, _), Give_exact (c2, _) -> Constr.equal c1 c2
-| Res_pf_THEN_trivial_fail (c1, _), Res_pf_THEN_trivial_fail (c2, _) -> Constr.equal c1 c2
-| Unfold_nth gr1, Unfold_nth gr2 -> eq_egr gr1 gr2
-| Extern tac1, Extern tac2 -> tac1 == tac2 (** May cause redundancy in addkv *)
-| (Res_pf _ | ERes_pf _ | Give_exact _ | Res_pf_THEN_trivial_fail _
- | Unfold_nth _ | Extern _), _ -> false
-
-let eq_hint_metadata t1 t2 =
- Int.equal t1.pri t2.pri &&
- Option.equal constr_pattern_eq t1.pat t2.pat &&
- eq_hints_path_atom t1.name t2.name &&
- eq_auto_tactic t1.code t2.code
-
let pri_order_int (id1, {pri=pri1}) (id2, {pri=pri2}) =
let d = pri1 - pri2 in
if Int.equal d 0 then id2 - id1
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index a87181588..5450a00f4 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1115,9 +1115,6 @@ let rec read_match_rule lfun ist env sigma = function
(* misc *)
-let mk_hyp_value ist env sigma c =
- (mkVar (interp_hyp ist env sigma c))
-
let interp_focussed wit f v =
Ftactic.nf_enter begin fun gl ->
let v = Genarg.out_gen (glbwit wit) v in
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-20 04:30:08 +0000