aboutsummaryrefslogtreecommitdiff
path: root/engine
diff options
context:
space:
mode:
Diffstat (limited to 'engine')
-rw-r--r--engine/eConstr.ml20
-rw-r--r--engine/evd.ml5
-rw-r--r--engine/evd.mli8
-rw-r--r--engine/proofview.ml12
-rw-r--r--engine/proofview.mli17
-rw-r--r--engine/proofview_monad.ml9
-rw-r--r--engine/proofview_monad.mli2
-rw-r--r--engine/termops.ml8
-rw-r--r--engine/termops.mli3
-rw-r--r--engine/uState.ml24
-rw-r--r--engine/uState.mli9
11 files changed, 59 insertions, 58 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 8493119ee5..8756ebfdf2 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -405,25 +405,17 @@ let compare_cumulative_instances cv_pb nargs_ok variances u u' cstrs =
let cmp_inductives cv_pb (mind,ind as spec) nargs u1 u2 cstrs =
let open UnivProblem in
- match mind.Declarations.mind_universes with
- | Declarations.Monomorphic_ind _ ->
- assert (Univ.Instance.length u1 = 0 && Univ.Instance.length u2 = 0);
- cstrs
- | Declarations.Polymorphic_ind _ ->
- enforce_eq_instances_univs false u1 u2 cstrs
- | Declarations.Cumulative_ind cumi ->
+ match mind.Declarations.mind_variance with
+ | None -> enforce_eq_instances_univs false u1 u2 cstrs
+ | Some variances ->
let num_param_arity = Reduction.inductive_cumulativity_arguments spec in
- let variances = Univ.ACumulativityInfo.variance cumi in
compare_cumulative_instances cv_pb (Int.equal num_param_arity nargs) variances u1 u2 cstrs
let cmp_constructors (mind, ind, cns as spec) nargs u1 u2 cstrs =
let open UnivProblem in
- match mind.Declarations.mind_universes with
- | Declarations.Monomorphic_ind _ ->
- cstrs
- | Declarations.Polymorphic_ind _ ->
- enforce_eq_instances_univs false u1 u2 cstrs
- | Declarations.Cumulative_ind cumi ->
+ match mind.Declarations.mind_variance with
+ | None -> enforce_eq_instances_univs false u1 u2 cstrs
+ | Some _ ->
let num_cnstr_args = Reduction.constructor_cumulativity_arguments spec in
if not (Int.equal num_cnstr_args nargs)
then enforce_eq_instances_univs false u1 u2 cstrs
diff --git a/engine/evd.ml b/engine/evd.ml
index eee2cb700c..f0433d3387 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -852,8 +852,9 @@ let universe_context_set d = UState.context_set d.universes
let to_universe_context evd = UState.context evd.universes
-let const_univ_entry ~poly evd = UState.const_univ_entry ~poly evd.universes
-let ind_univ_entry ~poly evd = UState.ind_univ_entry ~poly evd.universes
+let univ_entry ~poly evd = UState.univ_entry ~poly evd.universes
+
+let const_univ_entry = univ_entry
let check_univ_decl ~poly evd decl = UState.check_univ_decl ~poly evd.universes decl
diff --git a/engine/evd.mli b/engine/evd.mli
index de73144895..d2d18ca486 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -597,12 +597,12 @@ val universes : evar_map -> UGraph.t
[Univ.ContextSet.to_context]. *)
val to_universe_context : evar_map -> Univ.UContext.t
-val const_univ_entry : poly:bool -> evar_map -> Entries.constant_universes_entry
+val univ_entry : poly:bool -> evar_map -> Entries.universes_entry
-(** NB: [ind_univ_entry] cannot create cumulative entries. *)
-val ind_univ_entry : poly:bool -> evar_map -> Entries.inductive_universes
+val const_univ_entry : poly:bool -> evar_map -> Entries.universes_entry
+[@@ocaml.deprecated "Use [univ_entry]."]
-val check_univ_decl : poly:bool -> evar_map -> UState.universe_decl -> Entries.constant_universes_entry
+val check_univ_decl : poly:bool -> evar_map -> UState.universe_decl -> Entries.universes_entry
val merge_universe_context : evar_map -> UState.t -> evar_map
val set_universe_context : evar_map -> UState.t -> evar_map
diff --git a/engine/proofview.ml b/engine/proofview.ml
index d4ad53ff5f..a725444e81 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -223,9 +223,9 @@ module Proof = Logical
type +'a tactic = 'a Proof.t
(** Applies a tactic to the current proofview. *)
-let apply env t sp =
+let apply ~name ~poly env t sp =
let open Logic_monad in
- let ans = Proof.repr (Proof.run t false (sp,env)) in
+ let ans = Proof.repr (Proof.run t P.{trace=false; name; poly} (sp,env)) in
let ans = Logic_monad.NonLogical.run ans in
match ans with
| Nil (e, info) -> iraise (TacticFailure e, info)
@@ -993,7 +993,10 @@ let tclTIME s t =
tclOR (tclUNIT x) (fun e -> aux (n+1) (k e))
in aux 0 t
-
+let tclProofInfo =
+ let open Proof in
+ Logical.current >>= fun P.{name; poly} ->
+ tclUNIT (name, poly)
(** {7 Unsafe primitives} *)
@@ -1275,7 +1278,8 @@ module V82 = struct
let of_tactic t gls =
try
let init = { shelf = []; solution = gls.Evd.sigma ; comb = [with_empty_state gls.Evd.it] } in
- let (_,final,_,_) = apply (goal_env gls.Evd.sigma gls.Evd.it) t init in
+ let name, poly = Names.Id.of_string "legacy_pe", false in
+ let (_,final,_,_) = apply ~name ~poly (goal_env gls.Evd.sigma gls.Evd.it) t init in
{ Evd.sigma = final.solution ; it = CList.map drop_state final.comb }
with Logic_monad.TacticFailure e as src ->
let (_, info) = CErrors.push src in
diff --git a/engine/proofview.mli b/engine/proofview.mli
index 286703c0dc..680a93f0cc 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -156,10 +156,15 @@ type +'a tactic
tactic has given up. In case of multiple success the first one is
selected. If there is no success, fails with
{!Logic_monad.TacticFailure}*)
-val apply : Environ.env -> 'a tactic -> proofview -> 'a
- * proofview
- * (bool*Evar.t list*Evar.t list)
- * Proofview_monad.Info.tree
+val apply
+ : name:Names.Id.t
+ -> poly:bool
+ -> Environ.env
+ -> 'a tactic
+ -> proofview
+ -> 'a * proofview
+ * (bool*Evar.t list*Evar.t list)
+ * Proofview_monad.Info.tree
(** {7 Monadic primitives} *)
@@ -407,6 +412,10 @@ val tclTIMEOUT : int -> 'a tactic -> 'a tactic
identifying annotation if present *)
val tclTIME : string option -> 'a tactic -> 'a tactic
+(** Internal, don't use. *)
+val tclProofInfo : (Names.Id.t * bool) tactic
+[@@ocaml.deprecated "internal, don't use"]
+
(** {7 Unsafe primitives} *)
(** The primitives in the [Unsafe] module should be avoided as much as
diff --git a/engine/proofview_monad.ml b/engine/proofview_monad.ml
index 69341d97df..80eb9d0124 100644
--- a/engine/proofview_monad.ml
+++ b/engine/proofview_monad.ml
@@ -177,7 +177,7 @@ module P = struct
type s = proofview * Environ.env
(** Recording info trace (true) or not. *)
- type e = bool
+ type e = { trace: bool; name : Names.Id.t; poly : bool }
(** Status (safe/unsafe) * shelved goals * given up *)
type w = bool * goal list
@@ -254,13 +254,16 @@ end
(** Lens and utilies pertaining to the info trace *)
module InfoL = struct
- let recording = Logical.current
+ let recording = Logical.(map (fun {P.trace} -> trace) current)
let if_recording t =
let open Logical in
recording >>= fun r ->
if r then t else return ()
- let record_trace t = Logical.local true t
+ let record_trace t =
+ Logical.(
+ current >>= fun s ->
+ local {s with P.trace = true} t)
let raw_update = Logical.update
let update f = if_recording (raw_update f)
diff --git a/engine/proofview_monad.mli b/engine/proofview_monad.mli
index a08cab3bf6..3437b6ce77 100644
--- a/engine/proofview_monad.mli
+++ b/engine/proofview_monad.mli
@@ -98,7 +98,7 @@ module P : sig
val wprod : w -> w -> w
(** Recording info trace (true) or not. *)
- type e = bool
+ type e = { trace: bool; name : Names.Id.t; poly : bool }
type u = Info.state
diff --git a/engine/termops.ml b/engine/termops.ml
index 579100ad4c..2f766afaa6 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -1417,11 +1417,9 @@ let prod_applist_assum sigma n c l =
| _ -> anomaly (Pp.str "Not enough prod/let's.") in
app n [] c l
-(* Combinators on judgments *)
-
-let on_judgment f j = { uj_val = f j.uj_val; uj_type = f j.uj_type }
-let on_judgment_value f j = { j with uj_val = f j.uj_val }
-let on_judgment_type f j = { j with uj_type = f j.uj_type }
+let on_judgment = Environ.on_judgment
+let on_judgment_value = Environ.on_judgment_value
+let on_judgment_type = Environ.on_judgment_type
(* Cut a context ctx in 2 parts (ctx1,ctx2) with ctx1 containing k non let-in
variables skips let-in's; let-in's in the middle are put in ctx2 *)
diff --git a/engine/termops.mli b/engine/termops.mli
index 61a6ec1cd6..dea59e9efc 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -295,8 +295,11 @@ val reference_of_level : Evd.evar_map -> Univ.Level.t -> Libnames.qualid option
(** Combinators on judgments *)
val on_judgment : ('a -> 'b) -> ('a, 'a) punsafe_judgment -> ('b, 'b) punsafe_judgment
+[@@ocaml.deprecated "Use [Environ.on_judgment]."]
val on_judgment_value : ('c -> 'c) -> ('c, 't) punsafe_judgment -> ('c, 't) punsafe_judgment
+[@@ocaml.deprecated "Use [Environ.on_judgment_value]."]
val on_judgment_type : ('t -> 't) -> ('c, 't) punsafe_judgment -> ('c, 't) punsafe_judgment
+[@@ocaml.deprecated "Use [Environ.on_judgment_type]."]
(** {5 Debug pretty-printers} *)
diff --git a/engine/uState.ml b/engine/uState.ml
index 430a3a2fd9..77d1896683 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -100,24 +100,16 @@ let constraints ctx = snd ctx.uctx_local
let context ctx = ContextSet.to_context ctx.uctx_local
-let const_univ_entry ~poly uctx =
+let univ_entry ~poly uctx =
let open Entries in
if poly then
let (binders, _) = uctx.uctx_names in
let uctx = context uctx in
let nas = UnivNames.compute_instance_binders (UContext.instance uctx) binders in
- Polymorphic_const_entry (nas, uctx)
- else Monomorphic_const_entry (context_set uctx)
+ Polymorphic_entry (nas, uctx)
+ else Monomorphic_entry (context_set uctx)
-(* does not support cumulativity since you need more info *)
-let ind_univ_entry ~poly uctx =
- let open Entries in
- if poly then
- let (binders, _) = uctx.uctx_names in
- let uctx = context uctx in
- let nas = UnivNames.compute_instance_binders (UContext.instance uctx) binders in
- Polymorphic_ind_entry (nas, uctx)
- else Monomorphic_ind_entry (context_set uctx)
+let const_univ_entry = univ_entry
let of_context_set ctx = { empty with uctx_local = ctx }
@@ -422,10 +414,10 @@ let check_univ_decl ~poly uctx decl =
let (binders, _) = uctx.uctx_names in
let uctx = universe_context ~names ~extensible uctx in
let nas = UnivNames.compute_instance_binders (UContext.instance uctx) binders in
- Entries.Polymorphic_const_entry (nas, uctx)
+ Entries.Polymorphic_entry (nas, uctx)
else
let () = check_universe_context_set ~names ~extensible uctx in
- Entries.Monomorphic_const_entry uctx.uctx_local
+ Entries.Monomorphic_entry uctx.uctx_local
in
if not decl.univdecl_extensible_constraints then
check_implication uctx
@@ -458,8 +450,8 @@ let restrict ctx vars =
let demote_seff_univs entry uctx =
let open Entries in
match entry.const_entry_universes with
- | Polymorphic_const_entry _ -> uctx
- | Monomorphic_const_entry (univs, _) ->
+ | Polymorphic_entry _ -> uctx
+ | Monomorphic_entry (univs, _) ->
let seff = LSet.union uctx.uctx_seff_univs univs in
{ uctx with uctx_seff_univs = seff }
diff --git a/engine/uState.mli b/engine/uState.mli
index 5170184ef4..a358813825 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -64,12 +64,11 @@ val constraints : t -> Univ.Constraint.t
val context : t -> Univ.UContext.t
(** Shorthand for {!context_set} with {!Context_set.to_context}. *)
-val const_univ_entry : poly:bool -> t -> Entries.constant_universes_entry
+val univ_entry : poly:bool -> t -> Entries.universes_entry
(** Pick from {!context} or {!context_set} based on [poly]. *)
-val ind_univ_entry : poly:bool -> t -> Entries.inductive_universes
-(** Pick from {!context} or {!context_set} based on [poly].
- Cannot create cumulative entries. *)
+val const_univ_entry : poly:bool -> t -> Entries.universes_entry
+[@@ocaml.deprecated "Use [univ_entry]."]
(** {5 Constraints handling} *)
@@ -177,7 +176,7 @@ val default_univ_decl : universe_decl
When polymorphic, the universes corresponding to
[decl.univdecl_instance] come first in the order defined by that
list. *)
-val check_univ_decl : poly:bool -> t -> universe_decl -> Entries.constant_universes_entry
+val check_univ_decl : poly:bool -> t -> universe_decl -> Entries.universes_entry
val check_mono_univ_decl : t -> universe_decl -> Univ.ContextSet.t
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 02:16:13 +0000