aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--pretyping/evarutil.ml22
-rw-r--r--pretyping/evarutil.mli10
-rw-r--r--pretyping/evd.ml29
-rw-r--r--pretyping/evd.mli3
-rw-r--r--pretyping/typeclasses.ml5
-rw-r--r--pretyping/typeclasses.mli3
-rw-r--r--proofs/proof_global.ml4
-rw-r--r--tactics/rewrite.ml14
-rw-r--r--theories/Numbers/NatInt/NZGcd.v4
-rw-r--r--theories/Structures/GenericMinMax.v2
-rw-r--r--toplevel/command.ml8
11 files changed, 57 insertions, 47 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index a4eae5fdff..128a7e55c4 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -355,47 +355,41 @@ let new_pure_evar_full evd evi =
let evd = Evd.add evd evk evi in
(evd, evk)
-let new_pure_evar evd sign ?(src=default_source) ?filter ?candidates typ =
+let new_pure_evar evd sign ?(src=default_source) ?filter ?candidates ?store typ =
let newevk = new_untyped_evar() in
- let evd = evar_declare sign newevk typ ~src ?filter ?candidates evd in
+ let evd = evar_declare sign newevk typ ~src ?filter ?candidates ?store evd in
(evd,newevk)
-let new_evar_instance sign evd typ ?src ?filter ?candidates instance =
+let new_evar_instance sign evd typ ?src ?filter ?candidates ?store instance =
assert (not !Flags.debug ||
List.distinct (ids_of_named_context (named_context_of_val sign)));
- let evd,newevk = new_pure_evar evd sign ?src ?filter ?candidates typ in
+ let evd,newevk = new_pure_evar evd sign ?src ?filter ?candidates ?store typ in
(evd,mkEvar (newevk,Array.of_list instance))
(* [new_evar] declares a new existential in an env env with type typ *)
(* Converting the env into the sign of the evar to define *)
-let new_evar evd env ?src ?filter ?candidates typ =
+let new_evar evd env ?src ?filter ?candidates ?store typ =
let sign,typ',instance,subst,vsubst = push_rel_context_to_named_context env typ in
let candidates = Option.map (List.map (subst2 subst vsubst)) candidates in
let instance =
match filter with
| None -> instance
| Some filter -> Filter.filter_list filter instance in
- new_evar_instance sign evd typ' ?src ?filter ?candidates instance
+ new_evar_instance sign evd typ' ?src ?filter ?candidates ?store instance
let new_type_evar ?src ?filter rigid evd env =
let evd', s = new_sort_variable rigid evd in
let evd', e = new_evar evd' env ?src ?filter (mkSort s) in
evd', (e, s)
- (* The same using side-effect *)
-let e_new_evar evdref env ?(src=(Loc.ghost,Evar_kinds.InternalHole)) ?filter ?candidates ty =
- let (evd',ev) = new_evar !evdref env ~src:src ?filter ?candidates ty in
- evdref := evd';
- ev
-
let e_new_type_evar evdref ?src ?filter rigid env =
let evd', c = new_type_evar ?src ?filter rigid !evdref env in
evdref := evd';
c
(* The same using side-effect *)
-let e_new_evar evdref env ?(src=default_source) ?filter ?candidates ty =
- let (evd',ev) = new_evar !evdref env ~src:src ?filter ?candidates ty in
+let e_new_evar evdref env ?(src=default_source) ?filter ?candidates ?store ty =
+ let (evd',ev) = new_evar !evdref env ~src:src ?filter ?candidates ?store ty in
evdref := evd';
ev
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index d197ad2efe..7715691b0c 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -23,18 +23,18 @@ val mk_new_meta : unit -> constr
(** {6 Creating a fresh evar given their type and context} *)
val new_evar :
evar_map -> env -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
- ?candidates:constr list -> types -> evar_map * constr
+ ?candidates:constr list -> ?store:Store.t -> types -> evar_map * constr
val new_pure_evar :
evar_map -> named_context_val -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
- ?candidates:constr list -> types -> evar_map * evar
+ ?candidates:constr list -> ?store:Store.t -> types -> evar_map * evar
val new_pure_evar_full : evar_map -> evar_info -> evar_map * evar
(** the same with side-effects *)
val e_new_evar :
evar_map ref -> env -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
- ?candidates:constr list -> types -> constr
+ ?candidates:constr list -> ?store:Store.t -> types -> constr
(** Create a new Type existential variable, as we keep track of
them during type-checking and unification. *)
@@ -57,7 +57,9 @@ val e_new_global : evar_map ref -> Globnames.global_reference -> constr
of [inst] are typed in the occurrence context and their type (seen
as a telescope) is [sign] *)
val new_evar_instance :
- named_context_val -> evar_map -> types -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> ?candidates:constr list -> constr list -> evar_map * constr
+ named_context_val -> evar_map -> types ->
+ ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> ?candidates:constr list ->
+ ?store:Store.t -> constr list -> evar_map * constr
val make_pure_subst : evar_info -> constr array -> (Id.t * constr) list
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 1bd995d5d1..5a9281c890 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -295,7 +295,6 @@ let is_empty_evar_universe_context ctx =
let union_evar_universe_context ctx ctx' =
if ctx == ctx' then ctx
- else if is_empty_evar_universe_context ctx then ctx'
else if is_empty_evar_universe_context ctx' then ctx
else
let local =
@@ -331,7 +330,7 @@ let diff_evar_universe_context ctx' ctx =
Univ.LSet.diff ctx'.uctx_univ_algebraic ctx.uctx_univ_algebraic;
uctx_univ_template =
Univ.LSet.diff ctx'.uctx_univ_template ctx.uctx_univ_template;
- uctx_universes = Univ.empty_universes;
+ uctx_universes = ctx.uctx_initial_universes;
uctx_initial_universes = ctx.uctx_initial_universes }
(* let diff_evar_universe_context_key = Profile.declare_profile "diff_evar_universe_context";; *)
@@ -354,7 +353,7 @@ let instantiate_variable l b v =
exception UniversesDiffer
-let process_universe_constraints univs vars alg templ local cstrs =
+let process_universe_constraints univs vars alg templ cstrs =
let vars = ref vars in
let normalize = Universes.normalize_universe_opt_subst vars in
let rec unify_universes fo l d r local =
@@ -370,10 +369,11 @@ let process_universe_constraints univs vars alg templ local cstrs =
if Univ.check_leq univs l r then
(** Keep Prop/Set <= var around if var might be instantiated by prop or set
later. *)
- if Univ.is_small_univ l && not (Univ.is_small_univ r) then
- match Univ.Universe.level l, Univ.Universe.level r with
- | Some l, Some r -> Univ.Constraint.add (l,Univ.Le,r) local
- | _, _ -> local
+ if Univ.is_small_univ l then
+ match Univ.Universe.level r with
+ | Some r when Univ.LMap.mem r !vars ->
+ Univ.Constraint.add (Option.get (Univ.Universe.level l),Univ.Le,r) local
+ | _ -> local
else local
else
match Univ.Universe.level r with
@@ -423,7 +423,7 @@ let process_universe_constraints univs vars alg templ local cstrs =
in
let local =
Univ.UniverseConstraints.fold (fun (l,d,r) local -> unify_universes false l d r local)
- cstrs local
+ cstrs Univ.Constraint.empty
in
!vars, local
@@ -440,7 +440,7 @@ let add_constraints_context ctx cstrs =
let vars, local' =
process_universe_constraints ctx.uctx_universes
ctx.uctx_univ_variables ctx.uctx_univ_algebraic
- ctx.uctx_univ_template local cstrs'
+ ctx.uctx_univ_template cstrs'
in
{ ctx with uctx_local = (univs, Univ.Constraint.union local local');
uctx_univ_variables = vars;
@@ -454,7 +454,7 @@ let add_universe_constraints_context ctx cstrs =
let vars, local' =
process_universe_constraints ctx.uctx_universes
ctx.uctx_univ_variables ctx.uctx_univ_algebraic
- ctx.uctx_univ_template local cstrs
+ ctx.uctx_univ_template cstrs
in
{ ctx with uctx_local = (univs, Univ.Constraint.union local local');
uctx_univ_variables = vars;
@@ -769,7 +769,8 @@ let define evk body evd =
in
{ evd with defn_evars; undf_evars; last_mods; }
-let evar_declare hyps evk ty ?(src=(Loc.ghost,Evar_kinds.InternalHole)) ?(filter = Filter.identity) ?candidates evd =
+let evar_declare hyps evk ty ?(src=(Loc.ghost,Evar_kinds.InternalHole))
+ ?(filter=Filter.identity) ?candidates ?(store=Store.empty) evd =
let () = match Filter.repr filter with
| None -> ()
| Some filter ->
@@ -782,7 +783,7 @@ let evar_declare hyps evk ty ?(src=(Loc.ghost,Evar_kinds.InternalHole)) ?(filter
evar_filter = filter;
evar_source = src;
evar_candidates = candidates;
- evar_extra = Store.empty; }
+ evar_extra = store; }
in
{ evd with undf_evars = EvMap.add evk evar_info evd.undf_evars; }
@@ -1128,9 +1129,9 @@ let set_leq_sort evd s1 s2 =
| Prop c, Prop c' ->
if c == Null && c' == Pos then evd
else (raise (Univ.UniverseInconsistency (Univ.Le, u1, u2, [])))
- | _, _ ->
+ | _, _ ->
add_universe_constraints evd (Univ.UniverseConstraints.singleton (u1,Univ.ULe,u2))
-
+
let check_eq evd s s' =
Univ.check_eq evd.universes.uctx_universes s s'
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index fb348ae226..49a91f524e 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -234,7 +234,8 @@ val evars_reset_evd : ?with_conv_pbs:bool -> ?with_univs:bool ->
val evar_declare :
named_context_val -> evar -> types -> ?src:Loc.t * Evar_kinds.t ->
- ?filter:Filter.t -> ?candidates:constr list -> evar_map -> evar_map
+ ?filter:Filter.t -> ?candidates:constr list -> ?store:Store.t ->
+ evar_map -> evar_map
(** Convenience function. Just a wrapper around {!add}. *)
val evar_source : existential_key -> evar_map -> Evar_kinds.t located
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index ada497ece7..8364387783 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -507,6 +507,9 @@ let is_implicit_arg = function
let resolvable = Store.field ()
+let set_resolvable s b =
+ Store.set s resolvable b
+
let is_resolvable evi =
assert (match evi.evar_body with Evar_empty -> true | _ -> false);
Option.default true (Store.get evi.evar_extra resolvable)
@@ -540,7 +543,7 @@ let mark_resolvability filter b sigma =
Evd.raw_map_undefined map sigma
let mark_unresolvables ?(filter=all_evars) sigma = mark_resolvability filter false sigma
-let mark_resolvables sigma = mark_resolvability all_evars true sigma
+let mark_resolvables ?(filter=all_evars) sigma = mark_resolvability filter true sigma
let has_typeclasses filter evd =
let check ev evi =
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index a8ce9ca7c9..ebc6be45fb 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -92,11 +92,12 @@ val no_goals_or_obligations : evar_filter
(** Resolvability.
Only undefined evars can be marked or checked for resolvability. *)
+val set_resolvable : Evd.Store.t -> bool -> Evd.Store.t
val is_resolvable : evar_info -> bool
val mark_unresolvable : evar_info -> evar_info
val mark_unresolvables : ?filter:evar_filter -> evar_map -> evar_map
+val mark_resolvables : ?filter:evar_filter -> evar_map -> evar_map
val mark_resolvable : evar_info -> evar_info
-val mark_resolvables : evar_map -> evar_map
val is_class_evar : evar_map -> evar_info -> bool
val resolve_typeclasses : ?filter:evar_filter -> ?split:bool -> ?fail:bool ->
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index e49a57af39..5cb677d1c6 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -226,7 +226,7 @@ let start_proof id str goals terminator =
let initial_state = {
pid = id;
terminator = Ephemeron.create terminator;
- proof = Proof.start Evd.empty goals;
+ proof = Proof.start (Evd.from_env (Global.env ())) goals;
endline_tactic = None;
section_vars = None;
strength = str;
@@ -237,7 +237,7 @@ let start_dependent_proof id str goals terminator =
let initial_state = {
pid = id;
terminator = Ephemeron.create terminator;
- proof = Proof.dependent_start Evd.empty goals;
+ proof = Proof.dependent_start (Evd.from_env (Global.env ())) goals;
endline_tactic = None;
section_vars = None;
strength = str;
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index dc9cc471c2..9dd6c941ee 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -120,8 +120,10 @@ let goalevars evars = fst evars
let cstrevars evars = snd evars
let new_cstr_evar (evd,cstrs) env t =
- let evd', t = Evarutil.new_evar evd env t in
- (evd', Evar.Set.add (fst (destEvar t)) cstrs), t
+ let s = Typeclasses.set_resolvable Evd.Store.empty false in
+ let evd', t = Evarutil.new_evar ~store:s evd env t in
+ let ev, _ = destEvar t in
+ (evd', Evar.Set.add ev cstrs), t
(** Building or looking up instances. *)
let e_new_cstr_evar evars env t =
@@ -602,6 +604,9 @@ let shrink_evd sigma ext =
let no_constraints cstrs =
fun ev _ -> not (Evar.Set.mem ev cstrs)
+let all_constraints cstrs =
+ fun ev _ -> Evar.Set.mem ev cstrs
+
let poly_inverse sort =
if sort then PropGlobal.inverse else TypeGlobal.inverse
@@ -641,7 +646,7 @@ let unify_eqn env (sigma, cstrs) hypinfo by t =
(* env'.evd, prf, c1, c2, car, rel) *)
else raise Reduction.NotConvertible
in
- let evars = evd', Evar.Set.empty in
+ let evars = evd', cstrs in
let evd, res =
if l2r then evars, (prf, (car, rel, c1, c2))
else
@@ -1332,7 +1337,8 @@ let apply_strategy (s : strategy) env avoid concl (prop, cstr) evars =
Some (Some (res.rew_prf, res.rew_evars, res.rew_car, res.rew_from, res.rew_to))
let solve_constraints env (evars,cstrs) =
- Typeclasses.resolve_typeclasses env ~split:false ~fail:true evars
+ Typeclasses.resolve_typeclasses env ~split:false ~fail:true
+ (Typeclasses.mark_resolvables ~filter:(all_constraints cstrs) evars)
let nf_zeta =
Reductionops.clos_norm_flags (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA])
diff --git a/theories/Numbers/NatInt/NZGcd.v b/theories/Numbers/NatInt/NZGcd.v
index d7e598fb4e..e4e1fe3b03 100644
--- a/theories/Numbers/NatInt/NZGcd.v
+++ b/theories/Numbers/NatInt/NZGcd.v
@@ -107,8 +107,8 @@ Proof.
now rewrite Hr, Hq, mul_assoc.
Qed.
-Instance divide_reflexive : Reflexive divide := divide_refl.
-Instance divide_transitive : Transitive divide := divide_trans.
+Instance divide_reflexive : Reflexive divide | 5 := divide_refl.
+Instance divide_transitive : Transitive divide | 5 := divide_trans.
(** Due to sign, no general antisymmetry result *)
diff --git a/theories/Structures/GenericMinMax.v b/theories/Structures/GenericMinMax.v
index a0ee4caaa5..ac52d1bbb9 100644
--- a/theories/Structures/GenericMinMax.v
+++ b/theories/Structures/GenericMinMax.v
@@ -110,7 +110,7 @@ Proof.
intros x x' Hx y y' Hy.
assert (H1 := max_spec x y). assert (H2 := max_spec x' y').
set (m := max x y) in *; set (m' := max x' y') in *; clearbody m m'.
- rewrite <- Hx, <- Hy in *.
+ rewrite <- Hx, <- Hy in *.
destruct (lt_total x y); intuition order.
Qed.
diff --git a/toplevel/command.ml b/toplevel/command.ml
index f4171da1b3..bc6f88e691 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -245,7 +245,7 @@ let declare_assumptions idl is_coe k c imps impl_is_on nl =
let do_assumptions kind nl l =
let env = Global.env () in
- let evdref = ref Evd.empty in
+ let evdref = ref (Evd.from_env env) in
let _,l = List.fold_map (fun env (is_coe,(idl,c)) ->
let (t,ctx),imps = interp_assumption evdref env [] c in
let env =
@@ -752,8 +752,8 @@ let nf_evar_context sigma ctx =
let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
Coqlib.check_required_library ["Coq";"Program";"Wf"];
- let evdref = ref Evd.empty in
let env = Global.env() in
+ let evdref = ref (Evd.from_env env) in
let _, ((env', binders_rel), impls) = interp_context_evars evdref env bl in
let len = List.length binders_rel in
let top_env = push_rel_context binders_rel env in
@@ -892,7 +892,7 @@ let interp_recursive isfix fixl notations =
let fixnames = List.map (fun fix -> fix.fix_name) fixl in
(* Interp arities allowing for unresolved types *)
- let evdref = ref Evd.empty in
+ let evdref = ref (Evd.from_env env) in
let fixctxs, fiximppairs, fixannots =
List.split3 (List.map (interp_fix_context evdref env isfix) fixl) in
let fixctximpenvs, fixctximps = List.split fiximppairs in
@@ -978,8 +978,10 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) indexe
let env = Global.env() in
let indexes = search_guard Loc.ghost env indexes fixdecls in
let fiximps = List.map (fun (n,r,p) -> r) fiximps in
+ let vars = Universes.universes_of_constr (mkFix ((indexes,0),fixdecls)) in
let fixdecls =
List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in
+ let ctx = Universes.restrict_universe_context ctx vars in
let fixdecls = List.map Term_typing.mk_pure_proof fixdecls in
let ctx = Univ.ContextSet.to_context ctx in
ignore (List.map4 (declare_fix (local, poly, Fixpoint) ctx)
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 02:58:05 +0000