aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--plugins/subtac/subtac_obligations.ml19
-rw-r--r--plugins/subtac/subtac_obligations.mli1
-rw-r--r--pretyping/typeclasses_errors.ml2
-rw-r--r--proofs/refiner.ml6
-rw-r--r--proofs/refiner.mli3
-rw-r--r--tactics/class_tactics.ml41
-rw-r--r--tactics/refine.ml2
-rw-r--r--tactics/rewrite.ml45
-rw-r--r--tactics/tacinterp.ml2
-rw-r--r--tactics/tacticals.ml1
-rw-r--r--tactics/tacticals.mli1
-rw-r--r--toplevel/cerrors.ml4
-rw-r--r--toplevel/himsg.ml2
13 files changed, 29 insertions, 20 deletions
diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml
index 92ece7fe4..a54b3a86f 100644
--- a/plugins/subtac/subtac_obligations.ml
+++ b/plugins/subtac/subtac_obligations.ml
@@ -238,6 +238,7 @@ let reduce_fix =
let declare_mutual_definition l =
let len = List.length l in
+ let first = List.hd l in
let fixdefs, fixtypes, fiximps =
list_split3
(List.map (fun x ->
@@ -245,11 +246,11 @@ let declare_mutual_definition l =
(strip_lam_n len subs), snd (decompose_prod_n len typ), x.prg_implicits) l)
in
(* let fixdefs = List.map reduce_fix fixdefs in *)
- let fixkind = Option.get (List.hd l).prg_fixkind in
+ let fixkind = Option.get first.prg_fixkind in
let arrrec, recvec = Array.of_list fixtypes, Array.of_list fixdefs in
let fixdecls = (Array.of_list (List.map (fun x -> Name x.prg_name) l), arrrec, recvec) in
- let boxed = true (* TODO *) in
- let fixnames = (List.hd l).prg_deps in
+ let (local,boxed,kind) = first.prg_kind in
+ let fixnames = first.prg_deps in
let kind = if fixkind <> IsCoFixpoint then Fixpoint else CoFixpoint in
let indexes, fixdecls =
match fixkind with
@@ -264,9 +265,11 @@ let declare_mutual_definition l =
(* Declare the recursive definitions *)
let kns = list_map4 (declare_fix boxed kind) fixnames fixdecls fixtypes fiximps in
(* Declare notations *)
- List.iter (Command.declare_interning_data ([],[])) (List.hd l).prg_notations;
+ List.iter (Command.declare_interning_data ([],[])) first.prg_notations;
Flags.if_verbose ppnl (Command.recursive_message kind indexes fixnames);
- (match List.hd kns with ConstRef kn -> kn | _ -> assert false)
+ let gr = List.hd kns in
+ let kn = match gr with ConstRef kn -> kn | _ -> assert false in
+ first.prg_hook local gr; kn
let declare_obligation obl body =
match obl.obl_status with
@@ -468,7 +471,7 @@ and solve_obligation_by_tac prg obls i tac =
| Stdpp.Exc_located(_, Proof_type.LtacLocated (_, Refiner.FailError (_, s)))
| Stdpp.Exc_located(_, Refiner.FailError (_, s))
| Refiner.FailError (_, s) ->
- user_err_loc (obl.obl_location, "solve_obligation", s)
+ user_err_loc (obl.obl_location, "solve_obligation", Lazy.force s)
| e -> false)
and solve_prg_obligations prg tac =
@@ -547,11 +550,11 @@ let add_definition n b t ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic
| Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res
| _ -> res)
-let add_mutual_definitions l ?tactic ?(kind=Global,false,Definition) notations fixkind =
+let add_mutual_definitions l ?tactic ?(kind=Global,false,Definition) ?(hook=fun _ _ -> ()) notations fixkind =
let deps = List.map (fun (n, b, t, imps, obls) -> n) l in
let upd = List.fold_left
(fun acc (n, b, t, imps, obls) ->
- let prg = init_prog_info n b t deps (Some fixkind) notations obls imps kind (fun _ _ -> ()) in
+ let prg = init_prog_info n b t deps (Some fixkind) notations obls imps kind hook in
ProgMap.add n prg acc)
!from_prg l
in
diff --git a/plugins/subtac/subtac_obligations.mli b/plugins/subtac/subtac_obligations.mli
index 50f189dde..2afcb1941 100644
--- a/plugins/subtac/subtac_obligations.mli
+++ b/plugins/subtac/subtac_obligations.mli
@@ -34,6 +34,7 @@ val add_mutual_definitions :
(Topconstr.explicitation * (bool * bool * bool)) list * obligation_info) list ->
?tactic:Proof_type.tactic ->
?kind:Decl_kinds.definition_kind ->
+ ?hook:Tacexpr.declaration_hook ->
notations ->
Command.fixpoint_kind -> unit
diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index f1a57ffc1..c7e3895e0 100644
--- a/pretyping/typeclasses_errors.ml
+++ b/pretyping/typeclasses_errors.ml
@@ -47,7 +47,7 @@ let unsatisfiable_constraints env evd ev =
| None ->
raise (TypeClassError (env, UnsatisfiableConstraints (evd, None)))
| Some ev ->
- let evi = Evd.find ( evd) ev in
+ let evi = Evd.find evd ev in
let loc, kind = Evd.evar_source ev evd in
raise (Stdpp.Exc_located (loc, TypeClassError
(env, UnsatisfiableConstraints (evd, Some (evi, kind)))))
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index b0239eeb4..8b3789c3b 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -335,10 +335,12 @@ let tclIDTAC_MESSAGE s gls =
let tclFAIL_s s gls = errorlabstrm "Refiner.tclFAIL_s" (str s)
(* A special exception for levels for the Fail tactic *)
-exception FailError of int * std_ppcmds
+exception FailError of int * std_ppcmds Lazy.t
(* The Fail tactic *)
-let tclFAIL lvl s g = raise (FailError (lvl,s))
+let tclFAIL lvl s g = raise (FailError (lvl,lazy s))
+
+let tclFAIL_lazy lvl s g = raise (FailError (lvl,s))
let start_tac gls =
let (sigr,g) = unpackage gls in
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index d6bd73ca4..9a587a965 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -134,7 +134,7 @@ val tclTHENLASTn : tactic -> tactic array -> tactic
val tclTHENFIRSTn : tactic -> tactic array -> tactic
(* A special exception for levels for the Fail tactic *)
-exception FailError of int * Pp.std_ppcmds
+exception FailError of int * Pp.std_ppcmds Lazy.t
(* Takes an exception and either raise it at the next
level or do nothing. *)
@@ -151,6 +151,7 @@ val tclTHENTRY : tactic -> tactic -> tactic
val tclCOMPLETE : tactic -> tactic
val tclAT_LEAST_ONCE : tactic -> tactic
val tclFAIL : int -> Pp.std_ppcmds -> tactic
+val tclFAIL_lazy : int -> Pp.std_ppcmds Lazy.t -> tactic
val tclDO : int -> tactic -> tactic
val tclPROGRESS : tactic -> tactic
val tclWEAK_PROGRESS : tactic -> tactic
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 8f548210b..9146d02c5 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -452,7 +452,6 @@ let resolve_all_evars debug m env p oevd do_split fail =
if fail then
(* Unable to satisfy the constraints. *)
let evm = if do_split then select_evars comp evd else evd in
- let evm = Evarutil.nf_evars evm in
let _, ev = Evd.fold
(fun ev evi (b,acc) ->
(* focus on one instance if only one was searched for *)
diff --git a/tactics/refine.ml b/tactics/refine.ml
index f1ecc4da9..ff644c143 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -372,7 +372,7 @@ let rec tcc_aux subst (TH (c,mm,sgp) as _th) gl =
let refine (evd,c) gl =
let sigma = project gl in
- let evd = Typeclasses.resolve_typeclasses (pf_env gl) evd in
+ let evd = Typeclasses.resolve_typeclasses ~onlyargs:true (pf_env gl) evd in
let c = Evarutil.nf_evar evd c in
let (evd,c) = Evarutil.evars_to_metas sigma (evd,c) in
(* Relies on Cast's put on Meta's by evars_to_metas, because it is otherwise
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 213dcc8d2..7260f1fd7 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -834,8 +834,9 @@ let cl_rewrite_clause_aux ?(abs=None) strat goal_meta clause gl =
with
| Stdpp.Exc_located (_, TypeClassError (env, (UnsatisfiableConstraints _ as e)))
| TypeClassError (env, (UnsatisfiableConstraints _ as e)) ->
- tclFAIL 0 (str"setoid rewrite failed: unable to satisfy the rewriting constraints."
- ++ fnl () ++ Himsg.explain_typeclass_error env e) gl)
+ Refiner.tclFAIL_lazy 0
+ (lazy (str"setoid rewrite failed: unable to satisfy the rewriting constraints."
+ ++ fnl () ++ Himsg.explain_typeclass_error env e)) gl)
| Some None ->
tclFAIL 0 (str"setoid rewrite failed: no progress made") gl
| None -> raise Not_found
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index c21a4c080..0942fde83 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1918,7 +1918,7 @@ and eval_with_fail ist is_lazy goal tac =
with
| FailError (0,s) | Stdpp.Exc_located(_, FailError (0,s))
| Stdpp.Exc_located(_,LtacLocated (_,FailError (0,s))) ->
- raise (Eval_fail s)
+ raise (Eval_fail (Lazy.force s))
| FailError (lvl,s) -> raise (FailError (lvl - 1, s))
| Stdpp.Exc_located(s,FailError (lvl,s')) ->
raise (Stdpp.Exc_located(s,FailError (lvl - 1, s')))
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index ab7120b8b..2b69d7233 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -59,6 +59,7 @@ let tclINFO = Refiner.tclINFO
let tclCOMPLETE = Refiner.tclCOMPLETE
let tclAT_LEAST_ONCE = Refiner.tclAT_LEAST_ONCE
let tclFAIL = Refiner.tclFAIL
+let tclFAIL_lazy = Refiner.tclFAIL_lazy
let tclDO = Refiner.tclDO
let tclPROGRESS = Refiner.tclPROGRESS
let tclWEAK_PROGRESS = Refiner.tclWEAK_PROGRESS
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index fe6dd2d64..762c7dc76 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -53,6 +53,7 @@ val tclINFO : tactic -> tactic
val tclCOMPLETE : tactic -> tactic
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 tclPROGRESS : tactic -> tactic
val tclWEAK_PROGRESS : tactic -> tactic
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index 4250040ec..f9a336430 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -85,7 +85,7 @@ let rec explain_exn_default_aux anomaly_string report_fn = function
hov 0 (str "Error:" ++ spc () ++ Himsg.explain_inductive_error e)
| RecursionSchemeError e ->
hov 0 (str "Error:" ++ spc () ++ Himsg.explain_recursion_scheme_error e)
- | Proof_type.LtacLocated (_,(Refiner.FailError (i,s) as exc)) when s <> mt () ->
+ | Proof_type.LtacLocated (_,(Refiner.FailError (i,s) as exc)) when Lazy.force s <> mt () ->
explain_exn_default_aux anomaly_string report_fn exc
| Proof_type.LtacLocated (s,exc) ->
hov 0 (Himsg.explain_ltac_call_trace s ++ fnl ()
@@ -108,7 +108,7 @@ let rec explain_exn_default_aux anomaly_string report_fn = function
Libnames.pr_qualid q ++ str ".")
| Refiner.FailError (i,s) ->
hov 0 (str "Error: Tactic failure" ++
- (if s <> mt() then str ":" ++ s else mt ()) ++
+ (if Lazy.force s <> mt() then str ":" ++ Lazy.force s else mt ()) ++
if i=0 then str "." else str " (level " ++ int i ++ str").")
| Stdpp.Exc_located (loc,exc) ->
hov 0 ((if loc = dummy_loc then (mt ())
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 4e5eded8e..e8a8dcb7c 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -525,7 +525,7 @@ let pr_constraints printenv env evm =
pr_evar_defs evm
let explain_unsatisfiable_constraints env evd constr =
- let evm = evd in
+ let evm = Evarutil.nf_evars evd in
match constr with
| None ->
str"Unable to satisfy the following constraints:" ++ fnl() ++
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-11 08:00:35 +0000