aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--pretyping/cases.ml4
-rw-r--r--pretyping/evarsolve.ml85
-rw-r--r--pretyping/evarsolve.mli5
-rw-r--r--pretyping/evarutil.ml24
-rw-r--r--pretyping/evarutil.mli7
-rw-r--r--pretyping/evd.ml43
-rw-r--r--pretyping/evd.mli14
-rw-r--r--pretyping/pretyping.ml60
-rw-r--r--pretyping/typing.ml2
-rw-r--r--pretyping/unification.ml2
-rw-r--r--theories/FSets/FMapPositive.v2
-rw-r--r--toplevel/record.ml2
12 files changed, 102 insertions, 148 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 94ec09db2..b5aeeae3a 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1559,7 +1559,7 @@ let abstract_tycon loc env evdref subst _tycon extenv t =
map_constr_with_full_binders push_binder aux x t
| Evar ev ->
let ty = get_type_of env sigma t in
- let ty = Evarutil.evd_comb1 (refresh_universes false) evdref ty in
+ let ty = Evarutil.evd_comb1 (refresh_universes false env) evdref ty in
let inst =
List.map_i
(fun i _ ->
@@ -1577,7 +1577,7 @@ let abstract_tycon loc env evdref subst _tycon extenv t =
let vl = List.map pi1 good in
let ty =
let ty = get_type_of env !evdref t in
- Evarutil.evd_comb1 (refresh_universes false) evdref ty
+ Evarutil.evd_comb1 (refresh_universes false env) evdref ty
in
let ty = lift (-k) (aux x ty) in
let depvl = free_rels ty in
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 66d65bab6..26e96af48 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -26,23 +26,72 @@ let normalize_evar evd ev =
| Evar (evk,args) -> (evk,args)
| _ -> assert false
-let refresh_universes ?(all=false) ?(template=false) ?(with_globals=false) dir evd t =
+let get_polymorphic_positions f =
+ let open Declarations in
+ match kind_of_term f with
+ | Ind (ind, u) | Construct ((ind, _), u) ->
+ let mib,oib = Global.lookup_inductive ind in
+ (match oib.mind_arity with
+ | RegularArity _ -> assert false
+ | TemplateArity templ -> templ.template_param_levels)
+ | Const (cst, u) ->
+ let cb = Global.lookup_constant cst in
+ (match cb.const_type with
+ | RegularArity _ -> assert false
+ | TemplateArity (_, templ) ->
+ templ.template_param_levels)
+ | _ -> assert false
+
+let refresh_universes dir env evd t =
let evdref = ref evd in
let modified = ref false in
- let rec refresh dir t = match kind_of_term t with
- | Sort (Type u as s) when Univ.universe_level u = None
- || (with_globals && Evd.is_sort_variable evd s = None) ->
- (modified := true;
- (* s' will appear in the term, it can't be algebraic *)
- let s' = evd_comb0 (new_sort_variable ~template Evd.univ_flexible) evdref in
- evdref :=
- (if dir then set_leq_sort !evdref s' s else
- set_leq_sort !evdref s s');
- mkSort s')
- | Prod (na,u,v) -> mkProd (na,(if all then refresh true u else u),refresh dir v)
- | _ -> t in
- let t' = refresh dir t in
- if !modified then !evdref, t' else evd, t
+ let rec refresh dir t =
+ match kind_of_term t with
+ | Sort (Type u as s) when
+ (match Univ.universe_level u with
+ | None -> true
+ | Some l -> Option.is_empty (Evd.is_sort_variable evd s)) ->
+ (* s' will appear in the term, it can't be algebraic *)
+ let s' = evd_comb0 (new_sort_variable Evd.univ_flexible) evdref in
+ let evd =
+ if dir then set_leq_sort !evdref s' s
+ else set_leq_sort !evdref s s'
+ in
+ modified := true; evdref := evd; mkSort s'
+ | Prod (na,u,v) ->
+ mkProd (na,u,refresh dir v)
+ | _ -> t
+ (** Refresh the types of evars under template polymorphic references *)
+ and refresh_term_evars onevars t =
+ match kind_of_term t with
+ | App (f, args) when is_template_polymorphic env f ->
+ let pos = get_polymorphic_positions f in
+ refresh_polymorphic_positions args pos
+ | Evar (ev, a) when onevars ->
+ let evi = Evd.find !evdref ev in
+ let ty' = refresh true evi.evar_concl in
+ if !modified then
+ evdref := Evd.add !evdref ev {evi with evar_concl = ty'}
+ else ()
+ | _ -> iter_constr (refresh_term_evars onevars) t
+ and refresh_polymorphic_positions args pos =
+ let rec aux i = function
+ | Some l :: ls ->
+ if i < Array.length args then
+ ignore(refresh_term_evars true args.(i));
+ aux (succ i) ls
+ | None :: ls ->
+ if i < Array.length args then
+ ignore(refresh_term_evars false args.(i));
+ aux (succ i) ls
+ | [] -> ()
+ in aux 0 pos
+ in
+ let t' =
+ if isArity t then refresh dir t
+ else (refresh_term_evars false t; t)
+ in
+ if !modified then !evdref, t' else !evdref, t
(************************)
(* Unification results *)
@@ -504,7 +553,7 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
let id = next_name_away na avoid in
let evd,t_in_sign =
let s = Retyping.get_sort_of env evd t_in_env in
- let evd,ty_t_in_sign = refresh_universes false evd (mkSort s) in
+ let evd,ty_t_in_sign = refresh_universes false env evd (mkSort s) in
define_evar_from_virtual_equation define_fun env evd t_in_env
ty_t_in_sign sign filter inst_in_env in
let evd,b_in_sign = match b with
@@ -523,7 +572,7 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
in
let evd,ev2ty_in_sign =
let s = Retyping.get_sort_of env evd ty_in_env in
- let evd,ty_t_in_sign = refresh_universes false evd (mkSort s) in
+ let evd,ty_t_in_sign = refresh_universes false env evd (mkSort s) in
define_evar_from_virtual_equation define_fun env evd ty_in_env
ty_t_in_sign sign2 filter2 inst2_in_env in
let evd,ev2_in_sign =
@@ -1387,7 +1436,7 @@ and evar_define conv_algo ?(choose=false) ?(dir=false) env evd pbty (evk,argsv a
(* so we recheck acyclicity *)
if occur_evar evk body then raise (OccurCheckIn (evd',body));
(* needed only if an inferred type *)
- let evd', body = refresh_universes dir evd' body in
+ let evd', body = refresh_universes dir env evd' body in
(* Cannot strictly type instantiations since the unification algorithm
* does not unify applications from left to right.
* e.g problem f x == g y yields x==y and f==g (in that order)
diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli
index 23ed6a2ef..988938272 100644
--- a/pretyping/evarsolve.mli
+++ b/pretyping/evarsolve.mli
@@ -34,9 +34,8 @@ type conv_fun_bool =
val evar_define : conv_fun -> ?choose:bool -> ?dir:bool -> env -> evar_map ->
bool option -> existential -> constr -> evar_map
-val refresh_universes : ?all:bool (* Include domains of products *) ->
- ?template:bool -> (* Generate template fresh universe variables, to be instantiated eagerly *)
- ?with_globals:bool -> bool -> evar_map -> types -> evar_map * types
+val refresh_universes : bool (* direction: true for levels lower than the existing levels *) ->
+ env -> evar_map -> types -> evar_map * types
val solve_refl : ?can_drop:bool -> conv_fun_bool -> env -> evar_map ->
bool option -> existential_key -> constr array -> constr array -> evar_map
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index a842134df..7fa6f46fb 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -816,27 +816,3 @@ let lift_tycon n = Option.map (lift n)
let pr_tycon env = function
None -> str "None"
| Some t -> Termops.print_constr_env env t
-
-open Declarations
-
-let get_template_constructor_type evdref (ind, i) n =
- let mib,oib = Global.lookup_inductive ind in
- let ar =
- match oib.mind_arity with
- | RegularArity _ -> assert false
- | TemplateArity templ -> templ
- in
- let ty = oib.mind_user_lc.(pred i) in
- let subst = Inductive.ind_subst (fst ind) mib Univ.Instance.empty in
- let ty = substl subst ty in
- ar.template_param_levels, ty
-
-let get_template_inductive_type evdref ind n =
- let mib,oib = Global.lookup_inductive ind in
- let ar =
- match oib.mind_arity with
- | RegularArity _ -> assert false
- | TemplateArity templ -> templ
- in
- let ctx = oib.mind_arity_ctxt in
- ar.template_param_levels, mkArity(ctx, Type ar.template_level)
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 55171eb4c..c0708aa85 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -221,10 +221,3 @@ val generalize_evar_over_rels : evar_map -> existential -> types * constr list
val evd_comb0 : (evar_map -> evar_map * 'a) -> evar_map ref -> 'a
val evd_comb1 : (evar_map -> 'b -> evar_map * 'a) -> evar_map ref -> 'b -> 'a
val evd_comb2 : (evar_map -> 'b -> 'c -> evar_map * 'a) -> evar_map ref -> 'b -> 'c -> 'a
-
-(* val get_template_constructor_type : evar_map ref -> constructor -> int -> types *)
-val get_template_constructor_type : evar_map ref -> constructor -> int ->
- (Univ.universe_level option list * types)
-
-val get_template_inductive_type : evar_map ref -> inductive -> int ->
- (Univ.universe_level option list * types)
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index d5aaf9df3..09e34c6aa 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -288,7 +288,6 @@ type evar_universe_context =
uctx_univ_variables : Universes.universe_opt_subst;
(** The local universes that are unification variables *)
uctx_univ_algebraic : Univ.universe_set;
- uctx_univ_template : Univ.universe_set;
(** The subset of unification variables that
can be instantiated with algebraic universes as they appear in types
and universe instances only. *)
@@ -301,7 +300,6 @@ let empty_evar_universe_context =
uctx_local = Univ.ContextSet.empty;
uctx_univ_variables = Univ.LMap.empty;
uctx_univ_algebraic = Univ.LSet.empty;
- uctx_univ_template = Univ.LSet.empty;
uctx_universes = Univ.initial_universes;
uctx_initial_universes = Univ.initial_universes }
@@ -332,8 +330,6 @@ let union_evar_universe_context ctx ctx' =
Univ.LMap.subst_union ctx.uctx_univ_variables ctx'.uctx_univ_variables;
uctx_univ_algebraic =
Univ.LSet.union ctx.uctx_univ_algebraic ctx'.uctx_univ_algebraic;
- uctx_univ_template =
- Univ.LSet.union ctx.uctx_univ_template ctx'.uctx_univ_template;
uctx_initial_universes = ctx.uctx_initial_universes;
uctx_universes =
if local == ctx.uctx_local then ctx.uctx_universes
@@ -356,8 +352,6 @@ let diff_evar_universe_context ctx' ctx =
Univ.LMap.diff ctx'.uctx_univ_variables ctx.uctx_univ_variables;
uctx_univ_algebraic =
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 = ctx.uctx_initial_universes;
uctx_initial_universes = ctx.uctx_initial_universes }
@@ -381,7 +375,7 @@ let instantiate_variable l b v =
exception UniversesDiffer
-let process_universe_constraints univs vars alg templ cstrs =
+let process_universe_constraints univs vars alg cstrs =
let vars = ref vars in
let normalize = Universes.normalize_universe_opt_subst vars in
let rec unify_universes fo l d r local =
@@ -414,8 +408,6 @@ let process_universe_constraints univs vars alg templ cstrs =
Univ.enforce_eq (Univ.Universe.make l) r local
else raise (Univ.UniverseInconsistency (Univ.Le, Univ.Universe.make l, r, None)))
levels local
- else if Univ.LSet.mem rl templ && Univ.Universe.is_level l then
- unify_universes fo l Universes.UEq r local
else
Univ.enforce_leq l r local
else if d == Universes.ULub then
@@ -468,7 +460,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 cstrs'
+ cstrs'
in
{ ctx with uctx_local = (univs, Univ.Constraint.union local local');
uctx_univ_variables = vars;
@@ -482,7 +474,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 cstrs
+ cstrs
in
{ ctx with uctx_local = (univs, Univ.Constraint.union local local');
uctx_univ_variables = vars;
@@ -990,7 +982,7 @@ let merge_universe_subst evd subst =
let with_context_set rigid d (a, ctx) =
(merge_context_set rigid d ctx, a)
-let uctx_new_univ_variable template rigid name
+let uctx_new_univ_variable rigid name
({ uctx_local = ctx; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as uctx) =
let u = Universes.new_univ_level (Global.current_dirpath ()) in
let ctx' = Univ.ContextSet.union ctx (Univ.ContextSet.singleton u) in
@@ -1002,28 +994,24 @@ let uctx_new_univ_variable template rigid name
if b then {uctx with uctx_univ_variables = uvars';
uctx_univ_algebraic = Univ.LSet.add u avars}
else {uctx with uctx_univ_variables = Univ.LMap.add u None uvars} in
- let uctx'' = if template then
- {uctx' with uctx_univ_template = Univ.LSet.add u uctx'.uctx_univ_template}
- else uctx'
- in
let names =
match name with
| Some n -> UNameMap.add n u uctx.uctx_names
| None -> uctx.uctx_names
in
- {uctx'' with uctx_names = names; uctx_local = ctx';
+ {uctx' with uctx_names = names; uctx_local = ctx';
uctx_universes = Univ.add_universe u uctx.uctx_universes}, u
-let new_univ_level_variable ?(template=false) ?name rigid evd =
- let uctx', u = uctx_new_univ_variable template rigid name evd.universes in
+let new_univ_level_variable ?name rigid evd =
+ let uctx', u = uctx_new_univ_variable rigid name evd.universes in
({evd with universes = uctx'}, u)
-let new_univ_variable ?(template=false) ?name rigid evd =
- let uctx', u = uctx_new_univ_variable template rigid name evd.universes in
+let new_univ_variable ?name rigid evd =
+ let uctx', u = uctx_new_univ_variable rigid name evd.universes in
({evd with universes = uctx'}, Univ.Universe.make u)
-let new_sort_variable ?(template=false) ?name rigid d =
- let (d', u) = new_univ_variable ~template rigid ?name d in
+let new_sort_variable ?name rigid d =
+ let (d', u) = new_univ_variable rigid ?name d in
(d', Type u)
let make_flexible_variable evd b u =
@@ -1067,11 +1055,10 @@ let is_sort_variable evd s =
match s with
| Type u ->
(match Univ.universe_level u with
- | Some l ->
+ | Some l as x ->
let uctx = evd.universes in
- if Univ.LSet.mem l (Univ.ContextSet.levels uctx.uctx_local) then
- Some (l, not (Univ.LMap.mem l uctx.uctx_univ_variables))
- else None
+ if Univ.LSet.mem l (Univ.ContextSet.levels uctx.uctx_local) then x
+ else None
| None -> None)
| _ -> None
@@ -1193,7 +1180,6 @@ let refresh_undefined_univ_variables uctx =
let uctx' = {uctx_names = uctx.uctx_names;
uctx_local = ctx';
uctx_univ_variables = vars; uctx_univ_algebraic = alg;
- uctx_univ_template = uctx.uctx_univ_template;
uctx_universes = Univ.initial_universes;
uctx_initial_universes = uctx.uctx_initial_universes } in
uctx', subst
@@ -1218,7 +1204,6 @@ let normalize_evar_universe_context uctx =
uctx_local = us';
uctx_univ_variables = vars';
uctx_univ_algebraic = algs';
- uctx_univ_template = uctx.uctx_univ_template;
uctx_universes = universes;
uctx_initial_universes = uctx.uctx_initial_universes }
in fixpoint uctx'
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 1393a33d3..b6db3c263 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -261,7 +261,6 @@ val drop_side_effects : evar_map -> evar_map
Evar maps also keep track of the universe constraints defined at a given
point. This section defines the relevant manipulation functions. *)
-val is_sort_variable : evar_map -> sorts -> bool
val whd_sort_variable : evar_map -> constr -> constr
val set_leq_sort : evar_map -> sorts -> sorts -> evar_map
val set_eq_sort : evar_map -> sorts -> sorts -> evar_map
@@ -438,16 +437,15 @@ val normalize_evar_universe_context_variables : evar_universe_context ->
val normalize_evar_universe_context : evar_universe_context ->
evar_universe_context
-val new_univ_level_variable : ?template:bool -> ?name:string -> rigid -> evar_map -> evar_map * Univ.universe_level
-val new_univ_variable : ?template:bool -> ?name:string -> rigid -> evar_map -> evar_map * Univ.universe
-val new_sort_variable : ?template:bool -> ?name:string -> rigid -> evar_map -> evar_map * sorts
+val new_univ_level_variable : ?name:string -> rigid -> evar_map -> evar_map * Univ.universe_level
+val new_univ_variable : ?name:string -> rigid -> evar_map -> evar_map * Univ.universe
+val new_sort_variable : ?name:string -> rigid -> evar_map -> evar_map * sorts
val make_flexible_variable : evar_map -> bool -> Univ.universe_level -> evar_map
-val is_sort_variable : evar_map -> sorts -> (Univ.universe_level * bool) option
-(** [is_sort_variable evm s] returns [Some (u, is_rigid)] or [None] if [s] is
- not a sort variable declared in [evm] *)
+val is_sort_variable : evar_map -> sorts -> Univ.universe_level option
+(** [is_sort_variable evm s] returns [Some u] or [None] if [s] is
+ not a local sort variable declared in [evm] *)
val is_flexible_level : evar_map -> Univ.Level.t -> bool
-
val whd_sort_variable : evar_map -> constr -> constr
(* val normalize_universe_level : evar_map -> Univ.universe_level -> Univ.universe_level *)
val normalize_universe : evar_map -> Univ.universe -> Univ.universe
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 6f8b407ae..1520e1a7e 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -527,20 +527,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref lvar t =
inh_conv_coerce_to_tycon loc env evdref j tycon
| GApp (loc,f,args) ->
- let univs, fj =
- match f with
- | GRef (loc, ConstructRef (ind, i as cstr), u')
- when Environ.template_polymorphic_ind ind env ->
- (** We refresh the universes so as to enforce using <= instead of instantiating
- an unkwown ?X with the template polymorphic type variable and destroying
- template polymorphism.
- e.g. when typechecking nil : Π A : Type n, list A, we don't
- want n to be used as the fixed carrier level of the list, so we
- refresh it preemptively. *)
- let univs, ty = Evarutil.get_template_constructor_type evdref cstr (List.length args) in
- univs, make_judge (mkConstruct cstr) ty
- | _ -> [], pretype empty_tycon env evdref lvar f
- in
+ let fj = pretype empty_tycon env evdref lvar f in
let floc = loc_of_glob_constr f in
let length = List.length args in
let candargs =
@@ -563,7 +550,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref lvar t =
with Not_found -> []
else []
in
- let rec apply_rec env n resj univs candargs = function
+ let rec apply_rec env n resj candargs = function
| [] -> resj
| c::rest ->
let argloc = loc_of_glob_constr c in
@@ -571,15 +558,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref lvar t =
let resty = whd_betadeltaiota env !evdref resj.uj_type in
match kind_of_term resty with
| Prod (na,c1,c2) ->
- let univs, tycon =
- match univs with
- | Some _ :: l ->
- if is_GHole c then
- l, Some (evd_comb1 (Evarsolve.refresh_universes ~template:true
- ~with_globals:true true) evdref c1)
- else l, Some c1
- | (None :: l) | l -> l, Some c1
- in
+ let tycon = Some c1 in
let hj = pretype tycon env evdref lvar c in
let candargs, ujval =
match candargs with
@@ -590,10 +569,8 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref lvar t =
else [], j_val hj
in
let value, typ = applist (j_val resj, [ujval]), subst1 ujval c2 in
- apply_rec env (n+1)
- { uj_val = value;
- uj_type = typ }
- univs candargs rest
+ let j = { uj_val = value; uj_type = typ } in
+ apply_rec env (n+1) j candargs rest
| _ ->
let hj = pretype empty_tycon env evdref lvar c in
@@ -601,7 +578,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref lvar t =
(Loc.merge floc argloc) env !evdref
resj [hj]
in
- let resj = apply_rec env 1 fj univs candargs args in
+ let resj = apply_rec env 1 fj candargs args in
let resj =
match evar_kind_of_term !evdref resj.uj_val with
| App (f,args) ->
@@ -611,30 +588,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref lvar t =
let c = mkApp (f,Array.map (whd_evar sigma) args) in
let t = Retyping.get_type_of env sigma c in
make_judge c (* use this for keeping evars: resj.uj_val *) t
- (* else *)
- (* if is_template_polymorphic_constructor env f then *)
- (* let ty = nf_evar !evdref resj.uj_type in *)
- (* if occur_existential resj.uj_type then *)
- (* (\* The type is not fully defined, e.g. list ?A where A : Type n *)
- (* for n the fixed template universe of lists. We don't want this *)
- (* n to escape (e.g. by later taking typeof(list A) = Type n) when *)
- (* instantiating other existentials. So we need to refresh the *)
- (* type of f and redo typechecking with this fresh type. *\) *)
- (* match kind_of_term f with *)
- (* | Construct ((ind, i as cstr,u)) -> *)
- (* (\** We refresh the universes so as to enforce using <= instead of instantiating *)
- (* an unkwown ?X with the template polymorphic type variable and destroying *)
- (* template polymorphism. *)
- (* e.g. when typechecking nil : Π A : Type n, list A, we don't *)
- (* want n to be used as the fixed carrier level of the list, so we *)
- (* refresh it preemptively. *\) *)
- (* evdref := initial_evd; *)
- (* let ty = Evarutil.get_template_constructor_type evdref cstr in *)
- (* let fj = make_judge (mkConstruct cstr) ty in *)
- (* typecheck_app fj *)
- (* | _ -> assert false *)
- (* else make_judge resj.uj_val ty *)
- else resj
+ else resj
| _ -> resj
in
inh_conv_coerce_to_tycon loc env evdref resj tycon
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 2f34f7efe..7702355b8 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -290,7 +290,7 @@ let e_type_of ?(refresh=false) env evd c =
let j = execute env evdref c in
(* side-effect on evdref *)
if refresh then
- Evarsolve.refresh_universes false !evdref j.uj_type
+ Evarsolve.refresh_universes false env !evdref j.uj_type
else !evdref, j.uj_type
let solve_evars env evdref c =
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 58296002f..4ad8f833e 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -936,7 +936,7 @@ let w_coerce env evd mv c =
w_coerce_to_type env evd c cty mvty
let unify_to_type env sigma flags c status u =
- let sigma, c = refresh_universes false sigma c in
+ let sigma, c = refresh_universes false env sigma c in
let t = get_type_of env sigma (nf_meta sigma c) in
let t = nf_betaiota sigma (nf_meta sigma t) in
unify_0 env sigma CUMUL flags t u
diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v
index a0ecdb756..c9d868c40 100644
--- a/theories/FSets/FMapPositive.v
+++ b/theories/FSets/FMapPositive.v
@@ -212,7 +212,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
try rewrite <- (gleaf i); auto; try apply IHi; congruence.
Qed.
- Lemma rleaf : forall (i : key), remove i (Leaf : t A) = Leaf.
+ Lemma rleaf : forall (i : key), remove i Leaf = Leaf.
Proof. destruct i; simpl; auto. Qed.
Theorem grs:
diff --git a/toplevel/record.ml b/toplevel/record.ml
index b3c052f01..d2aa48db9 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -93,7 +93,7 @@ let typecheck_params_and_fields def id t ps nots fs =
(match kind_of_term sred with
| Sort s' ->
(match Evd.is_sort_variable !evars s' with
- | Some (l, _) -> evars := Evd.make_flexible_variable !evars true (* (not def) *) l; sred
+ | Some l -> evars := Evd.make_flexible_variable !evars true (* (not def) *) l; sred
| None -> s)
| _ -> user_err_loc (constr_loc t,"", str"Sort expected."))
| None ->
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 12:59:14 +0000