diff options
Diffstat (limited to 'engine/evarutil.ml')
| -rw-r--r-- | engine/evarutil.ml | 209 |
1 files changed, 128 insertions, 81 deletions
diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 9cf81ecc..b77bf55d 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -13,7 +13,6 @@ open Util open Names open Term open Constr -open Pre_env open Environ open Evd open Termops @@ -23,7 +22,8 @@ module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration let safe_evar_value sigma ev = - try Some (Evd.existential_value sigma ev) + let ev = EConstr.of_existential ev in + try Some (EConstr.Unsafe.to_constr @@ Evd.existential_value sigma ev) with NotInstantiatedEvar | Not_found -> None (** Combinators *) @@ -44,11 +44,11 @@ let evd_comb2 f evdref x y = z let e_new_global evdref x = - EConstr.of_constr (evd_comb1 (Evd.fresh_global (Global.env())) evdref x) + evd_comb1 (Evd.fresh_global (Global.env())) evdref x let new_global evd x = let (evd, c) = Evd.fresh_global (Global.env()) evd x in - (evd, EConstr.of_constr c) + (evd, c) (****************************************************) (* Expanding/testing/exposing existential variables *) @@ -61,7 +61,7 @@ exception Uninstantiated_evar of Evar.t let rec flush_and_check_evars sigma c = match kind c with | Evar (evk,_ as ev) -> - (match existential_opt_value sigma ev with + (match existential_opt_value0 sigma ev with | None -> raise (Uninstantiated_evar evk) | Some c -> flush_and_check_evars sigma c) | _ -> Constr.map (flush_and_check_evars sigma) c @@ -72,9 +72,9 @@ let flush_and_check_evars sigma c = (** Term exploration up to instantiation. *) let kind_of_term_upto = EConstr.kind_upto -let nf_evar0 sigma t = EConstr.to_constr sigma (EConstr.of_constr t) +let nf_evar0 sigma t = EConstr.to_constr ~abort_on_undefined_evars:false sigma (EConstr.of_constr t) let whd_evar = EConstr.whd_evar -let nf_evar sigma c = EConstr.of_constr (EConstr.to_constr sigma c) +let nf_evar sigma c = EConstr.of_constr (EConstr.to_constr ~abort_on_undefined_evars:false sigma c) let j_nf_evar sigma j = { uj_val = nf_evar sigma j.uj_val; @@ -85,7 +85,7 @@ let tj_nf_evar sigma {utj_val=v;utj_type=t} = {utj_val=nf_evar sigma v;utj_type=t} let nf_evars_universes evm = - Universes.nf_evars_and_universes_opt_subst (safe_evar_value evm) + UnivSubst.nf_evars_and_universes_opt_subst (safe_evar_value evm) (Evd.universe_subst evm) let nf_evars_and_universes evm = @@ -102,7 +102,8 @@ let nf_evar_map_universes evm = if Univ.LMap.is_empty subst then evm, nf_evar0 evm else let f = nf_evars_universes evm in - Evd.raw_map (fun _ -> map_evar_info f) evm, f + let f' c = EConstr.of_constr (f (EConstr.Unsafe.to_constr c)) in + Evd.raw_map (fun _ -> map_evar_info f') evm, f let nf_named_context_evar sigma ctx = Context.Named.map (nf_evar0 sigma) ctx @@ -115,7 +116,7 @@ let nf_env_evar sigma env = let rel' = nf_rel_context_evar sigma (EConstr.rel_context env) in EConstr.push_rel_context rel' (reset_with_named_context (val_of_named_context nc') env) -let nf_evar_info evc info = map_evar_info (nf_evar0 evc) info +let nf_evar_info evc info = map_evar_info (nf_evar evc) info let nf_evar_map evm = Evd.raw_map (fun _ evi -> nf_evar_info evm evi) evm @@ -212,7 +213,7 @@ let mk_new_meta () = EConstr.mkMeta(new_meta()) let non_instantiated sigma = let listev = Evd.undefined_map sigma in - Evar.Map.smartmap (fun evi -> nf_evar_info sigma evi) listev + Evar.Map.Smart.map (fun evi -> nf_evar_info sigma evi) listev (************************) (* Manipulating filters *) @@ -340,7 +341,15 @@ let update_var src tgt subst = let csubst_var = Id.Map.add id (Constr.mkVar tgt) subst.csubst_var in { subst with csubst_var; csubst_rev } -let push_rel_decl_to_named_context sigma decl (subst, avoid, nc) = +type naming_mode = + | KeepUserNameAndRenameExistingButSectionNames + | KeepUserNameAndRenameExistingEvenSectionNames + | KeepExistingNames + | FailIfConflict + +let push_rel_decl_to_named_context + ?(hypnaming=KeepUserNameAndRenameExistingButSectionNames) + sigma decl (subst, avoid, nc) = let open EConstr in let open Vars in let map_decl f d = @@ -371,7 +380,9 @@ let push_rel_decl_to_named_context sigma decl (subst, avoid, nc) = next_ident_away (id_of_name_using_hdchar empty_env sigma (RelDecl.get_type decl) na) avoid in match extract_if_neq id na with - | Some id0 when not (is_section_variable id0) -> + | Some id0 when hypnaming = KeepUserNameAndRenameExistingEvenSectionNames || + hypnaming = KeepUserNameAndRenameExistingButSectionNames && + not (is_section_variable id0) -> (* spiwack: if [id<>id0], rather than introducing a new binding named [id], we will keep [id0] (the name given by the user) and rename [id0] into [id] in the named @@ -380,6 +391,8 @@ let push_rel_decl_to_named_context sigma decl (subst, avoid, nc) = let d = decl |> NamedDecl.of_rel_decl (fun _ -> id0) |> map_decl (csubst_subst subst) in let nc = List.map (replace_var_named_declaration id0 id) nc in (push_var id0 subst, Id.Set.add id avoid, d :: nc) + | Some id0 when hypnaming = FailIfConflict -> + user_err Pp.(Id.print id0 ++ str " is already used.") | _ -> (* spiwack: if [id0] is a section variable renaming it is incorrect. We revert to a less robust behaviour where @@ -388,7 +401,7 @@ let push_rel_decl_to_named_context sigma decl (subst, avoid, nc) = let d = decl |> NamedDecl.of_rel_decl (fun _ -> id) |> map_decl (csubst_subst subst) in (push_var id subst, Id.Set.add id avoid, d :: nc) -let push_rel_context_to_named_context env sigma typ = +let push_rel_context_to_named_context ?hypnaming env sigma typ = (* compute the instances relative to the named context and rel_context *) let open Context.Named.Declaration in let open EConstr in @@ -403,7 +416,7 @@ let push_rel_context_to_named_context env sigma typ = (* with vars of the rel context *) (* We do keep the instances corresponding to local definition (see above) *) let (subst, _, env) = - Context.Rel.fold_outside (fun d acc -> push_rel_decl_to_named_context sigma d acc) + Context.Rel.fold_outside (fun d acc -> push_rel_decl_to_named_context ?hypnaming sigma d acc) (rel_context env) ~init:(empty_csubst, avoid, named_context env) in (val_of_named_context env, csubst_subst subst typ, inst_rels@inst_vars, subst) @@ -413,25 +426,18 @@ let push_rel_context_to_named_context env sigma typ = let default_source = Loc.tag @@ Evar_kinds.InternalHole -let restrict_evar evd evk filter ?src candidates = - let candidates = Option.map (fun l -> List.map EConstr.Unsafe.to_constr l) candidates in - let evd, evk' = Evd.restrict evk filter ?candidates ?src evd in - Evd.declare_future_goal evk' evd, evk' - let new_pure_evar_full evd evi = let (evd, evk) = Evd.new_evar evd evi in let evd = Evd.declare_future_goal evk evd in (evd, evk) -let new_pure_evar sign evd ?(src=default_source) ?(filter = Filter.identity) ?candidates ?(store = Store.empty) ?naming ?(principal=false) typ = - let typ = EConstr.Unsafe.to_constr typ in - let candidates = Option.map (fun l -> List.map EConstr.Unsafe.to_constr l) candidates in - let default_naming = Misctypes.IntroAnonymous in +let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?candidates ?(store = Store.empty) ?naming ?(principal=false) sign evd typ = + let default_naming = IntroAnonymous in let naming = Option.default default_naming naming in let name = match naming with - | Misctypes.IntroAnonymous -> None - | Misctypes.IntroIdentifier id -> Some id - | Misctypes.IntroFresh id -> + | IntroAnonymous -> None + | IntroIdentifier id -> Some id + | IntroFresh id -> let has_name id = try let _ = Evd.evar_key id evd in true with Not_found -> false in let id = Namegen.next_ident_away_from id has_name in Some id @@ -452,14 +458,14 @@ let new_pure_evar sign evd ?(src=default_source) ?(filter = Filter.identity) ?ca in (evd, newevk) -let new_evar_instance sign evd typ ?src ?filter ?candidates ?store ?naming ?principal instance = +let new_evar_instance ?src ?filter ?candidates ?store ?naming ?principal sign evd typ instance = let open EConstr in assert (not !Flags.debug || List.distinct (ids_of_named_context (named_context_of_val sign))); let (evd, newevk) = new_pure_evar sign evd ?src ?filter ?candidates ?store ?naming ?principal typ in evd, mkEvar (newevk,Array.of_list instance) -let new_evar_from_context sign evd ?src ?filter ?candidates ?store ?naming ?principal typ = +let new_evar_from_context ?src ?filter ?candidates ?store ?naming ?principal sign evd typ = let instance = List.map (NamedDecl.get_id %> EConstr.mkVar) (named_context_of_val sign) in let instance = match filter with @@ -469,8 +475,8 @@ let new_evar_from_context sign evd ?src ?filter ?candidates ?store ?naming ?prin (* [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 env evd ?src ?filter ?candidates ?store ?naming ?principal typ = - let sign,typ',instance,subst = push_rel_context_to_named_context env evd typ in +let new_evar ?src ?filter ?candidates ?store ?naming ?principal ?hypnaming env evd typ = + let sign,typ',instance,subst = push_rel_context_to_named_context ?hypnaming env evd typ in let map c = csubst_subst subst c in let candidates = Option.map (fun l -> List.map map l) candidates in let instance = @@ -479,31 +485,46 @@ let new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal typ = | Some filter -> Filter.filter_list filter instance in new_evar_instance sign evd typ' ?src ?filter ?candidates ?store ?naming ?principal instance -let new_type_evar env evd ?src ?filter ?naming ?principal rigid = +let new_type_evar ?src ?filter ?naming ?principal ?hypnaming env evd rigid = let (evd', s) = new_sort_variable rigid evd in - let (evd', e) = new_evar env evd' ?src ?filter ?naming ?principal (EConstr.mkSort s) in + let (evd', e) = new_evar env evd' ?src ?filter ?naming ?principal ?hypnaming (EConstr.mkSort s) in evd', (e, s) -let e_new_type_evar env evdref ?src ?filter ?naming ?principal rigid = - let (evd, c) = new_type_evar env !evdref ?src ?filter ?naming ?principal rigid in +let e_new_type_evar env evdref ?src ?filter ?naming ?principal ?hypnaming rigid = + let (evd, c) = new_type_evar env !evdref ?src ?filter ?naming ?principal ?hypnaming rigid in evdref := evd; c -let new_Type ?(rigid=Evd.univ_flexible) env evd = +let new_Type ?(rigid=Evd.univ_flexible) evd = let open EConstr in let (evd, s) = new_sort_variable rigid evd in (evd, mkSort s) -let e_new_Type ?(rigid=Evd.univ_flexible) env evdref = +let e_new_Type ?(rigid=Evd.univ_flexible) evdref = let evd', s = new_sort_variable rigid !evdref in evdref := evd'; EConstr.mkSort s (* The same using side-effect *) -let e_new_evar env evdref ?(src=default_source) ?filter ?candidates ?store ?naming ?principal ty = - let (evd',ev) = new_evar env !evdref ~src:src ?filter ?candidates ?store ?naming ?principal ty in +let e_new_evar env evdref ?(src=default_source) ?filter ?candidates ?store ?naming ?principal ?hypnaming ty = + let (evd',ev) = new_evar env !evdref ~src:src ?filter ?candidates ?store ?naming ?principal ?hypnaming ty in evdref := evd'; ev +(* Safe interface to unification problems *) +type unification_pb = conv_pb * env * EConstr.constr * EConstr.constr + +let eq_unification_pb evd (pbty,env,t1,t2) (pbty',env',t1',t2') = + pbty == pbty' && env == env' && + EConstr.eq_constr evd t1 t1' && + EConstr.eq_constr evd t2 t2' + +let add_unification_pb ?(tail=false) pb evd = + let conv_pbs = Evd.conv_pbs evd in + if not (List.exists (eq_unification_pb evd pb) conv_pbs) then + let (pbty,env,t1,t2) = pb in + Evd.add_conv_pb ~tail (pbty,env,t1,t2) evd + else evd + (* This assumes an evar with identity instance and generalizes it over only the de Bruijn part of the context *) let generalize_evar_over_rels sigma (ev,args) = @@ -513,7 +534,7 @@ let generalize_evar_over_rels sigma (ev,args) = List.fold_left2 (fun (c,inst as x) a d -> if isRel sigma a then (mkNamedProd_or_LetIn d c,a::inst) else x) - (EConstr.of_constr evi.evar_concl,[]) (Array.to_list args) sign + (evi.evar_concl,[]) (Array.to_list args) sign (************************************) (* Removing a dependency in an evar *) @@ -522,11 +543,33 @@ let generalize_evar_over_rels sigma (ev,args) = type clear_dependency_error = | OccurHypInSimpleClause of Id.t option | EvarTypingBreak of existential +| NoCandidatesLeft of Evar.t -exception ClearDependencyError of Id.t * clear_dependency_error +exception ClearDependencyError of Id.t * clear_dependency_error * GlobRef.t option exception Depends of Id.t +let set_of_evctx l = + List.fold_left (fun s decl -> Id.Set.add (NamedDecl.get_id decl) s) Id.Set.empty l + +let filter_effective_candidates evd evi filter candidates = + let ids = set_of_evctx (Filter.filter_list filter (evar_context evi)) in + List.filter (fun a -> Id.Set.subset (collect_vars evd a) ids) candidates + +let restrict_evar evd evk filter ?src candidates = + let evar_info = Evd.find_undefined evd evk in + let candidates = Option.map (filter_effective_candidates evd evar_info filter) candidates in + match candidates with + | Some [] -> raise (ClearDependencyError (*FIXME*)(Id.of_string "blah", (NoCandidatesLeft evk), None)) + | _ -> + let evd, evk' = Evd.restrict evk filter ?candidates ?src evd in + (** Mark new evar as future goal, removing previous one, + circumventing Proofview.advance but making Proof.run_tactic catch these. *) + let future_goals = Evd.save_future_goals evd in + let future_goals = Evd.filter_future_goals (fun evk' -> not (Evar.equal evk evk')) future_goals in + let evd = Evd.restore_future_goals evd future_goals in + (Evd.declare_future_goal evk' evd, evk') + let rec check_and_clear_in_constr env evdref err ids global c = (* returns a new constr where all the evars have been 'cleaned' (ie the hypotheses ids have been removed from the contexts of @@ -534,13 +577,13 @@ let rec check_and_clear_in_constr env evdref err ids global c = is a section variable *) match kind c with | Var id' -> - if Id.Set.mem id' ids then raise (ClearDependencyError (id', err)) else c + if Id.Set.mem id' ids then raise (ClearDependencyError (id', err, None)) else c | ( Const _ | Ind _ | Construct _ ) -> let () = if global then let check id' = if Id.Set.mem id' ids then - raise (ClearDependencyError (id',err)) + raise (ClearDependencyError (id',err,Some (Globnames.global_of_constr c))) in Id.Set.iter check (Environ.vars_of_global env c) in @@ -549,7 +592,8 @@ let rec check_and_clear_in_constr env evdref err ids global c = | Evar (evk,l as ev) -> if Evd.is_defined !evdref evk then (* If evk is already defined we replace it by its definition *) - let nc = Evd.existential_value !evdref ev in + let nc = Evd.existential_value !evdref (EConstr.of_existential ev) in + let nc = EConstr.Unsafe.to_constr nc in (check_and_clear_in_constr env evdref err ids global nc) else (* We check for dependencies to elements of ids in the @@ -559,8 +603,7 @@ let rec check_and_clear_in_constr env evdref err ids global c = removed *) let evi = Evd.find_undefined !evdref evk in let ctxt = Evd.evar_filtered_context evi in - let ctxt = List.map (fun d -> map_named_decl EConstr.of_constr d) ctxt in - let (rids,filter) = + let (rids,filter) = List.fold_right2 (fun h a (ri,filter) -> try @@ -586,25 +629,29 @@ let rec check_and_clear_in_constr env evdref err ids global c = try let nids = Id.Map.domain rids in let global = Id.Set.exists is_section_variable nids in - check_and_clear_in_constr env evdref (EvarTypingBreak ev) nids global (evar_concl evi) - with ClearDependencyError (rid,err) -> - raise (ClearDependencyError (Id.Map.find rid rids,err)) in + let concl = EConstr.Unsafe.to_constr (evar_concl evi) in + check_and_clear_in_constr env evdref (EvarTypingBreak ev) nids global concl + with ClearDependencyError (rid,err,where) -> + raise (ClearDependencyError (Id.Map.find rid rids,err,where)) in if Id.Map.is_empty rids then c else let origfilter = Evd.evar_filter evi in let filter = Evd.Filter.apply_subfilter origfilter filter in let evd = !evdref in - let (evd,_) = restrict_evar evd evk filter None in + let candidates = Evd.evar_candidates evi in + let candidates = Option.map (List.map EConstr.of_constr) candidates in + let (evd,_) = restrict_evar evd evk filter candidates in evdref := evd; - Evd.existential_value !evdref ev + Evd.existential_value0 !evdref ev | _ -> Constr.map (check_and_clear_in_constr env evdref err ids global) c -let clear_hyps_in_evi_main env evdref hyps terms ids = +let clear_hyps_in_evi_main env sigma hyps terms ids = (* clear_hyps_in_evi erases hypotheses ids in hyps, checking if some hypothesis does not depend on a element of ids, and erases ids in the contexts of the evars occurring in evi *) + let evdref = ref sigma in let terms = List.map EConstr.Unsafe.to_constr terms in let global = Id.Set.exists is_section_variable ids in let terms = @@ -627,23 +674,23 @@ let clear_hyps_in_evi_main env evdref hyps terms ids = in remove_hyps ids check_context check_value hyps in - (nhyps,List.map EConstr.of_constr terms) + (!evdref, nhyps,List.map EConstr.of_constr terms) -let clear_hyps_in_evi env evdref hyps concl ids = - match clear_hyps_in_evi_main env evdref hyps [concl] ids with - | (nhyps,[nconcl]) -> (nhyps,nconcl) +let clear_hyps_in_evi env sigma hyps concl ids = + match clear_hyps_in_evi_main env sigma hyps [concl] ids with + | (sigma,nhyps,[nconcl]) -> (sigma,nhyps,nconcl) | _ -> assert false -let clear_hyps2_in_evi env evdref hyps t concl ids = - match clear_hyps_in_evi_main env evdref hyps [t;concl] ids with - | (nhyps,[t;nconcl]) -> (nhyps,t,nconcl) +let clear_hyps2_in_evi env sigma hyps t concl ids = + match clear_hyps_in_evi_main env sigma hyps [t;concl] ids with + | (sigma,nhyps,[t;nconcl]) -> (sigma,nhyps,t,nconcl) | _ -> assert false (* spiwack: a few functions to gather evars on which goals depend. *) let queue_set q is_dependent set = Evar.Set.iter (fun a -> Queue.push (is_dependent,a) q) set let queue_term q is_dependent c = - queue_set q is_dependent (evars_of_term c) + queue_set q is_dependent (evars_of_term (EConstr.Unsafe.to_constr c)) let process_dependent_evar q acc evm is_dependent e = let evi = Evd.find evm e in @@ -656,12 +703,12 @@ let process_dependent_evar q acc evm is_dependent e = match decl with | LocalAssum _ -> () | LocalDef (_,b,_) -> queue_term q true b - end (Environ.named_context_of_val evi.evar_hyps); + end (EConstr.named_context_of_val evi.evar_hyps); match evi.evar_body with | Evar_empty -> if is_dependent then Evar.Map.add e None acc else acc | Evar_defined b -> - let subevars = evars_of_term b in + let subevars = evars_of_term (EConstr.Unsafe.to_constr b) in (* evars appearing in the definition of an evar [e] are marked as dependent when [e] is dependent itself: if [e] is a non-dependent goal, then, unless they are reach from another @@ -729,11 +776,11 @@ let undefined_evars_of_named_context evd nc = ~init:Evar.Set.empty let undefined_evars_of_evar_info evd evi = - Evar.Set.union (undefined_evars_of_term evd (EConstr.of_constr evi.evar_concl)) + Evar.Set.union (undefined_evars_of_term evd evi.evar_concl) (Evar.Set.union (match evi.evar_body with | Evar_empty -> Evar.Set.empty - | Evar_defined b -> undefined_evars_of_term evd (EConstr.of_constr b)) + | Evar_defined b -> undefined_evars_of_term evd b) (undefined_evars_of_named_context evd (named_context_of_val evi.evar_hyps))) @@ -781,10 +828,11 @@ let filtered_undefined_evars_of_evar_info ?cache sigma evi = in let accu = match evi.evar_body with | Evar_empty -> Evar.Set.empty - | Evar_defined b -> evars_of_term b + | Evar_defined b -> evars_of_term (EConstr.Unsafe.to_constr b) in - let accu = Evar.Set.union (undefined_evars_of_term sigma (EConstr.of_constr evi.evar_concl)) accu in - evars_of_named_context cache accu (evar_filtered_context evi) + let accu = Evar.Set.union (undefined_evars_of_term sigma evi.evar_concl) accu in + let ctxt = EConstr.Unsafe.to_named_context (evar_filtered_context evi) in + evars_of_named_context cache accu ctxt (* spiwack: this is a more complete version of {!Termops.occur_evar}. The latter does not look recursively into an @@ -794,7 +842,7 @@ let occur_evar_upto sigma n c = let c = EConstr.Unsafe.to_constr c in let rec occur_rec c = match kind c with | Evar (sp,_) when Evar.equal sp n -> raise Occur - | Evar e -> Option.iter occur_rec (existential_opt_value sigma e) + | Evar e -> Option.iter occur_rec (existential_opt_value0 sigma e) | _ -> Constr.iter occur_rec c in try occur_rec c; false with Occur -> true @@ -807,22 +855,22 @@ let judge_of_new_Type evd = let (evd', s) = new_univ_variable univ_rigid evd in (evd', { uj_val = mkSort (Type s); uj_type = mkSort (Type (Univ.super s)) }) -let subterm_source evk (loc,k) = +let subterm_source evk ?where (loc,k) = let evk = match k with - | Evar_kinds.SubEvar (evk) -> evk + | Evar_kinds.SubEvar (None,evk) when where = None -> evk | _ -> evk in - (loc,Evar_kinds.SubEvar evk) + (loc,Evar_kinds.SubEvar (where,evk)) (* Add equality constraints for covariant/invariant positions. For irrelevant positions, unify universes when flexible. *) let compare_cumulative_instances cv_pb variances u u' sigma = - let open Universes in + let open UnivProblem in let cstrs = Univ.Constraint.empty in - let soft = Constraints.empty in + let soft = Set.empty in let cstrs, soft = Array.fold_left3 (fun (cstrs, soft) v u u' -> let open Univ.Variance in match v with - | Irrelevant -> cstrs, Constraints.add (UWeak (u,u')) soft + | Irrelevant -> cstrs, Set.add (UWeak (u,u')) soft | Covariant when cv_pb == Reduction.CUMUL -> Univ.Constraint.add (u,Univ.Le,u') cstrs, soft | Covariant | Invariant -> Univ.Constraint.add (u,Univ.Eq,u') cstrs, soft) @@ -834,10 +882,10 @@ let compare_cumulative_instances cv_pb variances u u' sigma = | exception Univ.UniverseInconsistency p -> Inr p let compare_constructor_instances evd u u' = - let open Universes in + let open UnivProblem in let soft = - Array.fold_left2 (fun cs u u' -> Constraints.add (UWeak (u,u')) cs) - Constraints.empty (Univ.Instance.to_array u) (Univ.Instance.to_array u') + Array.fold_left2 (fun cs u u' -> Set.add (UWeak (u,u')) cs) + Set.empty (Univ.Instance.to_array u) (Univ.Instance.to_array u') in Evd.add_universe_constraints evd soft @@ -849,17 +897,16 @@ let compare_constructor_instances evd u u' = let eq_constr_univs_test sigma1 sigma2 t u = (* spiwack: mild code duplication with {!Evd.eq_constr_univs}. *) let open Evd in + let t = EConstr.Unsafe.to_constr t + and u = EConstr.Unsafe.to_constr u in let fold cstr sigma = try Some (add_universe_constraints sigma cstr) with Univ.UniverseInconsistency _ | UniversesDiffer -> None in let ans = - Universes.eq_constr_univs_infer_with + 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 in match ans with None -> false | Some _ -> true - -type type_constraint = EConstr.types option -type val_constraint = EConstr.constr option |