diff options
Diffstat (limited to 'pretyping/unification.ml')
| -rw-r--r-- | pretyping/unification.ml | 214 |
1 files changed, 131 insertions, 83 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index f97f6fbc..25931869 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors +open CErrors open Pp open Util open Names @@ -19,6 +19,7 @@ open Evd open Reduction open Reductionops open Evarutil +open Evardefine open Evarsolve open Pretype_errors open Retyping @@ -27,6 +28,8 @@ open Recordops open Locus open Locusops open Find_subterm +open Sigma.Notations +open Context.Named.Declaration let keyed_unification = ref (false) let _ = Goptions.declare_bool_option { @@ -57,7 +60,7 @@ let occur_meta_or_undefined_evar evd c = | Evar_defined c -> occrec c; Array.iter occrec args | Evar_empty -> raise Occur) - | _ -> iter_constr occrec c + | _ -> Constr.iter occrec c in try occrec c; false with Occur | Not_found -> true let occur_meta_evd sigma mv c = @@ -66,7 +69,7 @@ let occur_meta_evd sigma mv c = let c = whd_evar sigma (whd_meta sigma c) in match kind_of_term c with | Meta mv' when Int.equal mv mv' -> raise Occur - | _ -> iter_constr occrec c + | _ -> Constr.iter occrec c in try occrec c; false with Occur -> true (* if lname_typ is [xn,An;..;x1,A1] and l is a list of terms, @@ -74,7 +77,10 @@ let occur_meta_evd sigma mv c = let abstract_scheme env evd c l lname_typ = List.fold_left2 - (fun (t,evd) (locc,a) (na,_,ta) -> + (fun (t,evd) (locc,a) decl -> + let open Context.Rel.Declaration in + let na = get_name decl in + let ta = get_type decl in let na = match kind_of_term a with Var id -> Name id | _ -> na in (* [occur_meta ta] test removed for support of eelim/ecase but consequences are unclear... @@ -107,7 +113,9 @@ let set_occurrences_of_last_arg args = Some AllOccurrences :: List.tl (Array.map_to_list (fun _ -> None) args) let abstract_list_all_with_dependencies env evd typ c l = - let evd,ev = new_evar env evd typ in + let evd = Sigma.Unsafe.of_evar_map evd in + let Sigma (ev, evd, _) = new_evar env evd typ in + let evd = Sigma.to_evar_map evd in let evd,ev' = evar_absorb_arguments env evd (destEvar ev) l in let n = List.length l in let argoccs = set_occurrences_of_last_arg (Array.sub (snd ev') 0 n) in @@ -143,7 +151,7 @@ let rec subst_meta_instances bl c = | Meta i -> let select (j,_,_) = Int.equal i j in (try pi2 (List.find select bl) with Not_found -> c) - | _ -> map_constr (subst_meta_instances bl) c + | _ -> Constr.map (subst_meta_instances bl) c (** [env] should be the context in which the metas live *) @@ -161,7 +169,7 @@ let pose_all_metas_as_evars env evd t = evdref := meta_assign mv (ev,(Conv,TypeNotProcessed)) !evdref; ev) | _ -> - map_constr aux t in + Constr.map aux t in let c = aux t in (* side-effect *) (!evdref, c) @@ -356,6 +364,22 @@ let set_no_delta_flags flags = { resolve_evars = flags.resolve_evars } +(* For the first phase of keyed unification, restrict + to conversion (including beta-iota) only on closed terms *) +let set_no_delta_open_core_flags flags = { flags with + modulo_delta = empty_transparent_state; + modulo_betaiota = false; +} + +let set_no_delta_open_flags flags = { + core_unify_flags = set_no_delta_open_core_flags flags.core_unify_flags; + merge_unify_flags = set_no_delta_open_core_flags flags.merge_unify_flags; + subterm_unify_flags = set_no_delta_open_core_flags flags.subterm_unify_flags; + allow_K_in_toplevel_higher_order_unification = + flags.allow_K_in_toplevel_higher_order_unification; + resolve_evars = flags.resolve_evars +} + (* Default flag for the "simple apply" version of unification of a *) (* type against a type (e.g. apply) *) (* We set only the flags available at the time the new "apply" extended *) @@ -436,7 +460,7 @@ let use_metas_pattern_unification flags nb l = Array.for_all (fun c -> isRel c && destRel c <= nb) l type key = - | IsKey of Closure.table_key + | IsKey of CClosure.table_key | IsProj of projection * constr let expand_table_key env = function @@ -455,8 +479,8 @@ let unfold_projection env p stk = let expand_key ts env sigma = function | Some (IsKey k) -> expand_table_key env k | Some (IsProj (p, c)) -> - let red = Stack.zip (fst (whd_betaiota_deltazeta_for_iota_state ts env sigma - Cst_stack.empty (c, unfold_projection env p []))) + let red = Stack.zip (fst (whd_betaiota_deltazeta_for_iota_state ts env sigma + Cst_stack.empty (c, unfold_projection env p []))) in if Term.eq_constr (mkProj (p, c)) red then None else Some red | None -> None @@ -481,7 +505,8 @@ let key_of env b flags f = Id.Pred.mem id (fst flags.modulo_delta) -> Some (IsKey (VarKey id)) | Proj (p, c) when Projection.unfolded p - || Cpred.mem (Projection.constant p) (snd flags.modulo_delta) -> + || (is_transparent env (ConstKey (Projection.constant p)) && + (Cpred.mem (Projection.constant p) (snd flags.modulo_delta))) -> Some (IsProj (p, c)) | _ -> None @@ -547,7 +572,8 @@ let constr_cmp pb sigma flags t u = else sigma, b let do_reduce ts (env, nb) sigma c = - Stack.zip (fst (whd_betaiota_deltazeta_for_iota_state ts env sigma Cst_stack.empty (c, Stack.empty))) + Stack.zip (fst (whd_betaiota_deltazeta_for_iota_state + ts env sigma Cst_stack.empty (c, Stack.empty))) let use_full_betaiota flags = flags.modulo_betaiota && Flags.version_strictly_greater Flags.V8_3 @@ -556,6 +582,19 @@ let isAllowedEvar flags c = match kind_of_term c with | Evar (evk,_) -> not (Evar.Set.mem evk flags.frozen_evars) | _ -> false + +let subst_defined_metas_evars (bl,el) c = + let rec substrec c = match kind_of_term c with + | Meta i -> + let select (j,_,_) = Int.equal i j in + substrec (pi2 (List.find select bl)) + | Evar (evk,args) -> + let select (_,(evk',args'),_) = Evar.equal evk evk' && Array.equal Constr.equal args args' in + (try substrec (pi3 (List.find select el)) + with Not_found -> Constr.map substrec c) + | _ -> Constr.map substrec c + in try Some (substrec c) with Not_found -> None + let check_compatibility env pbty flags (sigma,metasubst,evarsubst) tyM tyN = match subst_defined_metas_evars (metasubst,[]) tyM with | None -> sigma @@ -592,7 +631,7 @@ let is_eta_constructor_app env ts f l1 term = | Construct (((_, i as ind), j), u) when i == 0 && j == 1 -> let mib = lookup_mind (fst ind) env in (match mib.Declarations.mind_record with - | Some (Some (_,exp,projs)) when mib.Declarations.mind_finite <> Decl_kinds.CoFinite && + | Some (Some (_,exp,projs)) when mib.Declarations.mind_finite == Decl_kinds.BiFinite && Array.length projs == Array.length l1 - mib.Declarations.mind_nparams -> (** Check that the other term is neutral *) is_neutral env ts term @@ -619,7 +658,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb and cN = Evarutil.whd_head_evar sigma curn in let () = if !debug_unification then - msg_debug (Termops.print_constr_env curenv cM ++ str" ~= " ++ Termops.print_constr_env curenv cN) + Feedback.msg_debug (Termops.print_constr_env curenv cM ++ str" ~= " ++ Termops.print_constr_env curenv cN) in match (kind_of_term cM,kind_of_term cN) with | Meta k1, Meta k2 -> @@ -704,7 +743,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb then Evd.set_leq_sort curenv sigma s1 s2 else Evd.set_eq_sort curenv sigma s1 s2 in (sigma', metasubst, evarsubst) - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> error_cannot_unify curenv sigma (m,n)) | Lambda (na,t1,c1), Lambda (_,t2,c2) -> @@ -1016,12 +1055,14 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb else error_cannot_unify (fst curenvnb) sigma (cM,cN) in - if !debug_unification then msg_debug (str "Starting unification"); + if !debug_unification then Feedback.msg_debug (str "Starting unification"); let opt = { at_top = conv_at_top; with_types = false; with_cs = true } in try let res = - if occur_meta_or_undefined_evar sigma m || occur_meta_or_undefined_evar sigma n - || subterm_restriction opt flags then None + if subterm_restriction opt flags || + occur_meta_or_undefined_evar sigma m || occur_meta_or_undefined_evar sigma n + then + None else let sigma, b = match flags.modulo_conv_on_closed_terms with | Some convflags -> infer_conv ~pb:cv_pb ~ts:convflags env sigma m n @@ -1037,11 +1078,12 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb let a = match res with | Some sigma -> sigma, ms, es | None -> unirec_rec (env,0) cv_pb opt subst m n in - if !debug_unification then msg_debug (str "Leaving unification with success"); + if !debug_unification then Feedback.msg_debug (str "Leaving unification with success"); a with e -> - if !debug_unification then msg_debug (str "Leaving unification with failure"); - raise e + let e = CErrors.push e in + if !debug_unification then Feedback.msg_debug (str "Leaving unification with failure"); + iraise e let unify_0 env sigma = unify_0_with_initial_metas (sigma,[],[]) true env @@ -1050,7 +1092,7 @@ let left = true let right = false let rec unify_with_eta keptside flags env sigma c1 c2 = -(* Question: try whd_betadeltaiota on ci if not two lambdas? *) +(* Question: try whd_all on ci if not two lambdas? *) match kind_of_term c1, kind_of_term c2 with | (Lambda (na,t1,c1'), Lambda (_,t2,c2')) -> let env' = push_rel_assum (na,t1) env in @@ -1098,11 +1140,11 @@ let merge_instances env sigma flags st1 st2 c1 c2 = else (right, st2, res) | (IsSuperType,IsSubType) -> (try (left, IsSubType, unify_0 env sigma CUMUL flags c2 c1) - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> (right, IsSubType, unify_0 env sigma CUMUL flags c1 c2)) | (IsSubType,IsSuperType) -> (try (left, IsSuperType, unify_0 env sigma CUMUL flags c1 c2) - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> (right, IsSuperType, unify_0 env sigma CUMUL flags c2 c1)) (* Unification @@ -1154,31 +1196,31 @@ let merge_instances env sigma flags st1 st2 c1 c2 = * close it off. But this might not always work, * since other metavars might also need to be resolved. *) -let applyHead env evd n c = - let rec apprec n c cty evd = +let applyHead env (type r) (evd : r Sigma.t) n c = + let rec apprec : type s. _ -> _ -> _ -> (r, s) Sigma.le -> s Sigma.t -> (constr, r) Sigma.sigma = + fun n c cty p evd -> if Int.equal n 0 then - (evd, c) + Sigma (c, evd, p) else - match kind_of_term (whd_betadeltaiota env evd cty) with + match kind_of_term (whd_all env (Sigma.to_evar_map evd) cty) with | Prod (_,c1,c2) -> - let (evd',evar) = - Evarutil.new_evar env evd ~src:(Loc.ghost,Evar_kinds.GoalEvar) c1 in - apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) evd' + let Sigma (evar, evd', q) = Evarutil.new_evar env evd ~src:(Loc.ghost,Evar_kinds.GoalEvar) c1 in + apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) (p +> q) evd' | _ -> error "Apply_Head_Then" in - apprec n c (Typing.unsafe_type_of env evd c) evd - + apprec n c (Typing.unsafe_type_of env (Sigma.to_evar_map evd) c) Sigma.refl evd + let is_mimick_head ts f = match kind_of_term f with - | Const (c,u) -> not (Closure.is_transparent_constant ts c) - | Var id -> not (Closure.is_transparent_variable ts id) + | Const (c,u) -> not (CClosure.is_transparent_constant ts c) + | Var id -> not (CClosure.is_transparent_variable ts id) | (Rel _|Construct _|Ind _) -> true | _ -> false let try_to_coerce env evd c cty tycon = let j = make_judge c cty in let (evd',j') = inh_conv_coerce_rigid_to true Loc.ghost env evd j tycon in - let evd' = Evarconv.consider_remaining_unif_problems env evd' in + let evd' = Evarconv.solve_unif_constraints_with_heuristics env evd' in let evd' = Evd.map_metas_fvalue (nf_evar evd') evd' in (evd',j'.uj_val) @@ -1228,7 +1270,11 @@ let solve_simple_evar_eqn ts env evd ev rhs = | UnifFailure (evd,reason) -> error_cannot_unify env evd ~reason (mkEvar ev,rhs); | Success evd -> - Evarconv.consider_remaining_unif_problems env evd + if Flags.version_less_or_equal Flags.V8_5 then + (* We used to force solving unrelated problems at arbitrary times *) + Evarconv.solve_unif_constraints_with_heuristics env evd + else (* solve_simple_eqn calls reconsider_unif_constraints itself *) + evd (* [w_merge env sigma b metas evars] merges common instances in metas or in evars, possibly generating new unification problems; if [b] @@ -1255,7 +1301,6 @@ let w_merge env with_types flags (evd,metas,evars) = if is_mimick_head flags.modulo_delta f then let evd' = mimick_undefined_evar evd flags f (Array.length cl) evk in - (* let evd' = Evarconv.consider_remaining_unif_problems env evd' in *) w_merge_rec evd' metas evars eqns else let evd' = @@ -1303,7 +1348,7 @@ let w_merge env with_types flags (evd,metas,evars) = else let evd' = if occur_meta_evd evd mv c then - if isMetaOf mv (whd_betadeltaiota env evd c) then evd + if isMetaOf mv (whd_all env evd c) then evd else error_cannot_unify env evd (mkMeta mv,c) else meta_assign mv (c,(status,TypeProcessed)) evd in @@ -1313,7 +1358,7 @@ let w_merge env with_types flags (evd,metas,evars) = let rec process_eqns failures = function | (mv,status,c)::eqns -> (match (try Inl (unify_type env evd flags mv status c) - with e when Errors.noncritical e -> Inr e) + with e when CErrors.noncritical e -> Inr e) with | Inr e -> process_eqns (((mv,status,c),e)::failures) eqns | Inl (evd,metas,evars) -> @@ -1327,7 +1372,9 @@ let w_merge env with_types flags (evd,metas,evars) = and mimick_undefined_evar evd flags hdc nargs sp = let ev = Evd.find_undefined evd sp in let sp_env = Global.env_of_context ev.evar_hyps in - let (evd', c) = applyHead sp_env evd nargs hdc in + let evd = Sigma.Unsafe.of_evar_map evd in + let Sigma (c, evd', _) = applyHead sp_env evd nargs hdc in + let evd' = Sigma.to_evar_map evd' in let (evd'',mc,ec) = unify_0 sp_env evd' CUMUL flags (get_type_of sp_env evd' c) ev.evar_concl in @@ -1345,10 +1392,11 @@ let w_merge env with_types flags (evd,metas,evars) = in w_merge_rec evd [] [] eqns in let res = (* merge constraints *) - w_merge_rec evd (order_metas metas) (List.rev evars) [] + w_merge_rec evd (order_metas metas) + (* Assign evars in the order of assignments during unification *) + (List.rev evars) [] in - if with_types then check_types res - else res + if with_types then check_types res else res let w_unify_meta_types env ?(flags=default_unify_flags ()) evd = let metas,evd = retract_coercible_metas evd in @@ -1406,7 +1454,7 @@ let w_typed_unify_array env evd flags f1 l1 f2 l2 = let subst = Array.fold_left2 fold_subst subst l1 l2 in let evd = w_merge env true flags.merge_unify_flags subst in try_resolve_typeclasses env evd flags.resolve_evars - (mkApp(f1,l1)) (mkApp(f2,l2)) + (mkApp(f1,l1)) (mkApp(f2,l2)) (* takes a substitution s, an open term op and a closed term cl try to find a subterm of cl which matches op, if op is just a Meta @@ -1430,15 +1478,16 @@ let indirectly_dependent c d decls = it is needed otherwise, as e.g. when abstracting over "2" in "forall H:0=2, H=H:>(0=1+1) -> 0=2." where there is now obvious way to see that the second hypothesis depends indirectly over 2 *) - List.exists (fun (id,_,_) -> dependent_in_decl (mkVar id) d) decls + List.exists (fun d' -> dependent_in_decl (mkVar (get_id d')) d) decls let indirect_dependency d decls = - pi1 (List.hd (List.filter (fun (id,_,_) -> dependent_in_decl (mkVar id) d) decls)) + decls |> List.filter (fun d' -> dependent_in_decl (mkVar (get_id d')) d) |> List.hd |> get_id let finish_evar_resolution ?(flags=Pretyping.all_and_fail_flags) env current_sigma (pending,c) = + let current_sigma = Sigma.to_evar_map current_sigma in let sigma = Pretyping.solve_remaining_evars flags env current_sigma pending in let sigma, subst = nf_univ_variables sigma in - sigma, subst_univs_constr subst (nf_evar sigma c) + Sigma.Unsafe.of_pair (subst_univs_constr subst (nf_evar sigma c), sigma) let default_matching_core_flags sigma = let ts = Names.full_transparent_state in { @@ -1450,9 +1499,7 @@ let default_matching_core_flags sigma = check_applied_meta_types = true; use_pattern_unification = false; use_meta_bound_pattern_unification = false; - frozen_evars = - fold_undefined (fun evk _ evars -> Evar.Set.add evk evars) - sigma Evar.Set.empty; + frozen_evars = Evar.Map.domain (Evd.undefined_map sigma); restrict_conv_on_strict_subterms = false; modulo_betaiota = false; modulo_eta = false; @@ -1514,11 +1561,12 @@ let make_pattern_test from_prefix_of_ind is_correct_type env sigma (pending,c) = | PretypeError (_,_,CannotUnify (c1,c2,Some e)) -> raise (NotUnifiable (Some (c1,c2,e))) (** MS: This is pretty bad, it catches Not_found for example *) - | e when Errors.noncritical e -> raise (NotUnifiable None) in + | e when CErrors.noncritical e -> raise (NotUnifiable None) in let merge_fun c1 c2 = match c1, c2 with - | Some (evd,c1,_) as x, Some (_,c2,_) -> - if is_conv env sigma c1 c2 then x else raise (NotUnifiable None) + | Some (evd,c1,x), Some (_,c2,_) -> + let (evd,b) = infer_conv ~pb:CONV env evd c1 c2 in + if b then Some (evd, c1, x) else raise (NotUnifiable None) | Some _, None -> c1 | None, Some _ -> c2 | None, None -> None in @@ -1543,7 +1591,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl = let x = id_of_name_using_hdchar (Global.env()) t name in let ids = ids_of_named_context (named_context env) in if name == Anonymous then next_ident_away_in_goal x ids else - if mem_named_context x (named_context env) then + if mem_named_context_val x (named_context_val env) then errorlabstrm "Unification.make_abstraction_core" (str "The variable " ++ Nameops.pr_id x ++ str " is already declared.") else @@ -1551,21 +1599,15 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl = in let likefirst = clause_with_generic_occurrences occs in let mkvarid () = mkVar id in - let compute_dependency _ (hyp,_,_ as d) (sign,depdecls) = + let compute_dependency _ d (sign,depdecls) = + let hyp = get_id d in match occurrences_of_hyp hyp occs with | NoOccurrences, InHyp -> - if indirectly_dependent c d depdecls then - (* Told explicitly not to abstract over [d], but it is dependent *) - let id' = indirect_dependency d depdecls in - errorlabstrm "" (str "Cannot abstract over " ++ Nameops.pr_id id' - ++ str " without also abstracting or erasing " ++ Nameops.pr_id hyp - ++ str ".") - else - (push_named_context_val d sign,depdecls) + (push_named_context_val d sign,depdecls) | AllOccurrences, InHyp as occ -> let occ = if likefirst then LikeFirst else AtOccs occ in let newdecl = replace_term_occ_decl_modulo occ test mkvarid d in - if Context.eq_named_declaration d newdecl + if Context.Named.Declaration.equal d newdecl && not (indirectly_dependent c d depdecls) then if check_occs && not (in_every_hyp occs) @@ -1588,8 +1630,12 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl = replace_term_occ_modulo occ test mkvarid concl in let lastlhyp = - if List.is_empty depdecls then None else Some (pi1(List.last depdecls)) in - (id,sign,depdecls,lastlhyp,ccl,out test) + if List.is_empty depdecls then None else Some (get_id (List.last depdecls)) in + let res = match out test with + | None -> None + | Some (sigma, c) -> Some (Sigma.Unsafe.of_pair (c, sigma)) + in + (id,sign,depdecls,lastlhyp,ccl,res) with SubtermUnificationError e -> raise (PretypeError (env,sigma,CannotUnifyOccurrences e)) @@ -1611,12 +1657,13 @@ type abstraction_request = | AbstractPattern of prefix_of_inductive_support_flag * (types -> bool) * Name.t * pending_constr * clause * bool | AbstractExact of Name.t * constr * types option * clause * bool -type abstraction_result = +type 'r abstraction_result = Names.Id.t * named_context_val * - Context.named_declaration list * Names.Id.t option * - types * (Evd.evar_map * constr) option + Context.Named.Declaration.t list * Names.Id.t option * + types * (constr, 'r) Sigma.sigma option let make_abstraction env evd ccl abs = + let evd = Sigma.to_evar_map evd in match abs with | AbstractPattern (from_prefix,check,name,c,occs,check_occs) -> make_abstraction_core name @@ -1791,17 +1838,25 @@ let w_unify_to_subterm_list env evd flags hdmeta oplist t = let allow_K = flags.allow_K_in_toplevel_higher_order_unification in let flags = if occur_meta_or_existential op || !keyed_unification then + (* This is up to delta for subterms w/o metas ... *) flags else (* up to Nov 2014, unification was bypassed on evar/meta-free terms; now it is called in a minimalistic way, at least to possibly unify pre-existing non frozen evars of the goal or of the pattern *) - set_no_delta_flags flags in + set_no_delta_flags flags in + let t' = (strip_outer_cast op,t) in let (evd',cl) = try - (* This is up to delta for subterms w/o metas ... *) - w_unify_to_subterm env evd ~flags (strip_outer_cast op,t) + if is_keyed_unification () then + try (* First try finding a subterm w/o conversion on open terms *) + let flags = set_no_delta_open_flags flags in + w_unify_to_subterm env evd ~flags t' + with e -> + (* If this fails, try with full conversion *) + w_unify_to_subterm env evd ~flags t' + else w_unify_to_subterm env evd ~flags t' with PretypeError (env,_,NoOccurrenceFound _) when allow_K || (* w_unify_to_subterm does not go through evars, so @@ -1828,21 +1883,14 @@ let secondOrderAbstraction env evd flags typ (p, oplist) = error_wrong_abstraction_type env evd' (Evd.meta_name evd p) pred typp predtyp; w_merge env false flags.merge_unify_flags - (evd',[p,pred,(Conv,TypeProcessed)],[]) - - (* let evd',metas,evars = *) - (* try unify_0 env evd' CUMUL flags predtyp typp *) - (* with NotConvertible -> *) - (* error_wrong_abstraction_type env evd *) - (* (Evd.meta_name evd p) pred typp predtyp *) - (* in *) - (* w_merge env false flags (evd',(p,pred,(Conv,TypeProcessed))::metas,evars) *) + (evd',[p,pred,(Conv,TypeProcessed)],[]) let secondOrderDependentAbstraction env evd flags typ (p, oplist) = let typp = Typing.meta_type evd p in let evd, pred = abstract_list_all_with_dependencies env evd typp typ oplist in w_merge env false flags.merge_unify_flags - (evd,[p,pred,(Conv,TypeProcessed)],[]) + (evd,[p,pred,(Conv,TypeProcessed)],[]) + let secondOrderAbstractionAlgo dep = if dep then secondOrderDependentAbstraction else secondOrderAbstraction |