From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 14:31:27 -0500 Subject: Imported Upstream version 8.8.2 --- pretyping/evarconv.ml | 461 +++++++++++++++++++++++++++++++------------------- 1 file changed, 290 insertions(+), 171 deletions(-) (limited to 'pretyping/evarconv.ml') diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 9fd55a48..d37090a6 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -1,37 +1,41 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* - env -> evar_map -> conv_pb -> constr -> constr -> Evarsolve.unification_result + env -> evar_map -> conv_pb -> EConstr.constr -> EConstr.constr -> Evarsolve.unification_result let debug_unification = ref (false) let _ = Goptions.declare_bool_option { - Goptions.optsync = true; Goptions.optdepr = false; + Goptions.optdepr = false; Goptions.optname = "Print states sent to Evarconv unification"; Goptions.optkey = ["Debug";"Unification"]; @@ -39,6 +43,31 @@ let _ = Goptions.declare_bool_option { Goptions.optwrite = (fun a -> debug_unification:=a); } +(*******************************************) +(* Functions to deal with impossible cases *) +(*******************************************) +(* XXX: we would like to search for this with late binding + "data.id.type" etc... *) +let impossible_default_case () = + let c, ctx = Universes.fresh_global_instance (Global.env()) (Globnames.ConstRef Coqlib.id) in + let (_, u) = Constr.destConst c in + Some (c, Constr.mkConstU (Coqlib.type_of_id, u), ctx) + +let coq_unit_judge = + let open Environ in + let make_judge c t = make_judge (EConstr.of_constr c) (EConstr.of_constr t) in + let na1 = Name (Id.of_string "A") in + let na2 = Name (Id.of_string "H") in + fun () -> + match impossible_default_case () with + | Some (id, type_of_id, ctx) -> + make_judge id type_of_id, ctx + | None -> + (* In case the constants id/ID are not defined *) + Environ.make_judge (mkLambda (na1,mkProp,mkLambda(na2,mkRel 1,mkRel 1))) + (mkProd (na1,mkProp,mkArrow (mkRel 1) (mkRel 2))), + Univ.ContextSet.empty + let unfold_projection env evd ts p c = let cst = Projection.constant p in if is_transparent_constant ts cst then @@ -46,21 +75,20 @@ let unfold_projection env evd ts p c = else None let eval_flexible_term ts env evd c = - match kind_of_term c with - | Const (c,u as cu) -> + match EConstr.kind evd c with + | Const (c, u) -> if is_transparent_constant ts c - then constant_opt_value_in env cu + then Option.map EConstr.of_constr (constant_opt_value_in env (c, EInstance.kind evd u)) else None | Rel n -> (try match lookup_rel n env with - | LocalAssum _ -> None - | LocalDef (_,v,_) -> Some (lift n v) + | RelDecl.LocalAssum _ -> None + | RelDecl.LocalDef (_,v,_) -> Some (lift n v) with Not_found -> None) | Var id -> (try if is_transparent_variable ts id then - let open Context.Named.Declaration in - lookup_named id env |> get_value + env |> lookup_named id |> NamedDecl.get_value else None with Not_found -> None) | LetIn (_,b,_,c) -> Some (subst1 b c) @@ -72,11 +100,11 @@ let eval_flexible_term ts env evd c = type flex_kind_of_term = | Rigid - | MaybeFlexible of Constr.t (* reducible but not necessarily reduced *) - | Flexible of existential + | MaybeFlexible of EConstr.t (* reducible but not necessarily reduced *) + | Flexible of EConstr.existential let flex_kind_of_term ts env evd c sk = - match kind_of_term c with + match EConstr.kind evd c with | LetIn _ | Rel _ | Const _ | Var _ | Proj _ -> Option.cata (fun x -> MaybeFlexible x) Rigid (eval_flexible_term ts env evd c) | Lambda _ when not (Option.is_empty (Stack.decomp sk)) -> MaybeFlexible c @@ -86,10 +114,13 @@ let flex_kind_of_term ts env evd c sk = | Fix _ -> Rigid (* happens when the fixpoint is partially applied *) | Cast _ | App _ | Case _ -> assert false +let add_conv_pb (pb, env, x, y) sigma = + Evd.add_conv_pb (pb, env, EConstr.Unsafe.to_constr x, EConstr.Unsafe.to_constr y) sigma + let apprec_nohdbeta ts env evd c = let (t,sk as appr) = Reductionops.whd_nored_state evd (c, []) in if Stack.not_purely_applicative sk - then Stack.zip (fst (whd_betaiota_deltazeta_for_iota_state + then Stack.zip evd (fst (whd_betaiota_deltazeta_for_iota_state ts env evd Cst_stack.empty appr)) else c @@ -99,7 +130,7 @@ let position_problem l2r = function let occur_rigidly (evk,_ as ev) evd t = let rec aux t = - match kind_of_term (whd_evar evd t) with + match EConstr.kind evd t with | App (f, c) -> if aux f then Array.exists aux c else false | Construct _ | Ind _ | Sort _ | Meta _ | Fix _ | CoFix _ -> true | Proj (p, c) -> not (aux c) @@ -109,7 +140,7 @@ let occur_rigidly (evk,_ as ev) evd t = | Const _ -> false | Prod (_, b, t) -> ignore(aux b || aux t); true | Rel _ | Var _ -> false - | Case (_,_,c,_) -> if eq_constr (mkEvar ev) c then raise Occur else false + | Case (_,_,c,_) -> if eq_constr evd (mkEvar ev) c then raise Occur else false in try ignore(aux t); false with Occur -> true (* [check_conv_record env sigma (t1,stack1) (t2,stack2)] tries to decompose @@ -133,20 +164,28 @@ let occur_rigidly (evk,_ as ev) evd t = projection would have been reduced) *) let check_conv_record env sigma (t1,sk1) (t2,sk2) = - let (proji, u), arg = Universes.global_app_of_constr t1 in + let (proji, u), arg = Termops.global_app_of_constr sigma t1 in let canon_s,sk2_effective = try - match kind_of_term t2 with + match EConstr.kind sigma t2 with Prod (_,a,b) -> (* assert (l2=[]); *) - let _, a, b = destProd (Evarutil.nf_evar sigma t2) in - if dependent (mkRel 1) b then raise Not_found - else lookup_canonical_conversion (proji, Prod_cs), + let _, a, b = destProd sigma t2 in + if noccurn sigma 1 b then + lookup_canonical_conversion (proji, Prod_cs), (Stack.append_app [|a;pop b|] Stack.empty) + else raise Not_found | Sort s -> + let s = ESorts.kind sigma s in lookup_canonical_conversion - (proji, Sort_cs (family_of_sort s)),[] + (proji, Sort_cs (Sorts.family s)),[] + | Proj (p, c) -> + let c2 = Globnames.ConstRef (Projection.constant p) in + let c = Retyping.expand_projection env sigma p c [] in + let _, args = destApp sigma c in + let sk2 = Stack.append_app args sk2 in + lookup_canonical_conversion (proji, Const_cs c2), sk2 | _ -> - let c2 = global_of_constr t2 in + let (c2, _) = Termops.global_of_constr sigma t2 in lookup_canonical_conversion (proji, Const_cs c2),sk2 with Not_found -> let (c, cs) = lookup_canonical_conversion (proji,Default_cs) in @@ -154,12 +193,14 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) = in let t', { o_DEF = c; o_CTX = ctx; o_INJ=n; o_TABS = bs; o_TPARAMS = params; o_NPARAMS = nparams; o_TCOMPS = us } = canon_s in + let us = List.map EConstr.of_constr us in + let params = List.map EConstr.of_constr params in let params1, c1, extra_args1 = match arg with | Some c -> (* A primitive projection applied to c *) let ty = Retyping.get_type_of ~lax:true env sigma c in let (i,u), ind_args = - try Inductiveops.find_mrectype env sigma ty + try Inductiveops.find_mrectype env sigma ty with _ -> raise Not_found in Stack.append_app_list ind_args Stack.empty, c, sk1 | None -> @@ -172,14 +213,19 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) = else match (Stack.strip_n_app (l_us-1) sk2_effective) with | None -> raise Not_found | Some (l',el,s') -> (l'@Stack.append_app [|el|] Stack.empty,s') in - let subst, ctx' = Universes.fresh_universe_context_set_instance ctx in + let u, ctx' = Universes.fresh_instance_from ctx None in + let subst = Univ.make_inverse_instance_subst u in + let c = EConstr.of_constr c in let c' = subst_univs_level_constr subst c in + let t' = EConstr.of_constr t' in let t' = subst_univs_level_constr subst t' in - let bs' = List.map (subst_univs_level_constr subst) bs in - let h, _ = decompose_app_vect t' in + let bs' = List.map (EConstr.of_constr %> subst_univs_level_constr subst) bs in + let params = List.map (fun c -> subst_univs_level_constr subst c) params in + let us = List.map (fun c -> subst_univs_level_constr subst c) us in + let h, _ = decompose_app_vect sigma t' in ctx',(h, t2),c',bs',(Stack.append_app_list params Stack.empty,params1), (Stack.append_app_list us Stack.empty,us2),(extra_args1,extra_args2),c1, - (n,Stack.zip(t2,sk2)) + (n, Stack.zip sigma (t2,sk2)) (* Precondition: one of the terms of the pb is an uninstantiated evar, * possibly applied to arguments. *) @@ -250,7 +296,7 @@ let ise_stack2 no_app env evd f sk1 sk2 = | UnifFailure _ as x -> fail x) | UnifFailure _ as x -> fail x) | Stack.Proj (n1,a1,p1,_)::q1, Stack.Proj (n2,a2,p2,_)::q2 -> - if eq_constant (Projection.constant p1) (Projection.constant p2) + if Constant.equal (Projection.constant p1) (Projection.constant p2) then ise_stack2 true i q1 q2 else fail (UnifFailure (i, NotSameHead)) | Stack.Fix (((li1, i1),(_,tys1,bds1 as recdef1)),a1,_)::q1, @@ -263,8 +309,6 @@ let ise_stack2 no_app env evd f sk1 sk2 = | Success i' -> ise_stack2 true i' q1 q2 | UnifFailure _ as x -> fail x else fail (UnifFailure (i,NotSameHead)) - | Stack.Update _ :: _, _ | Stack.Shift _ :: _, _ - | _, Stack.Update _ :: _ | _, Stack.Shift _ :: _ -> assert false | Stack.App _ :: _, Stack.App _ :: _ -> if no_app && deep then fail ((*dummy*)UnifFailure(i,NotSameHead)) else begin match ise_app_stack2 env f i sk1 sk2 with @@ -294,11 +338,9 @@ let exact_ise_stack2 env evd f sk1 sk2 = (fun i -> ise_stack2 i a1 a2)] else UnifFailure (i,NotSameHead) | Stack.Proj (n1,a1,p1,_)::q1, Stack.Proj (n2,a2,p2,_)::q2 -> - if eq_constant (Projection.constant p1) (Projection.constant p2) + if Constant.equal (Projection.constant p1) (Projection.constant p2) then ise_stack2 i q1 q2 else (UnifFailure (i, NotSameHead)) - | Stack.Update _ :: _, _ | Stack.Shift _ :: _, _ - | _, Stack.Update _ :: _ | _, Stack.Shift _ :: _ -> assert false | Stack.App _ :: _, Stack.App _ :: _ -> begin match ise_app_stack2 env f i sk1 sk2 with |_,(UnifFailure _ as x) -> x @@ -310,6 +352,14 @@ let exact_ise_stack2 env evd f sk1 sk2 = ise_stack2 evd (List.rev sk1) (List.rev sk2) else UnifFailure (evd, (* Dummy *) NotSameHead) +(* Add equality constraints for covariant/invariant positions. For + irrelevant positions, unify universes when flexible. *) +let compare_cumulative_instances evd variances u u' = + match Evarutil.compare_cumulative_instances CONV variances u u' evd with + | Inl evd -> + Success evd + | Inr p -> UnifFailure (evd, UnifUnivInconsistency p) + let rec evar_conv_x ts env evd pbty term1 term2 = let term1 = whd_head_evar evd term1 in let term2 = whd_head_evar evd term2 in @@ -321,7 +371,7 @@ let rec evar_conv_x ts env evd pbty term1 term2 = let e = try let evd, b = infer_conv ~catch_incon:false ~pb:pbty ~ts:(fst ts) - env evd term1 term2 + env evd term1 term2 in if b then Success evd else UnifFailure (evd, ConversionFailed (env,term1,term2)) @@ -335,7 +385,7 @@ let rec evar_conv_x ts env evd pbty term1 term2 = match ground_test with | Some result -> result | None -> - (* Until pattern-unification is used consistently, use nohdbeta to not + (* Until pattern-unification is used consistently, use nohdbeta to not destroy beta-redexes that can be used for 1st-order unification *) let term1 = apprec_nohdbeta (fst ts) env evd term1 in let term2 = apprec_nohdbeta (fst ts) env evd term2 in @@ -344,16 +394,16 @@ let rec evar_conv_x ts env evd pbty term1 term2 = (whd_nored_state evd (term1,Stack.empty), Cst_stack.empty) (whd_nored_state evd (term2,Stack.empty), Cst_stack.empty) in - begin match kind_of_term term1, kind_of_term term2 with + begin match EConstr.kind evd term1, EConstr.kind evd term2 with | Evar ev, _ when Evd.is_undefined evd (fst ev) -> (match solve_simple_eqn (evar_conv_x ts) env evd - (position_problem true pbty,ev,term2) with + (position_problem true pbty,ev, term2) with | UnifFailure (_,OccurCheck _) -> (* Eta-expansion might apply *) default () | x -> x) | _, Evar ev when Evd.is_undefined evd (fst ev) -> (match solve_simple_eqn (evar_conv_x ts) env evd - (position_problem false pbty,ev,term1) with + (position_problem false pbty,ev, term1) with | UnifFailure (_, OccurCheck _) -> (* Eta-expansion might apply *) default () | x -> x) @@ -369,8 +419,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty match is_unification_pattern_evar env evd ev lF tM with | None -> fallback () | Some l1' -> (* Miller-Pfenning's patterns unification *) - let t2 = nf_evar evd tM in - let t2 = solve_pattern_eqn env l1' t2 in + let t2 = tM in + let t2 = solve_pattern_eqn env evd l1' t2 in solve_simple_eqn (evar_conv_x ts) env evd (position_problem on_left pbty,ev,t2) in @@ -379,34 +429,82 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty let not_only_app = Stack.not_purely_applicative skO in match switch (ise_stack2 not_only_app env evd (evar_conv_x ts)) skF skO with |Some (l,r), Success i' when on_left && (not_only_app || List.is_empty l) -> - switch (evar_conv_x ts env i' pbty) (Stack.zip(termF,l)) (Stack.zip(termO,r)) + switch (evar_conv_x ts env i' pbty) (Stack.zip evd (termF,l)) (Stack.zip evd (termO,r)) |Some (r,l), Success i' when not on_left && (not_only_app || List.is_empty l) -> - switch (evar_conv_x ts env i' pbty) (Stack.zip(termF,l)) (Stack.zip(termO,r)) + switch (evar_conv_x ts env i' pbty) (Stack.zip evd (termF,l)) (Stack.zip evd (termO,r)) |None, Success i' -> switch (evar_conv_x ts env i' pbty) termF termO |_, (UnifFailure _ as x) -> x |Some _, _ -> UnifFailure (evd,NotSameArgSize) in let eta env evd onleft sk term sk' term' = assert (match sk with [] -> true | _ -> false); - let (na,c1,c'1) = destLambda term in + let (na,c1,c'1) = destLambda evd term in let c = nf_evar evd c1 in - let env' = push_rel (LocalAssum (na,c)) env in + let env' = push_rel (RelDecl.LocalAssum (na,c)) env in let out1 = whd_betaiota_deltazeta_for_iota_state (fst ts) env' evd Cst_stack.empty (c'1, Stack.empty) in let out2 = whd_nored_state evd - (Stack.zip (term', sk' @ [Stack.Shift 1]), Stack.append_app [|mkRel 1|] Stack.empty), + (lift 1 (Stack.zip evd (term', sk')), Stack.append_app [|EConstr.mkRel 1|] Stack.empty), Cst_stack.empty in if onleft then evar_eqappr_x ts env' evd CONV out1 out2 else evar_eqappr_x ts env' evd CONV out2 out1 in let rigids env evd sk term sk' term' = - let b,univs = Universes.eq_constr_universes term term' in - if b then - ise_and evd [(fun i -> - let cstrs = Universes.to_constraints (Evd.universes i) univs in - try Success (Evd.add_constraints i cstrs) - with Univ.UniverseInconsistency p -> UnifFailure (i, UnifUnivInconsistency p)); - (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk sk')] - else UnifFailure (evd,NotSameHead) + let check_strict evd u u' = + let cstrs = Univ.enforce_eq_instances u u' Univ.Constraint.empty in + try Success (Evd.add_constraints evd cstrs) + with Univ.UniverseInconsistency p -> UnifFailure (evd, UnifUnivInconsistency p) + in + let compare_heads evd = + match EConstr.kind evd term, EConstr.kind evd term' with + | Const (c, u), Const (c', u') when Constant.equal c c' -> + let u = EInstance.kind evd u and u' = EInstance.kind evd u' in + check_strict evd u u' + | Const _, Const _ -> UnifFailure (evd, NotSameHead) + | Ind ((mi,i) as ind , u), Ind (ind', u') when Names.eq_ind ind ind' -> + if EInstance.is_empty u && EInstance.is_empty u' then Success evd + else + let u = EInstance.kind evd u and u' = EInstance.kind evd u' in + let mind = Environ.lookup_mind mi env in + let open Declarations in + begin match mind.mind_universes with + | Monomorphic_ind _ -> assert false + | Polymorphic_ind _ -> check_strict evd u u' + | Cumulative_ind cumi -> + let nparamsaplied = Stack.args_size sk in + let nparamsaplied' = Stack.args_size sk' in + let needed = Reduction.inductive_cumulativity_arguments (mind,i) in + if not (Int.equal nparamsaplied needed && Int.equal nparamsaplied' needed) + then check_strict evd u u' + else + compare_cumulative_instances evd (Univ.ACumulativityInfo.variance cumi) u u' + end + | Ind _, Ind _ -> UnifFailure (evd, NotSameHead) + | Construct (((mi,ind),ctor as cons), u), Construct (cons', u') + when Names.eq_constructor cons cons' -> + if EInstance.is_empty u && EInstance.is_empty u' then Success evd + else + let u = EInstance.kind evd u and u' = EInstance.kind evd u' in + let mind = Environ.lookup_mind mi env in + let open Declarations in + begin match mind.mind_universes with + | Monomorphic_ind _ -> assert false + | Polymorphic_ind _ -> check_strict evd u u' + | Cumulative_ind cumi -> + let nparamsaplied = Stack.args_size sk in + let nparamsaplied' = Stack.args_size sk' in + let needed = Reduction.constructor_cumulativity_arguments (mind,ind,ctor) in + if not (Int.equal nparamsaplied needed && Int.equal nparamsaplied' needed) + then check_strict evd u u' + else + Success (compare_constructor_instances evd u u') + end + | Construct _, Construct _ -> UnifFailure (evd, NotSameHead) + | _, _ -> anomaly (Pp.str "") + in + ise_and evd [(fun i -> + try compare_heads i + with Univ.UniverseInconsistency p -> UnifFailure (i, UnifUnivInconsistency p)); + (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk sk')] in let flex_maybeflex on_left ev ((termF,skF as apprF),cstsF) ((termM, skM as apprM),cstsM) vM = let switch f a b = if on_left then f a b else f b a in @@ -415,10 +513,10 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty match Stack.list_of_app_stack skF with | None -> quick_fail evd | Some lF -> - let tM = Stack.zip apprM in + let tM = Stack.zip evd apprM in miller_pfenning on_left (fun () -> if not_only_app then (* Postpone the use of an heuristic *) - switch (fun x y -> Success (add_conv_pb (pbty,env,x,y) i)) (Stack.zip apprF) tM + switch (fun x y -> Success (add_conv_pb (pbty,env,x,y) i)) (Stack.zip evd apprF) tM else quick_fail i) ev lF tM i and consume (termF,skF as apprF) (termM,skM as apprM) i = @@ -432,7 +530,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty in let default i = ise_try i [f1; consume apprF apprM; delta] in - match kind_of_term termM with + match EConstr.kind evd termM with | Proj (p, c) when not (Stack.is_empty skF) -> (* Might be ?X args = p.c args', and we have to eta-expand the primitive projection if |args| >= |args'|+1. *) @@ -462,7 +560,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty let flex_rigid on_left ev (termF, skF as apprF) (termR, skR as apprR) = let switch f a b = if on_left then f a b else f b a in let eta evd = - match kind_of_term termR with + match EConstr.kind evd termR with | Lambda _ when (* if ever problem is ill-typed: *) List.is_empty skR -> eta env evd false skR termR skF termF | Construct u -> eta_constructor ts env evd skR u skF termF @@ -472,7 +570,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty | None -> ise_try evd [consume_stack on_left apprF apprR; eta] | Some lF -> - let tR = Stack.zip apprR in + let tR = Stack.zip evd apprR in miller_pfenning on_left (fun () -> ise_try evd @@ -480,12 +578,12 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty (fun i -> if not (occur_rigidly ev i tR) then let i,tF = - if isRel tR || isVar tR then + if isRel i tR || isVar i tR then (* Optimization so as to generate candidates *) let i,ev = evar_absorb_arguments env i ev lF in i,mkEvar ev else - i,Stack.zip apprF in + i,Stack.zip evd apprF in switch (fun x y -> Success (add_conv_pb (pbty,env,x,y) i)) tF tR else @@ -496,8 +594,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty (* Evar must be undefined since we have flushed evars *) let () = if !debug_unification then let open Pp in - Feedback.msg_notice (v 0 (pr_state appr1 ++ cut () ++ pr_state appr2 ++ cut ()) - ++ fnl ()) in + Feedback.msg_notice (v 0 (pr_state appr1 ++ cut () ++ pr_state appr2 ++ cut ())) in match (flex_kind_of_term (fst ts) env evd term1 sk1, flex_kind_of_term (fst ts) env evd term2 sk2) with | Flexible (sp1,al1 as ev1), Flexible (sp2,al2 as ev2) -> @@ -509,9 +606,9 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty (* We do have sk1[] = sk2[]: we now unify ?ev1 and ?ev2 *) (* Note that ?ev1 and ?ev2, may have been instantiated in the meantime *) let ev1' = whd_evar i' (mkEvar ev1) in - if isEvar ev1' then + if isEvar i' ev1' then solve_simple_eqn (evar_conv_x ts) env i' - (position_problem true pbty,destEvar ev1',term2) + (position_problem true pbty,destEvar i' ev1', term2) else evar_eqappr_x ts env evd pbty ((ev1', sk1), csts1) ((term2, sk2), csts2) @@ -519,9 +616,9 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty (* We have sk1'[] = sk2[] for some sk1' s.t. sk1[]=sk1'[r[]] *) (* we now unify r[?ev1] and ?ev2 *) let ev2' = whd_evar i' (mkEvar ev2) in - if isEvar ev2' then + if isEvar i' ev2' then solve_simple_eqn (evar_conv_x ts) env i' - (position_problem false pbty,destEvar ev2',Stack.zip(term1,r)) + (position_problem false pbty,destEvar i' ev2',Stack.zip evd (term1,r)) else evar_eqappr_x ts env evd pbty ((ev2', sk1), csts1) ((term2, sk2), csts2) @@ -530,9 +627,9 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty (* We have sk1[] = sk2'[] for some sk2' s.t. sk2[]=sk2'[r[]] *) (* we now unify ?ev1 and r[?ev2] *) let ev1' = whd_evar i' (mkEvar ev1) in - if isEvar ev1' then + if isEvar i' ev1' then solve_simple_eqn (evar_conv_x ts) env i' - (position_problem true pbty,destEvar ev1',Stack.zip(term2,r)) + (position_problem true pbty,destEvar i' ev1',Stack.zip evd (term2,r)) else evar_eqappr_x ts env evd pbty ((ev1', sk1), csts1) ((term2, sk2), csts2) | None, (UnifFailure _ as x) -> @@ -585,7 +682,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty flex_maybeflex false ev2 (appr2,csts2) (appr1,csts1) v1 | MaybeFlexible v1, MaybeFlexible v2 -> begin - match kind_of_term term1, kind_of_term term2 with + match EConstr.kind evd term1, EConstr.kind evd term2 with | LetIn (na1,b1,t1,c'1), LetIn (na2,b2,t2,c'2) -> let f1 i = (* FO *) ise_and i @@ -596,8 +693,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty (fun i -> let b = nf_evar i b1 in let t = nf_evar i t1 in - let na = Nameops.name_max na1 na2 in - evar_conv_x ts (push_rel (LocalDef (na,b,t)) env) i pbty c'1 c'2); + let na = Nameops.Name.pick na1 na2 in + evar_conv_x ts (push_rel (RelDecl.LocalDef (na,b,t)) env) i pbty c'1 c'2); (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)] and f2 i = let out1 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts1 (v1,sk1) @@ -620,9 +717,9 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty ise_try evd [f1; f2] (* Catch the p.c ~= p c' cases *) - | Proj (p,c), Const (p',u) when eq_constant (Projection.constant p) p' -> + | Proj (p,c), Const (p',u) when Constant.equal (Projection.constant p) p' -> let res = - try Some (destApp (Retyping.expand_projection env evd p c [])) + try Some (destApp evd (Retyping.expand_projection env evd p c [])) with Retyping.RetypeError _ -> None in (match res with @@ -631,9 +728,9 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty (appr2,csts2) | None -> UnifFailure (evd,NotSameHead)) - | Const (p,u), Proj (p',c') when eq_constant p (Projection.constant p') -> + | Const (p,u), Proj (p',c') when Constant.equal p (Projection.constant p') -> let res = - try Some (destApp (Retyping.expand_projection env evd p' c' [])) + try Some (destApp evd (Retyping.expand_projection env evd p' c' [])) with Retyping.RetypeError _ -> None in (match res with @@ -648,14 +745,16 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty allow this identification (first-order unification of universes). Otherwise fallback to unfolding. *) - let b,univs = Universes.eq_constr_universes term1 term2 in - if b then + let univs = EConstr.eq_constr_universes env evd term1 term2 in + match univs with + | Some univs -> ise_and i [(fun i -> try Success (Evd.add_universe_constraints i univs) with UniversesDiffer -> UnifFailure (i,NotSameHead) | Univ.UniverseInconsistency p -> UnifFailure (i, UnifUnivInconsistency p)); (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)] - else UnifFailure (i,NotSameHead) + | None -> + UnifFailure (i,NotSameHead) and f2 i = (try if not (snd ts) then raise Not_found @@ -668,7 +767,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty if the first argument is a beta-redex (expand a constant only if necessary) or the second argument is potentially usable as a canonical projection or canonical value *) - let rec is_unnamed (hd, args) = match kind_of_term hd with + let rec is_unnamed (hd, args) = match EConstr.kind i hd with | (Var _|Construct _|Ind _|Const _|Prod _|Sort _) -> Stack.not_purely_applicative args | (CoFix _|Meta _|Rel _)-> true @@ -689,7 +788,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty let rhs_is_already_stuck = rhs_is_already_stuck || rhs_is_stuck_and_unnamed () in - if (isLambda term1 || rhs_is_already_stuck) + if (EConstr.isLambda i term1 || rhs_is_already_stuck) && (not (Stack.not_purely_applicative sk1)) then evar_eqappr_x ~rhs_is_already_stuck ts env i pbty (whd_betaiota_deltazeta_for_iota_state @@ -703,16 +802,16 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty ise_try evd [f1; f2; f3] end - | Rigid, Rigid when isLambda term1 && isLambda term2 -> - let (na1,c1,c'1) = destLambda term1 in - let (na2,c2,c'2) = destLambda term2 in + | Rigid, Rigid when EConstr.isLambda evd term1 && EConstr.isLambda evd term2 -> + let (na1,c1,c'1) = EConstr.destLambda evd term1 in + let (na2,c2,c'2) = EConstr.destLambda evd term2 in assert app_empty; ise_and evd [(fun i -> evar_conv_x ts env i CONV c1 c2); (fun i -> let c = nf_evar i c1 in - let na = Nameops.name_max na1 na2 in - evar_conv_x ts (push_rel (LocalAssum (na,c)) env) i CONV c'1 c'2)] + let na = Nameops.Name.pick na1 na2 in + evar_conv_x ts (push_rel (RelDecl.LocalAssum (na,c)) env) i CONV c'1 c'2)] | Flexible ev1, Rigid -> flex_rigid true ev1 appr1 appr2 | Rigid, Flexible ev2 -> flex_rigid false ev2 appr2 appr1 @@ -745,17 +844,19 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty ise_try evd [f3; f4] (* Eta-expansion *) - | Rigid, _ when isLambda term1 && (* if ever ill-typed: *) List.is_empty sk1 -> + | Rigid, _ when isLambda evd term1 && (* if ever ill-typed: *) List.is_empty sk1 -> eta env evd true sk1 term1 sk2 term2 - | _, Rigid when isLambda term2 && (* if ever ill-typed: *) List.is_empty sk2 -> + | _, Rigid when isLambda evd term2 && (* if ever ill-typed: *) List.is_empty sk2 -> eta env evd false sk2 term2 sk1 term1 | Rigid, Rigid -> begin - match kind_of_term term1, kind_of_term term2 with + match EConstr.kind evd term1, EConstr.kind evd term2 with | Sort s1, Sort s2 when app_empty -> (try + let s1 = ESorts.kind evd s1 in + let s2 = ESorts.kind evd s2 in let evd' = if pbty == CONV then Evd.set_eq_sort env evd s1 s2 @@ -770,8 +871,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty [(fun i -> evar_conv_x ts env i CONV c1 c2); (fun i -> let c = nf_evar i c1 in - let na = Nameops.name_max n1 n2 in - evar_conv_x ts (push_rel (LocalAssum (na,c)) env) i pbty c'1 c'2)] + let na = Nameops.Name.pick n1 n2 in + evar_conv_x ts (push_rel (RelDecl.LocalAssum (na,c)) env) i pbty c'1 c'2)] | Rel x1, Rel x2 -> if Int.equal x1 x2 then @@ -818,7 +919,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty begin match ise_stack2 true env evd (evar_conv_x ts) sk1 sk2 with |_, (UnifFailure _ as x) -> x |None, Success i' -> evar_conv_x ts env i' CONV term1 term2 - |Some (sk1',sk2'), Success i' -> evar_conv_x ts env i' CONV (Stack.zip (term1,sk1')) (Stack.zip (term2,sk2')) + |Some (sk1',sk2'), Success i' -> evar_conv_x ts env i' CONV (Stack.zip i' (term1,sk1')) (Stack.zip i' (term2,sk2')) end | (Ind _ | Sort _ | Prod _ | CoFix _ | Fix _ | Rel _ | Var _ | Const _), _ -> @@ -866,10 +967,8 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2) let test i = evar_conv_x trs env i CUMUL ty (substl ks b) in (i,t2::ks, m-1, test) else - let dloc = (Loc.ghost,Evar_kinds.InternalHole) in - let i = Sigma.Unsafe.of_evar_map i in - let Sigma (ev, i', _) = Evarutil.new_evar env i ~src:dloc (substl ks b) in - let i' = Sigma.to_evar_map i' in + let dloc = Loc.tag Evar_kinds.InternalHole in + let (i', ev) = Evarutil.new_evar env i ~src:dloc (substl ks b) in (i', ev :: ks, m - 1,test)) (evd,[],List.length bs,fun i -> Success i) bs in @@ -887,19 +986,19 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2) (fun i -> exact_ise_stack2 env i (evar_conv_x trs) sk1 sk2); test; (fun i -> evar_conv_x trs env i CONV h2 - (fst (decompose_app_vect (substl ks h))))] + (fst (decompose_app_vect i (substl ks h))))] else UnifFailure(evd,(*dummy*)NotSameHead) and eta_constructor ts env evd sk1 ((ind, i), u) sk2 term2 = let mib = lookup_mind (fst ind) env in match mib.Declarations.mind_record with - | Some (Some (id, projs, pbs)) when mib.Declarations.mind_finite == Decl_kinds.BiFinite -> + | Some (Some (id, projs, pbs)) when mib.Declarations.mind_finite == Declarations.BiFinite -> let pars = mib.Declarations.mind_nparams in (try let l1' = Stack.tail pars sk1 in let l2' = - let term = Stack.zip (term2,sk2) in - List.map (fun p -> mkProj (Projection.make p false, term)) (Array.to_list projs) + let term = Stack.zip evd (term2,sk2) in + List.map (fun p -> EConstr.mkProj (Projection.make p false, term)) (Array.to_list projs) in exact_ise_stack2 env evd (evar_conv_x (fst ts, false)) l1' (Stack.append_app_list l2' Stack.empty) @@ -914,8 +1013,8 @@ let evar_conv_x ts = evar_conv_x (ts, true) (* Profiling *) let evar_conv_x = if Flags.profile then - let evar_conv_xkey = Profile.declare_profile "evar_conv_x" in - Profile.profile6 evar_conv_xkey evar_conv_x + let evar_conv_xkey = CProfile.declare_profile "evar_conv_x" in + CProfile.profile6 evar_conv_xkey evar_conv_x else evar_conv_x let evar_conv_hook_get, evar_conv_hook_set = Hook.make ~default:evar_conv_x () @@ -943,50 +1042,57 @@ let first_order_unification ts env evd (ev1,l1) (term2,l2) = let choose_less_dependent_instance evk evd term args = let evi = Evd.find_undefined evd evk in let subst = make_pure_subst evi args in - let subst' = List.filter (fun (id,c) -> Term.eq_constr c term) subst in + let subst' = List.filter (fun (id,c) -> EConstr.eq_constr evd c term) subst in match subst' with | [] -> None - | (id, _) :: _ -> Some (Evd.define evk (mkVar id) evd) + | (id, _) :: _ -> Some (Evd.define evk (Constr.mkVar id) evd) -open Context.Named.Declaration let apply_on_subterm env evdref f c t = let rec applyrec (env,(k,c) as acc) t = (* By using eq_constr, we make an approximation, for instance, we *) (* could also be interested in finding a term u convertible to t *) (* such that c occurs in u *) - if e_eq_constr_univs evdref c t then f k + let eq_constr c1 c2 = match EConstr.eq_constr_universes env !evdref c1 c2 with + | None -> false + | Some cstr -> + try ignore (Evd.add_universe_constraints !evdref cstr); true + with UniversesDiffer -> false + in + if eq_constr c t then f k else - match kind_of_term t with - | Evar (evk,args) when Evd.is_undefined !evdref evk -> + match EConstr.kind !evdref t with + | Evar (evk,args) -> let ctx = evar_filtered_context (Evd.find_undefined !evdref evk) in let g decl a = if is_local_assum decl then applyrec acc a else a in mkEvar (evk, Array.of_list (List.map2 g ctx (Array.to_list args))) | _ -> - map_constr_with_binders_left_to_right + map_constr_with_binders_left_to_right !evdref (fun d (env,(k,c)) -> (push_rel d env, (k+1,lift 1 c))) applyrec acc t in applyrec (env,(0,c)) t -let filter_possible_projections c ty ctxt args = +let filter_possible_projections evd c ty ctxt args = (* Since args in the types will be replaced by holes, we count the fv of args to have a well-typed filter; don't know how necessary - it is however to have a well-typed filter here *) - let fv1 = free_rels (mkApp (c,args)) (* Hack: locally untyped *) in - let fv2 = collect_vars (mkApp (c,args)) in + it is however to have a well-typed filter here *) + let fv1 = free_rels evd (mkApp (c,args)) (* Hack: locally untyped *) in + let fv2 = collect_vars evd (mkApp (c,args)) in let len = Array.length args in - let tyvars = collect_vars ty in + let tyvars = collect_vars evd ty in List.map_i (fun i decl -> let () = assert (i < len) in let a = Array.unsafe_get args i in - (match decl with LocalAssum _ -> false | LocalDef (_,c,_) -> not (isRel c || isVar c)) || + (match decl with + | NamedDecl.LocalAssum _ -> false + | NamedDecl.LocalDef (_,c,_) -> not (isRel evd (EConstr.of_constr c) || isVar evd (EConstr.of_constr c))) || a == c || (* Here we make an approximation, for instance, we could also be *) (* interested in finding a term u convertible to c such that a occurs *) (* in u *) - isRel a && Int.Set.mem (destRel a) fv1 || - isVar a && Id.Set.mem (destVar a) fv2 || - Id.Set.mem (get_id decl) tyvars) + isRel evd a && Int.Set.mem (destRel evd a) fv1 || + isVar evd a && Id.Set.mem (destVar evd a) fv2 || + Id.Set.mem (NamedDecl.get_id decl) tyvars) 0 ctxt let solve_evars = ref (fun _ -> failwith "solve_evars not installed") @@ -1017,39 +1123,39 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = let env_evar = evar_filtered_env evi in let sign = named_context_val env_evar in let ctxt = evar_filtered_context evi in - let instance = List.map mkVar (List.map get_id ctxt) in + let instance = List.map mkVar (List.map NamedDecl.get_id ctxt) in let rec make_subst = function - | decl'::ctxt', c::l, occs::occsl when isVarId (get_id decl') c -> + | decl'::ctxt', c::l, occs::occsl when isVarId evd (NamedDecl.get_id decl') c -> begin match occs with | Some _ -> - error "Cannot force abstraction on identity instance." + user_err Pp.(str "Cannot force abstraction on identity instance.") | None -> make_subst (ctxt',l,occsl) end | decl'::ctxt', c::l, occs::occsl -> - let (id,_,t) = to_tuple decl' in + let id = NamedDecl.get_id decl' in + let t = EConstr.of_constr (NamedDecl.get_type decl') in let evs = ref [] in let ty = Retyping.get_type_of env_rhs evd c in - let filter' = filter_possible_projections c ty ctxt args in + let filter' = filter_possible_projections evd c ty ctxt args in (id,t,c,ty,evs,Filter.make filter',occs) :: make_subst (ctxt',l,occsl) | _, _, [] -> [] - | _ -> anomaly (Pp.str "Signature or instance are shorter than the occurrences list") in + | _ -> anomaly (Pp.str "Signature or instance are shorter than the occurrences list.") in let rec set_holes evdref rhs = function | (id,_,c,cty,evsref,filter,occs)::subst -> let set_var k = match occs with | Some Locus.AllOccurrences -> mkVar id - | Some _ -> error "Selection of specific occurrences not supported" + | Some _ -> user_err Pp.(str "Selection of specific occurrences not supported") | None -> let evty = set_holes evdref cty subst in let instance = Filter.filter_list filter instance in - let evd = Sigma.Unsafe.of_evar_map !evdref in - let Sigma (ev, evd, _) = new_evar_instance sign evd evty ~filter instance in - let evd = Sigma.to_evar_map evd in + let evd = !evdref in + let (evd, ev) = new_evar_instance sign evd evty ~filter instance in evdref := evd; - evsref := (fst (destEvar ev),evty)::!evsref; + evsref := (fst (destEvar !evdref ev),evty)::!evsref; ev in set_holes evdref (apply_on_subterm env_rhs evdref set_var c rhs) subst | [] -> rhs in @@ -1077,12 +1183,12 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = (* We force abstraction over this unconstrained occurrence *) (* and we use typing to propagate this instantiation *) (* This is an arbitrary choice *) - let evd = Evd.define evk (mkVar id) evd in + let evd = Evd.define evk (Constr.mkVar id) evd in match evar_conv_x ts env_evar evd CUMUL idty evty with - | UnifFailure _ -> error "Cannot find an instance" + | UnifFailure _ -> user_err Pp.(str "Cannot find an instance") | Success evd -> match reconsider_unif_constraints (evar_conv_x ts) evd with - | UnifFailure _ -> error "Cannot find an instance" + | UnifFailure _ -> user_err Pp.(str "Cannot find an instance") | Success evd -> evd else @@ -1095,15 +1201,18 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = force_instantiation evd !evsref | [] -> let evd = - try Evarsolve.check_evar_instance evd evk rhs + try Evarsolve.check_evar_instance evd evk rhs (evar_conv_x full_transparent_state) with IllTypedInstance _ -> raise (TypingFailed evd) in - Evd.define evk rhs evd + Evd.define evk (EConstr.Unsafe.to_constr rhs) evd in abstract_free_holes evd subst, true with TypingFailed evd -> evd, false +let to_pb (pb, env, t1, t2) = + (pb, env, EConstr.Unsafe.to_constr t1, EConstr.Unsafe.to_constr t2) + let second_order_matching_with_args ts env evd pbty ev l t = (* let evd,ev = evar_absorb_arguments env evd ev l in @@ -1113,18 +1222,22 @@ let second_order_matching_with_args ts env evd pbty ev l t = else UnifFailure (evd, ConversionFailed (env,mkApp(mkEvar ev,l),t)) if b then Success evd else *) - let pb = (pbty,env,mkApp(mkEvar ev,l),t) in + let pb = to_pb (pbty,env,mkApp(mkEvar ev,l),t) in UnifFailure (evd, CannotSolveConstraint (pb,ProblemBeyondCapabilities)) let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = let t1 = apprec_nohdbeta ts env evd (whd_head_evar evd t1) in let t2 = apprec_nohdbeta ts env evd (whd_head_evar evd t2) in - let (term1,l1 as appr1) = try destApp t1 with DestKO -> (t1, [||]) in - let (term2,l2 as appr2) = try destApp t2 with DestKO -> (t2, [||]) in + let (term1,l1 as appr1) = try destApp evd t1 with DestKO -> (t1, [||]) in + let (term2,l2 as appr2) = try destApp evd t2 with DestKO -> (t2, [||]) in + let () = if !debug_unification then + let open Pp in + Feedback.msg_notice (v 0 (str "Heuristic:" ++ spc () ++ print_constr t1 + ++ cut () ++ print_constr t2 ++ cut ())) in let app_empty = Array.is_empty l1 && Array.is_empty l2 in - match kind_of_term term1, kind_of_term term2 with + match EConstr.kind evd term1, EConstr.kind evd term2 with | Evar (evk1,args1), (Rel _|Var _) when app_empty - && List.for_all (fun a -> Term.eq_constr a term2 || isEvar a) + && List.for_all (fun a -> EConstr.eq_constr evd a term2 || isEvar evd a) (remove_instance_local_defs evd evk1 args1) -> (* The typical kind of constraint coming from pattern-matching return type inference *) @@ -1132,9 +1245,9 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = | Some evd -> Success evd | None -> let reason = ProblemBeyondCapabilities in - UnifFailure (evd, CannotSolveConstraint ((pbty,env,t1,t2),reason))) + UnifFailure (evd, CannotSolveConstraint (to_pb (pbty,env,t1,t2),reason))) | (Rel _|Var _), Evar (evk2,args2) when app_empty - && List.for_all (fun a -> Term.eq_constr a term1 || isEvar a) + && List.for_all (fun a -> EConstr.eq_constr evd a term1 || isEvar evd a) (remove_instance_local_defs evd evk2 args2) -> (* The typical kind of constraint coming from pattern-matching return type inference *) @@ -1142,7 +1255,7 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = | Some evd -> Success evd | None -> let reason = ProblemBeyondCapabilities in - UnifFailure (evd, CannotSolveConstraint ((pbty,env,t1,t2),reason))) + UnifFailure (evd, CannotSolveConstraint (to_pb (pbty,env,t1,t2),reason))) | Evar (evk1,args1), Evar (evk2,args2) when Evar.equal evk1 evk2 -> let f env evd pbty x y = is_fconv ~reds:ts pbty env evd x y in Success (solve_refl ~can_drop:true f env evd @@ -1176,29 +1289,31 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = evar_conv_x ts env evd pbty t1 t2 let error_cannot_unify env evd pb ?reason t1 t2 = - Pretype_errors.error_cannot_unify_loc - (loc_of_conv_pb evd pb) env + Pretype_errors.error_cannot_unify + ?loc:(loc_of_conv_pb evd pb) env evd ?reason (t1, t2) let check_problems_are_solved env evd = match snd (extract_all_conv_pbs evd) with - | (pbty,env,t1,t2) as pb::_ -> error_cannot_unify env evd pb t1 t2 + | (pbty,env,t1,t2) as pb::_ -> error_cannot_unify env evd pb (EConstr.of_constr t1) (EConstr.of_constr t2) | _ -> () +exception MaxUndefined of (Evar.t * evar_info * Constr.t list) + let max_undefined_with_candidates evd = - (* If evar were ordered with highest index first, fold_undefined - would be going decreasingly and we could use fold_undefined to - find the undefined evar of maximum index (alternatively, - max_bindings from ocaml 3.12 could be used); instead we traverse - the whole map *) - let l = Evd.fold_undefined - (fun evk ev_info evars -> - match ev_info.evar_candidates with - | None -> evars - | Some l -> (evk,ev_info,l)::evars) evd [] in - match l with - | [] -> None - | a::l -> Some (List.last (a::l)) + let fold evk evi () = match evi.evar_candidates with + | None -> () + | Some l -> raise (MaxUndefined (evk, evi, l)) + in + (** [fold_right] traverses the undefined map in decreasing order of indices. + The evar with candidates of maximum index is thus the first evar with + candidates found by a [fold_right] traversal. This has a significant impact on + performance. *) + try + let () = Evar.Map.fold_right fold (Evd.undefined_map evd) () in + None + with MaxUndefined ans -> + Some ans let rec solve_unconstrained_evars_with_candidates ts evd = (* max_undefined is supposed to return the most recent, hence @@ -1207,11 +1322,11 @@ let rec solve_unconstrained_evars_with_candidates ts evd = | None -> evd | Some (evk,ev_info,l) -> let rec aux = function - | [] -> error "Unsolvable existential variables." + | [] -> user_err Pp.(str "Unsolvable existential variables.") | a::l -> try let conv_algo = evar_conv_x ts in - let evd = check_evar_instance evd evk a conv_algo in + let evd = check_evar_instance evd evk (EConstr.of_constr a) conv_algo in let evd = Evd.define evk a evd in match reconsider_unif_constraints conv_algo evd with | Success evd -> solve_unconstrained_evars_with_candidates ts evd @@ -1229,11 +1344,11 @@ let solve_unconstrained_impossible_cases env evd = match ev_info.evar_source with | loc,Evar_kinds.ImpossibleCase -> let j, ctx = coq_unit_judge () in - let evd' = Evd.merge_context_set Evd.univ_flexible_alg ~loc evd' ctx in + let evd' = Evd.merge_context_set Evd.univ_flexible_alg ?loc evd' ctx in let ty = j_type j in let conv_algo = evar_conv_x full_transparent_state in let evd' = check_evar_instance evd' evk ty conv_algo in - Evd.define evk ty evd' + Evd.define evk (EConstr.Unsafe.to_constr ty) evd' | _ -> evd') evd evd let solve_unif_constraints_with_heuristics env @@ -1242,6 +1357,8 @@ let solve_unif_constraints_with_heuristics env let rec aux evd pbs progress stuck = match pbs with | (pbty,env,t1,t2 as pb) :: pbs -> + let t1 = EConstr.of_constr t1 in + let t2 = EConstr.of_constr t2 in (match apply_conversion_problem_heuristic ts env evd pbty t1 t2 with | Success evd' -> let (evd', rest) = extract_all_conv_pbs evd' in @@ -1258,6 +1375,8 @@ let solve_unif_constraints_with_heuristics env match stuck with | [] -> (* We're finished *) evd | (pbty,env,t1,t2 as pb) :: _ -> + let t1 = EConstr.of_constr t1 in + let t2 = EConstr.of_constr t2 in (* There remains stuck problems *) error_cannot_unify env evd pb t1 t2 in -- cgit v1.2.3