aboutsummaryrefslogtreecommitdiff
path: root/engine
diff options
context:
space:
mode:
Diffstat (limited to 'engine')
-rw-r--r--engine/evarutil.ml18
-rw-r--r--engine/evarutil.mli17
-rw-r--r--engine/logic_monad.ml5
-rw-r--r--engine/logic_monad.mli2
-rw-r--r--engine/proofview.ml22
-rw-r--r--engine/proofview.mli15
6 files changed, 47 insertions, 32 deletions
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index ea71be8e43..c946125d3f 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -861,12 +861,12 @@ let compare_constructor_instances evd u u' =
in
Evd.add_universe_constraints evd soft
-(** [eq_constr_univs_test sigma1 sigma2 t u] tests equality of [t] and
- [u] up to existential variable instantiation and equalisable
- universes. The term [t] is interpreted in [sigma1] while [u] is
- interpreted in [sigma2]. The universe constraints in [sigma2] are
- assumed to be an extension of those in [sigma1]. *)
-let eq_constr_univs_test sigma1 sigma2 t u =
+(** [eq_constr_univs_test ~evd ~extended_evd t u] tests equality of
+ [t] and [u] up to existential variable instantiation and
+ equalisable universes. The term [t] is interpreted in [evd] while
+ [u] is interpreted in [extended_evd]. The universe constraints in
+ [extended_evd] are assumed to be an extension of those in [evd]. *)
+let eq_constr_univs_test ~evd ~extended_evd t u =
(* spiwack: mild code duplication with {!Evd.eq_constr_univs}. *)
let open Evd in
let t = EConstr.Unsafe.to_constr t
@@ -877,8 +877,8 @@ let eq_constr_univs_test sigma1 sigma2 t u =
in
let ans =
UnivProblem.eq_constr_univs_infer_with
- (fun t -> kind_of_term_upto sigma1 t)
- (fun u -> kind_of_term_upto sigma2 u)
- (universes sigma2) fold t u sigma2
+ (fun t -> kind_of_term_upto evd t)
+ (fun u -> kind_of_term_upto extended_evd u)
+ (universes extended_evd) fold t u extended_evd
in
match ans with None -> false | Some _ -> true
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index e9d579af32..7877b94582 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -204,12 +204,17 @@ val finalize : ?abort_on_undefined_evars:bool -> evar_map ->
val kind_of_term_upto : evar_map -> Constr.constr ->
(Constr.constr, Constr.types, Sorts.t, Univ.Instance.t) kind_of_term
-(** [eq_constr_univs_test sigma1 sigma2 t u] tests equality of [t] and
- [u] up to existential variable instantiation and equalisable
- universes. The term [t] is interpreted in [sigma1] while [u] is
- interpreted in [sigma2]. The universe constraints in [sigma2] are
- assumed to be an extension of those in [sigma1]. *)
-val eq_constr_univs_test : evar_map -> evar_map -> constr -> constr -> bool
+(** [eq_constr_univs_test ~evd ~extended_evd t u] tests equality of
+ [t] and [u] up to existential variable instantiation and
+ equalisable universes. The term [t] is interpreted in [evd] while
+ [u] is interpreted in [extended_evd]. The universe constraints in
+ [extended_evd] are assumed to be an extension of those in [evd]. *)
+val eq_constr_univs_test :
+ evd:Evd.evar_map ->
+ extended_evd:Evd.evar_map ->
+ constr ->
+ constr ->
+ bool
(** [compare_cumulative_instances cv_pb variance u1 u2 sigma] Returns
[Inl sigma'] where [sigma'] is [sigma] augmented with universe
diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml
index 7c06bb59f1..e3a5676942 100644
--- a/engine/logic_monad.ml
+++ b/engine/logic_monad.ml
@@ -30,7 +30,7 @@
exception Exception of exn
(** This exception is used to signal abortion in [timeout] functions. *)
-exception Timeout
+exception Tac_Timeout
(** This exception is used by the tactics to signal failure by lack of
successes, rather than some other exceptions (like system
@@ -38,7 +38,6 @@ exception Timeout
exception TacticFailure of exn
let _ = CErrors.register_handler begin function
- | Timeout -> CErrors.user_err ~hdr:"Some timeout function" (Pp.str"Timeout!")
| Exception e -> CErrors.print e
| TacticFailure e -> CErrors.print e
| _ -> raise CErrors.Unhandled
@@ -99,7 +98,7 @@ struct
let print_char = fun c -> (); fun () -> print_char c
let timeout = fun n t -> (); fun () ->
- Control.timeout n t () (Exception Timeout)
+ Control.timeout n t () (Exception Tac_Timeout)
let make f = (); fun () ->
try f ()
diff --git a/engine/logic_monad.mli b/engine/logic_monad.mli
index 90c920439a..75920455ce 100644
--- a/engine/logic_monad.mli
+++ b/engine/logic_monad.mli
@@ -30,7 +30,7 @@
exception Exception of exn
(** This exception is used to signal abortion in [timeout] functions. *)
-exception Timeout
+exception Tac_Timeout
(** This exception is used by the tactics to signal failure by lack of
successes, rather than some other exceptions (like system
diff --git a/engine/proofview.ml b/engine/proofview.ml
index 8b5bd4cd80..1f076470c1 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -849,7 +849,8 @@ let give_up =
module Progress = struct
- let eq_constr = Evarutil.eq_constr_univs_test
+ let eq_constr evd extended_evd =
+ Evarutil.eq_constr_univs_test ~evd ~extended_evd
(** equality function on hypothesis contexts *)
let eq_named_context_val sigma1 sigma2 ctx1 ctx2 =
@@ -879,10 +880,10 @@ module Progress = struct
eq_evar_body sigma1 sigma2 ei1.evar_body ei2.evar_body
(** Equality function on goals *)
- let goal_equal evars1 gl1 evars2 gl2 =
- let evi1 = Evd.find evars1 gl1 in
- let evi2 = Evd.find evars2 gl2 in
- eq_evar_info evars1 evars2 evi1 evi2
+ let goal_equal ~evd ~extended_evd evar extended_evar =
+ let evi = Evd.find evd evar in
+ let extended_evi = Evd.find extended_evd extended_evar in
+ eq_evar_info evd extended_evd evi extended_evi
end
@@ -899,17 +900,17 @@ let tclPROGRESS t =
let test =
quick_test ||
Util.List.for_all2eq begin fun i f ->
- Progress.goal_equal initial.solution (drop_state i) final.solution (drop_state f)
+ Progress.goal_equal ~evd:initial.solution
+ ~extended_evd:final.solution (drop_state i) (drop_state f)
end initial.comb final.comb
in
if not test then
tclUNIT res
else
- tclZERO (CErrors.UserError (Some "Proofview.tclPROGRESS" , Pp.str"Failed to progress."))
+ tclZERO (CErrors.UserError (Some "Proofview.tclPROGRESS", Pp.str "Failed to progress."))
-exception Timeout
let _ = CErrors.register_handler begin function
- | Timeout -> CErrors.user_err ~hdr:"Proofview.tclTIMEOUT" (Pp.str"Tactic timeout!")
+ | Logic_monad.Tac_Timeout -> CErrors.user_err ~hdr:"Proofview.tclTIMEOUT" (Pp.str"Tactic timeout!")
| _ -> raise CErrors.Unhandled
end
@@ -934,7 +935,8 @@ let tclTIMEOUT n t =
end
begin let open Logic_monad.NonLogical in function (e, info) ->
match e with
- | Logic_monad.Timeout -> return (Util.Inr (Timeout, info))
+ | Logic_monad.Tac_Timeout ->
+ return (Util.Inr (Logic_monad.Tac_Timeout, info))
| Logic_monad.TacticFailure e ->
return (Util.Inr (e, info))
| e -> Logic_monad.NonLogical.raise ~info e
diff --git a/engine/proofview.mli b/engine/proofview.mli
index f90f02f3e1..764a4a0058 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -398,14 +398,23 @@ val give_up : unit tactic
val tclPROGRESS : 'a tactic -> 'a tactic
module Progress : sig
- val goal_equal : Evd.evar_map -> Evar.t -> Evd.evar_map -> Evar.t -> bool
+(** [goal_equal ~evd ~extended_evd evar extended_evar] tests whether
+ the [evar_info] from [evd] corresponding to [evar] is equal to that
+ from [extended_evd] corresponding to [extended_evar], up to
+ existential variable instantiation and equalisable universes. The
+ universe constraints in [extended_evd] are assumed to be an
+ extension of the universe constraints in [evd]. *)
+ val goal_equal :
+ evd:Evd.evar_map ->
+ extended_evd:Evd.evar_map ->
+ Evar.t ->
+ Evar.t ->
+ bool
end
(** Checks for interrupts *)
val tclCHECKINTERRUPT : unit tactic
-exception Timeout
-
(** [tclTIMEOUT n t] can have only one success.
In case of timeout if fails with [tclZERO Timeout]. *)
val tclTIMEOUT : int -> 'a tactic -> 'a tactic
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 18:09:13 +0000