aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/clenv.ml9
-rw-r--r--pretyping/evarconv.ml41
-rw-r--r--pretyping/evarconv.mli4
-rw-r--r--pretyping/evarutil.ml20
-rw-r--r--pretyping/evd.ml79
-rw-r--r--pretyping/evd.mli3
-rw-r--r--pretyping/retyping.ml6
-rw-r--r--pretyping/retyping.mli2
-rw-r--r--pretyping/unification.ml90
9 files changed, 170 insertions, 84 deletions
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index dd2af306c9..695d93ca89 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -73,7 +73,8 @@ let clenv_push_prod cl =
let mv = new_meta () in
let dep = dependent (mkRel 1) u in
let na' = if dep then na else Anonymous in
- let e' = meta_declare mv t ~name:na' cl.evd in
+ let evd,t' = Evd.universes_to_variables cl.evd t in
+ let e' = meta_declare mv t' ~name:na' evd in
let concl = if dep then subst1 (mkMeta mv) u else u in
let def = applist (cl.templval.rebus,[mkMeta mv]) in
{ templval = mk_freelisted def;
@@ -95,7 +96,8 @@ let clenv_environments evd bound t =
let mv = new_meta () in
let dep = dependent (mkRel 1) t2 in
let na' = if dep then na else Anonymous in
- let e' = meta_declare mv t1 ~name:na' e in
+ let e',t1' = Evd.universes_to_variables e t1 in
+ let e' = meta_declare mv t1' ~name:na' e' in
clrec (e', (mkMeta mv)::metas) (Option.map ((+) (-1)) n)
(if dep then (subst1 (mkMeta mv) t2) else t2)
| (n, LetIn (na,b,_,t)) -> clrec (e,metas) n (subst1 b t)
@@ -112,7 +114,8 @@ let clenv_environments_evars env evd bound t =
| (Some 0, _) -> (e, List.rev ts, t)
| (n, Cast (t,_,_)) -> clrec (e,ts) n t
| (n, Prod (na,t1,t2)) ->
- let e',constr = Evarutil.new_evar e env t1 in
+ let e',t1' = Evd.universes_to_variables e t1 in
+ let e',constr = Evarutil.new_evar e' env t1' in
let dep = dependent (mkRel 1) t2 in
clrec (e', constr::ts) (Option.map ((+) (-1)) n)
(if dep then (subst1 constr t2) else t2)
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index d6b10b7d0e..352b76dd94 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -24,6 +24,31 @@ open Evarutil
open Libnames
open Evd
+let base_sort_conv evd pb s0 s1 =
+ match (s0,s1) with
+ | (Prop c1, Prop c2) -> if c1 = Null or c2 = Pos then Some evd else None (* Prop <= Set *)
+ | (Prop c1, Type u) -> if pb = Reduction.CUMUL then Some evd else None
+ | (Type u, Prop c) ->
+ if Evd.is_sort_variable evd s0 then
+ Some (Evd.define_sort_variable evd s0 s1)
+ else None
+ | (Type u1, Type u2) -> Some evd
+
+let unify_constr_univ evd f cv_pb t1 t2 =
+ match kind_of_term t1, kind_of_term t2 with
+ Sort s1, Sort s2 ->
+ (match base_sort_conv !evd cv_pb s1 s2 with
+ | Some evd' -> evd := evd'; true
+ | None -> false)
+ | Prod (_,t1,c1), Prod (_,t2,c2) ->
+ f Reduction.CONV t1 t2 & f cv_pb c1 c2
+ | _ -> compare_constr (f Reduction.CONV) t1 t2
+
+let constr_unify_with_sorts evd cv_pb t1 t2 =
+ let evdref = ref evd in
+ let rec aux cv_pb t1 t2 = unify_constr_univ evdref aux cv_pb t1 t2 in
+ if aux cv_pb t1 t2 then true, !evdref else false, evd
+
type flex_kind_of_term =
| Rigid of constr
| MaybeFlexible of constr
@@ -376,8 +401,10 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
| _, Cast (c2,_,_) -> evar_eqappr_x env evd pbty appr1 (c2,l2)
| Sort s1, Sort s2 when l1=[] & l2=[] ->
- (evd,base_sort_cmp pbty s1 s2)
-
+ (match base_sort_conv evd pbty s1 s2 with
+ | Some evd' -> evd',true
+ | None -> evd, false)
+
| Lambda (na,c1,c'1), Lambda (_,c2,c'2) when l1=[] & l2=[] ->
ise_and evd
[(fun i -> evar_conv_x env i CONV c1 c2);
@@ -542,11 +569,11 @@ let apply_conversion_problem_heuristic env evd pbty t1 t2 =
let consider_remaining_unif_problems env evd =
let (evd,pbs) = extract_all_conv_pbs evd in
- List.fold_left
- (fun (evd,b as p) (pbty,env,t1,t2) ->
- if b then apply_conversion_problem_heuristic env evd pbty t1 t2 else p)
- (evd,true)
- pbs
+ List.fold_left
+ (fun (evd,b as p) (pbty,env,t1,t2) ->
+ if b then apply_conversion_problem_heuristic env evd pbty t1 t2 else p)
+ (evd,true)
+ pbs
(* Main entry points *)
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index a281a3898f..2a2cd52717 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -16,6 +16,10 @@ open Reductionops
open Evd
(*i*)
+(* Comparison function considering sort variables. *)
+val constr_unify_with_sorts : evar_defs -> conv_pb ->
+ types -> types -> bool * evar_defs
+
(* returns exception Reduction.NotConvertible if not unifiable *)
val the_conv_x : env -> constr -> constr -> evar_defs -> evar_defs
val the_conv_x_leq : env -> constr -> constr -> evar_defs -> evar_defs
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index e7682285b9..8e9ddf1baf 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -947,22 +947,22 @@ and evar_define ?(choose=false) env (evk,_ as ev) rhs evd =
(* Auxiliary functions for the conversion algorithms modulo evars
*)
-let has_undefined_evars evd t =
- let evm = evd in
+let has_undefined_evars_or_sorts evd t =
let rec has_ev t =
match kind_of_term t with
- Evar (ev,args) ->
- (match evar_body (Evd.find evm ev) with
- | Evar_defined c ->
- has_ev c; Array.iter has_ev args
- | Evar_empty ->
- raise NotInstantiatedEvar)
- | _ -> iter_constr has_ev t in
+ | Evar (ev,args) ->
+ (match evar_body (Evd.find evd ev) with
+ | Evar_defined c ->
+ has_ev c; Array.iter has_ev args
+ | Evar_empty ->
+ raise NotInstantiatedEvar)
+ | Sort s when is_sort_variable evd s -> raise Not_found
+ | _ -> iter_constr has_ev t in
try let _ = has_ev t in false
with (Not_found | NotInstantiatedEvar) -> true
let is_ground_term evd t =
- not (has_undefined_evars evd t)
+ not (has_undefined_evars_or_sorts evd t)
let is_ground_env evd env =
let is_ground_decl = function
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 500e190020..79cdc7da58 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -184,9 +184,13 @@ type sort_constraints = sort_constraint UniverseMap.t
let rec canonical_find u scstr =
match UniverseMap.find u scstr with
- EqSort u' -> canonical_find u' scstr
- | c -> (u,c)
+ | EqSort u' -> canonical_find u' scstr
+ | c -> (u,c)
+let find_univ u scstr =
+ try canonical_find u scstr
+ with Not_found -> u, DefinedSort (Type u)
+
let whd_sort_var scstr t =
match kind_of_term t with
Sort(Type u) ->
@@ -238,7 +242,6 @@ let new_sort_var cstr =
let u = Termops.new_univ() in
(u, UniverseMap.add u (SortVar([],[])) cstr)
-
let set_leq_sort (u1,(leq1,geq1)) (u2,(leq2,geq2)) scstr =
let rec search_rec (is_b, betw, not_betw) u1 =
if List.mem u1 betw then (true, betw, not_betw)
@@ -264,8 +267,8 @@ let set_leq_sort (u1,(leq1,geq1)) (u2,(leq2,geq2)) scstr =
let set_leq s1 s2 scstr =
let u1 = var_of_sort s1 in
let u2 = var_of_sort s2 in
- let (cu1,c1) = canonical_find u1 scstr in
- let (cu2,c2) = canonical_find u2 scstr in
+ let (cu1,c1) = find_univ u1 scstr in
+ let (cu2,c2) = find_univ u2 scstr in
if cu1=cu2 then scstr
else
match c1,c2 with
@@ -315,8 +318,11 @@ module EvarMap = struct
let eq_evar_map x y = x == y ||
(EvarInfoMap.equal eq_evar_info (fst x) (fst y) &&
UniverseMap.equal (=) (snd x) (snd y))
-
- let merge e e' = fold (fun n v sigma -> add sigma n v) e' e
+ let constraints (sigma,sm) = sm
+ let merge (sigma,sm) (sigma',sm') =
+ let ev = EvarInfoMap.fold (fun n v sigma -> EvarInfoMap.add sigma n v) sigma' sigma in
+ let sm = UniverseMap.fold (fun u cstr sm -> UniverseMap.add u cstr sm) sm' sm in
+ (ev,sm)
end
@@ -479,11 +485,10 @@ let subst_evar_info s evi =
evar_body = subst_evb evi.evar_body }
let subst_evar_defs_light sub evd =
- assert (UniverseMap.is_empty (snd evd.evars));
assert (evd.conv_pbs = []);
{ evd with
- metas = Metamap.map (map_clb (subst_mps sub)) evd.metas;
- evars = ExistentialMap.map (subst_evar_info sub) (fst evd.evars), snd evd.evars
+ metas = Metamap.map (map_clb (subst_mps sub)) evd.metas;
+ evars = ExistentialMap.map (subst_evar_info sub) (fst evd.evars), (snd evd.evars);
}
let subst_evar_map = subst_evar_defs_light
@@ -572,6 +577,9 @@ let extract_changed_conv_pbs evd p =
let extract_all_conv_pbs evd =
extract_conv_pbs evd (fun _ -> true)
+let solve_sort_cstrs cstrs = (* TODO: Check validity *)
+ UniverseMap.empty
+
(* spiwack: should it be replaced by Evd.merge? *)
let evar_merge evd evars =
{ evd with evars = EvarMap.merge evd.evars evars.evars }
@@ -590,6 +598,30 @@ let set_leq_sort_variable ({evars=(sigma,sm)}as d) u1 u2 =
let define_sort_variable ({evars=(sigma,sm)}as d) u s =
{ d with evars = (sigma, set_sort_variable u s sm) }
let pr_sort_constraints {evars=(_,sm)} = pr_sort_cstrs sm
+let solve_sort_constraints ({evars=(sigma,sm)} as d) =
+ { d with evars = (sigma, solve_sort_cstrs sm) }
+
+(* This refreshes universes in types introducing sort variables;
+ works only for inferred types (i.e. for
+ types of the form (x1:A1)...(xn:An)B with B a sort or an atom in
+ head normal form) *)
+let universes_to_variables_gen strict evd t =
+ let modified = ref false in
+ let evdref = ref evd in
+ let rec refresh t = match kind_of_term t with
+ | Sort (Type u as us) when strict or u <> Univ.type0m_univ ->
+(* if Univ.is_univ_variable u then *)
+ let s', evd = new_sort_variable !evdref in
+ let evd = set_leq_sort_variable evd s' us in
+ evdref := evd; modified := true; mkSort s'
+(* else t *)
+ | Prod (na,u,v) -> mkProd (na,u,refresh v)
+ | _ -> t in
+ let t' = refresh t in
+ if !modified then !evdref, t' else evd, t
+
+let universes_to_variables = universes_to_variables_gen false
+let universes_to_variables_strict = universes_to_variables_gen true
(**********************************************************)
(* Accessing metas *)
@@ -764,10 +796,12 @@ let pr_meta_map mmap =
hov 0
(pr_meta mv ++ pr_name na ++ str " : " ++
print_constr b.rebus ++ fnl ())
- | (mv,Clval(na,(b,s),_)) ->
+ | (mv,Clval(na,(b,s),t)) ->
hov 0
(pr_meta mv ++ pr_name na ++ str " := " ++
- print_constr b.rebus ++ spc () ++ pr_instance_status s ++ fnl ())
+ print_constr b.rebus ++
+ str " : " ++ print_constr t.rebus ++
+ spc () ++ pr_instance_status s ++ fnl ())
in
prlist pr_meta_binding (metamap_to_list mmap)
@@ -788,12 +822,19 @@ let pr_evar_info evi =
in
hov 2 (str"[" ++ phyps ++ spc () ++ str"|- " ++ pty ++ pb ++ str"]")
-let pr_evar_defs_t sigma =
- h 0
- (prlist_with_sep pr_fnl
- (fun (ev,evi) ->
- h 0 (str(string_of_existential ev)++str"=="++ pr_evar_info evi))
- (EvarMap.to_list sigma))
+let pr_evar_defs_t (evars,cstrs as sigma) =
+ let evs =
+ if evars = EvarInfoMap.empty then mt ()
+ else
+ str"EVARS:"++brk(0,1)++
+ h 0 (prlist_with_sep pr_fnl
+ (fun (ev,evi) ->
+ h 0 (str(string_of_existential ev)++str"=="++ pr_evar_info evi))
+ (EvarMap.to_list sigma))++fnl()
+ and cs =
+ if cstrs = UniverseMap.empty then mt ()
+ else pr_sort_cstrs cstrs++fnl()
+ in evs ++ cs
let pr_constraints pbs =
h 0
@@ -807,7 +848,7 @@ let pr_constraints pbs =
let pr_evar_defs evd =
let pp_evm =
if evd.evars = EvarMap.empty then mt() else
- str"EVARS:"++brk(0,1)++pr_evar_defs_t evd.evars++fnl() in
+ pr_evar_defs_t evd.evars++fnl() in
let cstrs =
if evd.conv_pbs = [] then mt() else
str"CONSTRAINTS:"++brk(0,1)++pr_constraints evd.conv_pbs++fnl() in
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index e5cf8e2690..a26c2dadcd 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -241,6 +241,9 @@ val is_sort_variable : evar_defs -> sorts -> bool
val whd_sort_variable : evar_defs -> constr -> constr
val set_leq_sort_variable : evar_defs -> sorts -> sorts -> evar_defs
val define_sort_variable : evar_defs -> sorts -> sorts -> evar_defs
+val solve_sort_constraints : evar_defs -> evar_defs
+
+val universes_to_variables : evar_defs -> types -> evar_defs * types
(*********************************************************************)
(* constr with holes *)
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index eeee0c313d..b16508053a 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -161,8 +161,10 @@ let type_of_global_reference_knowing_conclusion env sigma c conclty =
(* We are outside the kernel: we take fresh universes *)
(* to avoid tactics and co to refresh universes themselves *)
-let get_type_of env sigma c =
- let f,_,_,_ = retype sigma in refresh_universes (f env c)
+let get_type_of ?(refresh=true) env sigma c =
+ let f,_,_,_ = retype sigma in
+ let t = f env c in
+ if refresh then refresh_universes t else t
(* Makes an assumption from a constr *)
let get_assumption_of env evc c = c
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli
index be42fd8585..9b65494c1e 100644
--- a/pretyping/retyping.mli
+++ b/pretyping/retyping.mli
@@ -21,7 +21,7 @@ open Environ
either produces a wrong result or raise an anomaly. Use with care.
It doesn't handle predicative universes too. *)
-val get_type_of : env -> evar_map -> constr -> types
+val get_type_of : ?refresh:bool -> env -> evar_map -> constr -> types
val get_sort_of : env -> evar_map -> types -> sorts
val get_sort_family_of : env -> evar_map -> types -> sorts_family
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 83c7b83704..48c8d65847 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -55,6 +55,10 @@ let abstract_list_all env evd typ c l =
(**)
+let get_type_of_with_variables env evd c =
+ let t = Retyping.get_type_of ~refresh:false env evd c in
+ Evd.universes_to_variables evd t
+
(* A refinement of [conv_pb]: the integers tells how many arguments
were applied in the context of the conversion problem; if the number
is non zero, steps of eta-expansion will be allowed
@@ -170,19 +174,24 @@ let oracle_order env cf1 cf2 =
match cf2 with
| None -> Some true
| Some k2 -> Some (Conv_oracle.oracle_order k1 k2)
-
+
+let is_trans_fconv_pb pb flags env sigma m n =
+ match pb with
+ | Cumul -> is_trans_fconv CUMUL flags env sigma m n
+ | ConvUnderApp _ -> is_trans_fconv CONV flags env sigma m n
+
let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flags m n =
let trivial_unify curenv pb (sigma,metasubst,_) m n =
let subst = if flags.use_metas_eagerly then metasubst else ms in
- match subst_defined_metas subst m with
- | Some m1 ->
+ match subst_defined_metas subst m, subst_defined_metas subst n with
+ | Some m1, Some n1 ->
if (match flags.modulo_conv_on_closed_terms with
Some flags ->
- is_trans_fconv (conv_pb_of pb) flags env sigma m1 n
+ is_trans_fconv_pb pb flags env sigma m1 n1
| None -> false) then true else
- if (not (is_ground_term (create_evar_defs sigma) m1))
- || occur_meta_or_existential n then false else
- error_cannot_unify curenv sigma (m, n)
+ let evd = create_evar_defs sigma in
+ if not (is_ground_term evd m1) || not (is_ground_term evd n1)
+ then false else error_cannot_unify curenv sigma (m, n)
| _ -> false in
let rec unirec_rec (curenv,nb as curenvnb) pb b ((sigma,metasubst,evarsubst) as substn) curm curn =
let cM = Evarutil.whd_castappevar sigma curm
@@ -261,12 +270,14 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
| _ ->
try canonical_projections curenvnb pb b cM cN substn
with ex when precatchable_exception ex ->
- if constr_cmp (conv_pb_of cv_pb) cM cN then substn else
- let (f1,l1) =
- match kind_of_term cM with App (f,l) -> (f,l) | _ -> (cM,[||]) in
- let (f2,l2) =
- match kind_of_term cN with App (f,l) -> (f,l) | _ -> (cN,[||]) in
- expand curenvnb pb b substn cM f1 l1 cN f2 l2
+ let (unif,sigma') = Evarconv.constr_unify_with_sorts sigma (conv_pb_of cv_pb) cM cN in
+ if unif then (sigma',metasubst,evarsubst)
+ else
+ let (f1,l1) =
+ match kind_of_term cM with App (f,l) -> (f,l) | _ -> (cM,[||]) in
+ let (f2,l2) =
+ match kind_of_term cN with App (f,l) -> (f,l) | _ -> (cN,[||]) in
+ expand curenvnb pb b substn cM f1 l1 cN f2 l2
and expand (curenv,_ as curenvnb) pb b (sigma, _, _ as substn) cM f1 l1 cN f2 l2 =
if trivial_unify curenv pb substn cM cN then substn
@@ -350,19 +361,19 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
unirec_rec curenvnb pb b substn c1 (applist (c,(List.rev ks)))
in
- if (if occur_meta m then false else
- if (match flags.modulo_conv_on_closed_terms with
- Some flags ->
- is_trans_fconv (conv_pb_of cv_pb) flags env sigma m n
- | None -> constr_cmp (conv_pb_of cv_pb) m n) then true else
+ if (if occur_meta m || occur_meta n then false else
+ if (match flags.modulo_conv_on_closed_terms with
+ | Some flags ->
+ is_trans_fconv_pb cv_pb flags env sigma m n
+ | None -> fst (Evarconv.constr_unify_with_sorts sigma (conv_pb_of cv_pb) m n)) then true else
if (not (is_ground_term (create_evar_defs sigma) m))
- || occur_meta_or_existential n then false else
- if (match flags.modulo_conv_on_closed_terms, flags.modulo_delta with
- | Some (cv_id, cv_k), (dl_id, dl_k) ->
- Idpred.subset dl_id cv_id && Cpred.subset dl_k cv_k
- | None,(dl_id, dl_k) ->
- Idpred.is_empty dl_id && Cpred.is_empty dl_k)
- then error_cannot_unify env sigma (m, n) else false)
+ || occur_meta_or_existential n then false else
+ if (match flags.modulo_conv_on_closed_terms, flags.modulo_delta with
+ | Some (cv_id, cv_k), (dl_id, dl_k) ->
+ Idpred.subset dl_id cv_id && Cpred.subset dl_k cv_k
+ | None,(dl_id, dl_k) ->
+ Idpred.is_empty dl_id && Cpred.is_empty dl_k)
+ then error_cannot_unify env sigma (m, n) else false)
then subst
else
unirec_rec (env,0) cv_pb conv_at_top subst m n
@@ -541,13 +552,12 @@ let w_coerce_to_type env evd c cty mvty =
try_to_coerce env evd c cty tycon
let w_coerce env evd mv c =
- let cty = get_type_of env evd c in
+ let evd,cty = get_type_of_with_variables env evd c in
let mvty = Typing.meta_type evd mv in
w_coerce_to_type env evd c cty mvty
let unify_to_type env sigma flags c status u =
- let c = refresh_universes c in
- let t = get_type_of env sigma c in
+ let sigma, t = get_type_of_with_variables env sigma c in
let t = Tacred.hnf_constr env sigma (nf_betaiota sigma (nf_meta sigma t)) in
let u = Tacred.hnf_constr env sigma u in
if status = IsSuperType then
@@ -561,9 +571,9 @@ let unify_to_type env sigma flags c status u =
let unify_type env sigma flags mv status c =
let mvty = Typing.meta_type sigma mv in
-(* if occur_meta_or_existential mvty or is_arity env sigma mvty then *)
+ if occur_meta_or_existential mvty or is_arity env sigma mvty then
unify_to_type env sigma flags c status mvty
-(* else (sigma,[],[]) *)
+ else (sigma,[],[])
(* Move metas that may need coercion at the end of the list of instances *)
@@ -677,19 +687,15 @@ let w_unify_meta_types env ?(flags=default_unify_flags) evd =
[clenv_typed_unify M N clenv] expects in addition that expected
types of metavars are unifiable with the types of their instances *)
-let check_types env flags (sigma,_,_ as subst) m n =
- if isEvar_or_Meta (fst (whd_stack sigma m)) then
- unify_0_with_initial_metas subst true env Cumul
- flags
- (Retyping.get_type_of env sigma n)
- (Retyping.get_type_of env sigma m)
- else if isEvar_or_Meta (fst (whd_stack sigma n)) then
- unify_0_with_initial_metas subst true env Cumul
- flags
- (Retyping.get_type_of env sigma m)
- (Retyping.get_type_of env sigma n)
+let check_types env flags (sigma,ms,es as subst) m n =
+ if isEvar_or_Meta (fst (whd_stack sigma m)) ||
+ isEvar_or_Meta (fst (whd_stack sigma n)) then
+ let sigma, mt = get_type_of_with_variables env sigma m in
+ let sigma, nt = get_type_of_with_variables env sigma n in
+ unify_0_with_initial_metas (sigma,ms,es) true env topconv
+ flags mt nt
else subst
-
+
let w_unify_core_0 env with_types cv_pb flags m n evd =
let (mc1,evd') = retract_coercible_metas evd in
let (sigma,ms,es) = check_types env flags (evd,mc1,[]) m n in
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:10:18 +0000