aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/arguments_renaming.ml8
-rw-r--r--pretyping/arguments_renaming.mli6
-rw-r--r--pretyping/cases.ml137
-rw-r--r--pretyping/cases.mli5
-rw-r--r--pretyping/evarconv.ml40
-rw-r--r--pretyping/evarconv.mli3
-rw-r--r--pretyping/evarsolve.ml66
-rw-r--r--pretyping/evarsolve.mli3
-rw-r--r--pretyping/pretyping.ml49
-rw-r--r--pretyping/pretyping.mli6
-rw-r--r--pretyping/program.ml6
-rw-r--r--pretyping/reductionops.ml2
-rw-r--r--pretyping/retyping.mli2
-rw-r--r--pretyping/typeclasses.ml48
-rw-r--r--pretyping/typeclasses.mli17
-rw-r--r--pretyping/unification.ml33
16 files changed, 233 insertions, 198 deletions
diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml
index ca1d0b7fba..e18aece090 100644
--- a/pretyping/arguments_renaming.ml
+++ b/pretyping/arguments_renaming.ml
@@ -16,12 +16,12 @@ open Libobject
(*i*)
let name_table =
- Summary.ref (Refmap.empty : Name.t list list Refmap.t)
+ Summary.ref (Refmap.empty : Name.t list Refmap.t)
~name:"rename-arguments"
type req =
| ReqLocal
- | ReqGlobal of global_reference * Name.t list list
+ | ReqGlobal of global_reference * Name.t list
let load_rename_args _ (_, (_, (r, names))) =
name_table := Refmap.add r names !name_table
@@ -49,7 +49,7 @@ let discharge_rename_args = function
let vars,_,_ = section_segment_of_reference c in
let c' = pop_global_reference c in
let var_names = List.map (fun (id, _,_,_) -> Name id) vars in
- let names' = List.map (fun l -> var_names @ l) names in
+ let names' = var_names @ names in
Some (ReqGlobal (c', names), (c', names'))
with Not_found -> Some req)
| _ -> None
@@ -83,7 +83,7 @@ let rec rename_prod c = function
| _ -> c
let rename_type ty ref =
- try rename_prod ty (List.hd (arguments_names ref))
+ try rename_prod ty (arguments_names ref)
with Not_found -> ty
let rename_type_of_constant env c =
diff --git a/pretyping/arguments_renaming.mli b/pretyping/arguments_renaming.mli
index a334055011..e123e77862 100644
--- a/pretyping/arguments_renaming.mli
+++ b/pretyping/arguments_renaming.mli
@@ -11,10 +11,10 @@ open Globnames
open Environ
open Term
-val rename_arguments : bool -> global_reference -> Name.t list list -> unit
+val rename_arguments : bool -> global_reference -> Name.t list -> unit
-(** [Not_found] is raised is no names are defined for [r] *)
-val arguments_names : global_reference -> Name.t list list
+(** [Not_found] is raised if no names are defined for [r] *)
+val arguments_names : global_reference -> Name.t list
val rename_type_of_constant : env -> pconstant -> types
val rename_type_of_inductive : env -> pinductive -> types
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index e89c3ea719..ef3e53bf1f 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -62,13 +62,15 @@ let error_wrong_numarg_constructor_loc loc env c n =
let error_wrong_numarg_inductive_loc loc env c n =
raise_pattern_matching_error (loc, env, Evd.empty, WrongNumargInductive(c,n))
-let rec list_try_compile f = function
- | [a] -> f a
- | [] -> anomaly (str "try_find_f")
+let list_try_compile f l =
+ let rec aux errors = function
+ | [] -> if errors = [] then anomaly (str "try_find_f") else iraise (List.last errors)
| h::t ->
try f h
- with UserError _ | TypeError _ | PretypeError _ | PatternMatchingError _ ->
- list_try_compile f t
+ with UserError _ | TypeError _ | PretypeError _ | PatternMatchingError _ as e ->
+ let e = CErrors.push e in
+ aux (e::errors) t in
+ aux [] l
let force_name =
let nx = Name default_dependent_ident in function Anonymous -> nx | na -> na
@@ -845,7 +847,7 @@ let subst_predicate (subst,copt) ccl tms =
| Some c -> c::subst in
substnl_predicate sigma 0 ccl tms
-let specialize_predicate_var (cur,typ,dep) tms ccl =
+let specialize_predicate_var (cur,typ,dep) env tms ccl =
let c = match dep with
| Anonymous -> None
| Name _ -> Some cur
@@ -853,7 +855,9 @@ let specialize_predicate_var (cur,typ,dep) tms ccl =
let l =
match typ with
| IsInd (_, IndType (_, _), []) -> []
- | IsInd (_, IndType (_, realargs), names) -> realargs
+ | IsInd (_, IndType (indf, realargs), names) ->
+ let arsign,_ = get_arity env indf in
+ subst_of_rel_context_instance arsign realargs
| NotInd _ -> [] in
subst_predicate (l,c) ccl tms
@@ -1388,7 +1392,7 @@ and match_current pb (initial,tomatch) =
and shift_problem ((current,t),_,na) pb =
let ty = type_of_tomatch t in
let tomatch = lift_tomatch_stack 1 pb.tomatch in
- let pred = specialize_predicate_var (current,t,na) pb.tomatch pb.pred in
+ let pred = specialize_predicate_var (current,t,na) pb.env pb.tomatch pb.pred in
let pb =
{ pb with
env = push_rel (LocalDef (na,current,ty)) pb.env;
@@ -1405,7 +1409,7 @@ and shift_problem ((current,t),_,na) pb =
are already introduced in the context, we avoid creating aliases to
themselves by treating this case specially. *)
and pop_problem ((current,t),_,na) pb =
- let pred = specialize_predicate_var (current,t,na) pb.tomatch pb.pred in
+ let pred = specialize_predicate_var (current,t,na) pb.env pb.tomatch pb.pred in
let pb =
{ pb with
pred = pred;
@@ -1870,22 +1874,16 @@ let inh_conv_coerce_to_tycon loc env evdref j tycon =
(* We put the tycon inside the arity signature, possibly discovering dependencies. *)
-let add_subst c len (rel_subst,var_subst) =
- match kind_of_term c with
- | Rel n -> (n,len) :: rel_subst, var_subst
- | Var id -> rel_subst, (id,len) :: var_subst
- | _ -> assert false
-
let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c =
let nar = List.fold_left (fun n sign -> Context.Rel.nhyps sign + n) 0 arsign in
- let (rel_subst,var_subst), len =
+ let subst, len =
List.fold_right2 (fun (tm, tmtype) sign (subst, len) ->
let signlen = List.length sign in
match kind_of_term tm with
- | Rel _ | Var _ when dependent tm c
+ | Rel n when dependent tm c
&& Int.equal signlen 1 (* The term to match is not of a dependent type itself *) ->
- (add_subst tm len subst, len - signlen)
- | Rel _ | Var _ when signlen > 1 (* The term is of a dependent type,
+ ((n, len) :: subst, len - signlen)
+ | Rel n when signlen > 1 (* The term is of a dependent type,
maybe some variable in its type appears in the tycon. *) ->
(match tmtype with
NotInd _ -> (subst, len - signlen)
@@ -1894,36 +1892,28 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c =
List.fold_left
(fun (subst, len) arg ->
match kind_of_term arg with
- | Rel _ | Var _ when dependent arg c ->
- (add_subst arg len subst, pred len)
+ | Rel n when dependent arg c ->
+ ((n, len) :: subst, pred len)
| _ -> (subst, pred len))
(subst, len) realargs
in
let subst =
- if dependent tm c && List.for_all (fun c -> isRel c || isVar c) realargs
- then add_subst tm len subst else subst
+ if dependent tm c && List.for_all isRel realargs
+ then (n, len) :: subst else subst
in (subst, pred len))
| _ -> (subst, len - signlen))
- (List.rev tomatchs) arsign (([],[]), nar)
+ (List.rev tomatchs) arsign ([], nar)
in
let rec predicate lift c =
match kind_of_term c with
| Rel n when n > lift ->
(try
(* Make the predicate dependent on the matched variable *)
- let idx = Int.List.assoc (n - lift) rel_subst in
+ let idx = Int.List.assoc (n - lift) subst in
mkRel (idx + lift)
with Not_found ->
- (* A variable that is not matched, lift over the arsign *)
+ (* A variable that is not matched, lift over the arsign. *)
mkRel (n + nar))
- | Var id ->
- (try
- (* Make the predicate dependent on the matched variable *)
- let idx = Id.List.assoc id var_subst in
- mkRel (idx + lift)
- with Not_found ->
- (* A variable that is not matched *)
- c)
| _ ->
map_constr_with_binders succ predicate lift c
in
@@ -1939,44 +1929,54 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c =
* type and 1 assumption for each term not _syntactically_ in an
* inductive type.
- * Each matched term is independently considered dependent or not.
+ * Each matched terms are independently considered dependent or not.
+
+ * A type constraint but no annotation case: we try to specialize the
+ * tycon to make the predicate if it is not closed.
*)
let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred =
+ let refresh_tycon sigma t =
+ (** If we put the typing constraint in the term, it has to be
+ refreshed to preserve the invariant that no algebraic universe
+ can appear in the term. *)
+ refresh_universes ~status:Evd.univ_flexible ~onlyalg:true (Some true)
+ env sigma t
+ in
let preds =
- match pred with
+ match pred, tycon with
(* No return clause *)
- | None ->
- let sigma,t =
- match tycon with
- | Some t -> sigma, t
- | None ->
- (* No type constraint: we first create a generic evar type constraint *)
- let src = (loc, Evar_kinds.CasesType false) in
- let sigma = Sigma.Unsafe.of_evar_map sigma in
- let Sigma ((t, _), sigma, _) = new_type_evar env sigma univ_flexible_alg ~src in
- let sigma = Sigma.to_evar_map sigma in
- sigma, t in
- (* First strategy: we build an "inversion" predicate, also replacing the *)
- (* dependencies with existential variables *)
- let sigma1,pred1 = build_inversion_problem loc env sigma tomatchs t in
- (* Optional second strategy: we abstract the tycon wrt to the dependencies *)
- let p2 =
+ | None, Some t when not (noccur_with_meta 0 max_int t) ->
+ (* If the tycon is not closed w.r.t real variables, we try *)
+ (* two different strategies *)
+ (* First strategy: we abstract the tycon wrt to the dependencies *)
+ let sigma, t = refresh_tycon sigma t in
+ let p1 =
prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign t in
- (* Third strategy: we take the type constraint as it is; of course we could *)
- (* need something inbetween, abstracting some but not all of the dependencies *)
- (* the "inversion" strategy deals with that but unification may not be *)
- (* powerful enough so strategy 2 and 3 helps; moreover, inverting does not *)
- (* work (yet) when a constructor has a type not precise enough for the inversion *)
- (* see log message for details *)
- let pred3 = lift (List.length (List.flatten arsign)) t in
- (match p2 with
- | Some (sigma2,pred2) when not (Constr.equal pred2 pred3) ->
- [sigma1, pred1; sigma2, pred2; sigma, pred3]
- | _ ->
- [sigma1, pred1; sigma, pred3])
+ (* Second strategy: we build an "inversion" predicate *)
+ let sigma2,pred2 = build_inversion_problem loc env sigma tomatchs t in
+ (match p1 with
+ | Some (sigma1,pred1) -> [sigma1, pred1; sigma2, pred2]
+ | None -> [sigma2, pred2])
+ | None, _ ->
+ (* No dependent type constraint, or no constraints at all: *)
+ (* we use two strategies *)
+ let sigma,t = match tycon with
+ | Some t -> refresh_tycon sigma t
+ | None ->
+ let sigma = Sigma.Unsafe.of_evar_map sigma in
+ let Sigma ((t, _), sigma, _) =
+ new_type_evar env sigma univ_flexible_alg ~src:(loc, Evar_kinds.CasesType false) in
+ let sigma = Sigma.to_evar_map sigma in
+ sigma, t
+ in
+ (* First strategy: we build an "inversion" predicate *)
+ let sigma1,pred1 = build_inversion_problem loc env sigma tomatchs t in
+ (* Second strategy: we directly use the evar as a non dependent pred *)
+ let pred2 = lift (List.length (List.flatten arsign)) t in
+ [sigma1, pred1; sigma, pred2]
(* Some type annotation *)
- | Some rtntyp ->
+ | Some rtntyp, _ ->
(* We extract the signature of the arity *)
let envar = List.fold_right push_rel_context arsign env in
let sigma, newt = new_sort_variable univ_flexible_alg sigma in
@@ -2577,6 +2577,9 @@ let compile_cases loc style (typing_fun, evdref) tycon env (predopt, tomatchl, e
typing_function = typing_fun } in
let j = compile pb in
+
+ (* We coerce to the tycon (if an elim predicate was provided) *)
+ let j = inh_conv_coerce_to_tycon loc env myevdref j tycon in
evdref := !myevdref;
j in
@@ -2587,6 +2590,4 @@ let compile_cases loc style (typing_fun, evdref) tycon env (predopt, tomatchl, e
(* We check for unused patterns *)
List.iter (check_unused_pattern env) matx;
- (* We coerce to the tycon (if an elim predicate was provided) *)
- inh_conv_coerce_to_tycon loc env evdref j tycon
-
+ j
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index ba566f3744..ee4148de64 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -114,10 +114,11 @@ val compile : 'a pattern_matching_problem -> Environ.unsafe_judgment
val prepare_predicate : Loc.t ->
(Evarutil.type_constraint ->
- Environ.env -> Evd.evar_map ref -> 'a -> Environ.unsafe_judgment) ->
+ Environ.env -> Evd.evar_map ref -> glob_constr -> Environ.unsafe_judgment) ->
Environ.env ->
Evd.evar_map ->
(Term.types * tomatch_type) list ->
Context.Rel.t list ->
Constr.constr option ->
- 'a option -> (Evd.evar_map * Names.name list * Term.constr) list
+ glob_constr option ->
+ (Evd.evar_map * Names.name list * Term.constr) list
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index b033f5a395..9fd55a488e 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -42,12 +42,7 @@ let _ = Goptions.declare_bool_option {
let unfold_projection env evd ts p c =
let cst = Projection.constant p in
if is_transparent_constant ts cst then
- let c' = Some (mkProj (Projection.make cst true, c)) in
- match ReductionBehaviour.get (Globnames.ConstRef cst) with
- | None -> c'
- | Some (recargs, nargs, flags) ->
- if (List.mem `ReductionNeverUnfold flags) then None
- else c'
+ Some (mkProj (Projection.make cst true, c))
else None
let eval_flexible_term ts env evd c =
@@ -102,19 +97,19 @@ let position_problem l2r = function
| CONV -> None
| CUMUL -> Some l2r
-let occur_rigidly ev evd t =
+let occur_rigidly (evk,_ as ev) evd t =
let rec aux t =
match kind_of_term (whd_evar 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)
- | Evar (ev',_) -> if Evar.equal ev ev' then raise Occur else false
+ | Evar (evk',_) -> if Evar.equal evk evk' then raise Occur else false
| Cast (p, _, _) -> aux p
| Lambda _ | LetIn _ -> false
| Const _ -> false
| Prod (_, b, t) -> ignore(aux b || aux t); true
| Rel _ | Var _ -> false
- | Case _ -> false
+ | Case (_,_,c,_) -> if eq_constr (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
@@ -483,7 +478,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
ise_try evd
[eta;(* Postpone the use of an heuristic *)
(fun i ->
- if not (occur_rigidly (fst ev) i tR) then
+ if not (occur_rigidly ev i tR) then
let i,tF =
if isRel tR || isVar tR then
(* Optimization so as to generate candidates *)
@@ -1086,7 +1081,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
match evar_conv_x ts env_evar evd CUMUL idty evty with
| UnifFailure _ -> error "Cannot find an instance"
| Success evd ->
- match reconsider_conv_pbs (evar_conv_x ts) evd with
+ match reconsider_unif_constraints (evar_conv_x ts) evd with
| UnifFailure _ -> error "Cannot find an instance"
| Success evd ->
evd
@@ -1152,7 +1147,7 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
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
(position_problem true pbty) evk1 args1 args2)
- | Evar ev1, Evar ev2 ->
+ | Evar ev1, Evar ev2 when app_empty ->
Success (solve_evar_evar ~force:true
(evar_define (evar_conv_x ts) ~choose:true) (evar_conv_x ts) env evd
(position_problem true pbty) ev1 ev2)
@@ -1180,9 +1175,14 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
(* Some head evar have been instantiated, or unknown kind of problem *)
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
+ evd ?reason (t1, t2)
+
let check_problems_are_solved env evd =
match snd (extract_all_conv_pbs evd) with
- | (pbty,env,t1,t2)::_ -> Pretype_errors.error_cannot_unify env evd (t1, t2)
+ | (pbty,env,t1,t2) as pb::_ -> error_cannot_unify env evd pb t1 t2
| _ -> ()
let max_undefined_with_candidates evd =
@@ -1213,7 +1213,7 @@ let rec solve_unconstrained_evars_with_candidates ts evd =
let conv_algo = evar_conv_x ts in
let evd = check_evar_instance evd evk a conv_algo in
let evd = Evd.define evk a evd in
- match reconsider_conv_pbs conv_algo evd with
+ match reconsider_unif_constraints conv_algo evd with
| Success evd -> solve_unconstrained_evars_with_candidates ts evd
| UnifFailure _ -> aux l
with
@@ -1236,7 +1236,7 @@ let solve_unconstrained_impossible_cases env evd =
Evd.define evk ty evd'
| _ -> evd') evd evd
-let consider_remaining_unif_problems env
+let solve_unif_constraints_with_heuristics env
?(ts=Conv_oracle.get_transp_state (Environ.oracle env)) evd =
let evd = solve_unconstrained_evars_with_candidates ts evd in
let rec aux evd pbs progress stuck =
@@ -1251,23 +1251,23 @@ let consider_remaining_unif_problems env
aux evd pbs progress (pb :: stuck)
end
| UnifFailure (evd,reason) ->
- Pretype_errors.error_cannot_unify_loc (loc_of_conv_pb evd pb)
- env evd ~reason (t1, t2))
+ error_cannot_unify env evd pb ~reason t1 t2)
| _ ->
if progress then aux evd stuck false []
else
match stuck with
| [] -> (* We're finished *) evd
| (pbty,env,t1,t2 as pb) :: _ ->
- (* There remains stuck problems *)
- Pretype_errors.error_cannot_unify_loc (loc_of_conv_pb evd pb)
- env evd (t1, t2)
+ (* There remains stuck problems *)
+ error_cannot_unify env evd pb t1 t2
in
let (evd,pbs) = extract_all_conv_pbs evd in
let heuristic_solved_evd = aux evd pbs false [] in
check_problems_are_solved env heuristic_solved_evd;
solve_unconstrained_impossible_cases env heuristic_solved_evd
+let consider_remaining_unif_problems = solve_unif_constraints_with_heuristics
+
(* Main entry points *)
exception UnableToUnify of evar_map * unification_error
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index 14947c8927..2231e5bc30 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -33,7 +33,10 @@ val e_cumul : env -> ?ts:transparent_state -> evar_map ref -> constr -> constr -
(** Try heuristics to solve pending unification problems and to solve
evars with candidates *)
+val solve_unif_constraints_with_heuristics : env -> ?ts:transparent_state -> evar_map -> evar_map
+
val consider_remaining_unif_problems : env -> ?ts:transparent_state -> evar_map -> evar_map
+(** @deprecated Alias for [solve_unif_constraints_with_heuristics] *)
(** Check all pending unification problems are solved and raise an
error otherwise *)
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 6c8677855a..4fd030845d 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -42,33 +42,39 @@ let get_polymorphic_positions f =
templ.template_param_levels)
| _ -> assert false
-let refresh_level evd s =
- match Evd.is_sort_variable evd s with
- | None -> true
- | Some l -> not (Evd.is_flexible_level evd l)
-
let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false)
pbty env evd t =
let evdref = ref evd in
let modified = ref false in
- let rec refresh status dir t =
- match kind_of_term t with
- | Sort (Type u as s) when
- (match Univ.universe_level u with
- | None -> true
- | Some l -> not onlyalg && refresh_level evd s) ->
+ (* direction: true for fresh universes lower than the existing ones *)
+ let refresh_sort status ~direction s =
let s' = evd_comb0 (new_sort_variable status) evdref in
let evd =
- if dir then set_leq_sort env !evdref s' s
+ if direction then set_leq_sort env !evdref s' s
else set_leq_sort env !evdref s s'
in
- modified := true; evdref := evd; mkSort s'
- | Sort (Prop Pos as s) when refreshset && not dir ->
- let s' = evd_comb0 (new_sort_variable status) evdref in
- let evd = set_leq_sort env !evdref s s' in
- modified := true; evdref := evd; mkSort s'
+ modified := true; evdref := evd; mkSort s'
+ in
+ let rec refresh ~onlyalg status ~direction t =
+ match kind_of_term t with
+ | Sort (Type u as s) ->
+ (match Univ.universe_level u with
+ | None -> refresh_sort status ~direction s
+ | Some l ->
+ (match Evd.universe_rigidity evd l with
+ | UnivRigid ->
+ if not onlyalg then refresh_sort status ~direction s
+ else t
+ | UnivFlexible alg ->
+ if onlyalg && alg then
+ (evdref := Evd.make_flexible_variable !evdref false l; t)
+ else t))
+ | Sort (Prop Pos as s) when refreshset && not direction ->
+ (* Cannot make a universe "lower" than "Set",
+ only refreshing when we want higher universes. *)
+ refresh_sort status ~direction s
| Prod (na,u,v) ->
- mkProd (na,u,refresh status dir v)
+ mkProd (na, u, refresh ~onlyalg status ~direction v)
| _ -> t
(** Refresh the types of evars under template polymorphic references *)
and refresh_term_evars onevars top t =
@@ -81,7 +87,7 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false)
Array.iter (refresh_term_evars onevars false) args
| Evar (ev, a) when onevars ->
let evi = Evd.find !evdref ev in
- let ty' = refresh univ_flexible true evi.evar_concl in
+ let ty' = refresh ~onlyalg univ_flexible ~direction:true evi.evar_concl in
if !modified then
evdref := Evd.add !evdref ev {evi with evar_concl = ty'}
else ()
@@ -101,9 +107,11 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false)
in
let t' =
if isArity t then
- (match pbty with
- | None -> t
- | Some dir -> refresh status dir t)
+ match pbty with
+ | None ->
+ (* No cumulativity needed, but we still need to refresh the algebraics *)
+ refresh ~onlyalg:true univ_flexible ~direction:false t
+ | Some direction -> refresh ~onlyalg status ~direction t
else (refresh_term_evars false true t; t)
in
if !modified then !evdref, t' else !evdref, t
@@ -613,7 +621,13 @@ let define_evar_from_virtual_equation define_fun env evd src t_in_env ty_t_in_si
* substitution u1..uq.
*)
+exception MorePreciseOccurCheckNeeeded
+
let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
+ if Evd.is_defined evd evk1 then
+ (* Some circularity somewhere (see e.g. #3209) *)
+ raise MorePreciseOccurCheckNeeeded;
+ let (evk1,args1) = destEvar (whd_evar evd (mkEvar (evk1,args1))) in
let evi1 = Evd.find_undefined evd evk1 in
let env1,rel_sign = env_rel_context_chop k env in
let sign1 = evar_hyps evi1 in
@@ -1553,6 +1567,8 @@ and evar_define conv_algo ?(choose=false) env evd pbty (evk,argsv as ev) rhs =
postpone_non_unique_projection env evd pbty ev sols rhs
| NotEnoughInformationEvarEvar t ->
add_conv_oriented_pb (pbty,env,mkEvar ev,t) evd
+ | MorePreciseOccurCheckNeeeded ->
+ add_conv_oriented_pb (pbty,env,mkEvar ev,rhs) evd
| NotInvertibleUsingOurAlgorithm _ | MetaOccurInBodyInternal as e ->
raise e
| OccurCheckIn (evd,rhs) ->
@@ -1595,7 +1611,7 @@ let status_changed lev (pbty,_,t1,t2) =
(try Evar.Set.mem (head_evar t1) lev with NoHeadEvar -> false) ||
(try Evar.Set.mem (head_evar t2) lev with NoHeadEvar -> false)
-let reconsider_conv_pbs conv_algo evd =
+let reconsider_unif_constraints conv_algo evd =
let (evd,pbs) = extract_changed_conv_pbs evd status_changed in
List.fold_left
(fun p (pbty,env,t1,t2 as x) ->
@@ -1608,6 +1624,8 @@ let reconsider_conv_pbs conv_algo evd =
(Success evd)
pbs
+let reconsider_conv_pbs = reconsider_unif_constraints
+
(* Tries to solve problem t1 = t2.
* Precondition: t1 is an uninstantiated evar
* Returns an optional list of evars that were instantiated, or None
@@ -1618,7 +1636,7 @@ let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1)
try
let t2 = whd_betaiota evd t2 in (* includes whd_evar *)
let evd = evar_define conv_algo ~choose env evd pbty ev1 t2 in
- reconsider_conv_pbs conv_algo evd
+ reconsider_unif_constraints conv_algo evd
with
| NotInvertibleUsingOurAlgorithm t ->
UnifFailure (evd,NotClean (ev1,env,t))
diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli
index f94c83b6dc..b6bdc07889 100644
--- a/pretyping/evarsolve.mli
+++ b/pretyping/evarsolve.mli
@@ -54,7 +54,10 @@ val solve_evar_evar : ?force:bool ->
val solve_simple_eqn : conv_fun -> ?choose:bool -> env -> evar_map ->
bool option * existential * constr -> unification_result
+val reconsider_unif_constraints : conv_fun -> evar_map -> unification_result
+
val reconsider_conv_pbs : conv_fun -> evar_map -> unification_result
+(** @deprecated Alias for [reconsider_unif_constraints] *)
val is_unification_pattern_evar : env -> evar_map -> existential -> constr list ->
constr -> constr list option
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 46f0219f91..4b6d10c640 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -239,25 +239,34 @@ let interp_elimination_sort = function
| GSet -> InSet
| GType _ -> InType
+type inference_hook = env -> evar_map -> evar -> evar_map * constr
+
type inference_flags = {
use_typeclasses : bool;
- use_unif_heuristics : bool;
- use_hook : (env -> evar_map -> evar -> constr) option;
+ solve_unification_constraints : bool;
+ use_hook : inference_hook option;
fail_evar : bool;
expand_evars : bool
}
-let frozen_holes (sigma, sigma') =
- (); fun ev -> Evar.Map.mem ev (Evd.undefined_map sigma)
-
-let pending_holes (sigma, sigma') =
- let fold evk _ accu =
- if not (Evd.mem sigma evk) then Evar.Set.add evk accu else accu
- in
- Evd.fold_undefined fold sigma' Evar.Set.empty
+(* Compute the set of still-undefined initial evars up to restriction
+ (e.g. clearing) and the set of yet-unsolved evars freshly created
+ in the extension [sigma'] of [sigma] (excluding the restrictions of
+ the undefined evars of [sigma] to be freshly created evars of
+ [sigma']). Otherwise said, we partition the undefined evars of
+ [sigma'] into those already in [sigma] or deriving from an evar in
+ [sigma] by restriction, and the evars properly created in [sigma'] *)
+
+let frozen_and_pending_holes (sigma, sigma') =
+ let add_derivative_of evk evi acc =
+ match advance sigma' evk with None -> acc | Some evk' -> Evar.Set.add evk' acc in
+ let frozen = Evd.fold_undefined add_derivative_of sigma Evar.Set.empty in
+ let fold evk _ accu = if not (Evar.Set.mem evk frozen) then Evar.Set.add evk accu else accu in
+ let pending = Evd.fold_undefined fold sigma' Evar.Set.empty in
+ (frozen,pending)
let apply_typeclasses env evdref frozen fail_evar =
- let filter_frozen = frozen in
+ let filter_frozen evk = Evar.Set.mem evk frozen in
evdref := Typeclasses.resolve_typeclasses
~filter:(if Flags.is_program_mode ()
then (fun evk evi -> Typeclasses.no_goals_or_obligations evk evi && not (filter_frozen evk))
@@ -272,7 +281,7 @@ let apply_inference_hook hook evdref pending =
if Evd.is_undefined sigma evk (* in particular not defined by side-effect *)
then
try
- let c = hook sigma evk in
+ let sigma, c = hook sigma evk in
Evd.define evk c sigma
with Exit ->
sigma
@@ -281,7 +290,7 @@ let apply_inference_hook hook evdref pending =
let apply_heuristics env evdref fail_evar =
(* Resolve eagerly, potentially making wrong choices *)
- try evdref := consider_remaining_unif_problems
+ try evdref := solve_unif_constraints_with_heuristics
~ts:(Typeclasses.classes_transparent_state ()) env !evdref
with e when CErrors.noncritical e ->
let e = CErrors.push e in if fail_evar then iraise e
@@ -325,19 +334,17 @@ let check_evars_are_solved env current_sigma frozen pending =
(* Try typeclasses, hooks, unification heuristics ... *)
let solve_remaining_evars flags env current_sigma pending =
- let frozen = frozen_holes pending in
- let pending = pending_holes pending in
+ let frozen,pending = frozen_and_pending_holes pending in
let evdref = ref current_sigma in
if flags.use_typeclasses then apply_typeclasses env evdref frozen false;
if Option.has_some flags.use_hook then
apply_inference_hook (Option.get flags.use_hook env) evdref pending;
- if flags.use_unif_heuristics then apply_heuristics env evdref false;
+ if flags.solve_unification_constraints then apply_heuristics env evdref false;
if flags.fail_evar then check_evars_are_solved env !evdref frozen pending;
!evdref
let check_evars_are_solved env current_sigma pending =
- let frozen = frozen_holes pending in
- let pending = pending_holes pending in
+ let frozen,pending = frozen_and_pending_holes pending in
check_evars_are_solved env current_sigma frozen pending
let process_inference_flags flags env initial_sigma (sigma,c) =
@@ -1102,14 +1109,14 @@ let ise_pretype_gen flags env sigma lvar kind c =
let default_inference_flags fail = {
use_typeclasses = true;
- use_unif_heuristics = true;
+ solve_unification_constraints = true;
use_hook = None;
fail_evar = fail;
expand_evars = true }
let no_classes_no_fail_inference_flags = {
use_typeclasses = false;
- use_unif_heuristics = true;
+ solve_unification_constraints = true;
use_hook = None;
fail_evar = false;
expand_evars = true }
@@ -1173,7 +1180,7 @@ let understand_ltac flags env sigma lvar kind c =
let constr_flags = {
use_typeclasses = true;
- use_unif_heuristics = true;
+ solve_unification_constraints = true;
use_hook = None;
fail_evar = true;
expand_evars = true }
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 824bb11aa4..0f3f7c3c9a 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -47,10 +47,12 @@ val empty_lvar : ltac_var_map
type glob_constr_ltac_closure = ltac_var_map * glob_constr
type pure_open_constr = evar_map * constr
+type inference_hook = env -> evar_map -> evar -> evar_map * constr
+
type inference_flags = {
use_typeclasses : bool;
- use_unif_heuristics : bool;
- use_hook : (env -> evar_map -> evar -> constr) option;
+ solve_unification_constraints : bool;
+ use_hook : inference_hook option;
fail_evar : bool;
expand_evars : bool
}
diff --git a/pretyping/program.ml b/pretyping/program.ml
index b4333847b7..62aedcfbf6 100644
--- a/pretyping/program.ml
+++ b/pretyping/program.ml
@@ -15,10 +15,12 @@ open Term
let make_dir l = DirPath.make (List.rev_map Id.of_string l)
let find_reference locstr dir s =
- let sp = Libnames.make_path (make_dir dir) (Id.of_string s) in
+ let dp = make_dir dir in
+ let sp = Libnames.make_path dp (Id.of_string s) in
try Nametab.global_of_path sp
with Not_found ->
- anomaly ~label:locstr (Pp.str "cannot find" ++ spc () ++ Libnames.pr_path sp)
+ user_err_loc (Loc.ghost, "", str "Library " ++ Libnames.pr_dirpath dp ++
+ str " has to be required first.")
let coq_reference locstr dir s = find_reference locstr ("Coq"::dir) s
let coq_constant locstr dir s = Universes.constr_of_global (coq_reference locstr dir s)
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 332d4e0b26..297f0a1a8e 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1262,7 +1262,7 @@ let sigma_compare_sorts env pb s0 s1 sigma =
match pb with
| Reduction.CONV -> Evd.set_eq_sort env sigma s0 s1
| Reduction.CUMUL -> Evd.set_leq_sort env sigma s0 s1
-
+
let sigma_compare_instances ~flex i0 i1 sigma =
try Evd.set_eq_instances ~flex sigma i0 i1
with Evd.UniversesDiffer
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli
index e4cca2679c..8ca40f829f 100644
--- a/pretyping/retyping.mli
+++ b/pretyping/retyping.mli
@@ -46,3 +46,5 @@ val type_of_global_reference_knowing_conclusion :
val sorts_of_context : env -> evar_map -> Context.Rel.t -> sorts list
val expand_projection : env -> evar_map -> Names.projection -> constr -> constr list -> constr
+
+val print_retype_error : retype_error -> Pp.std_ppcmds
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 31ef3dfdd7..b8da6b6852 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -65,7 +65,8 @@ type typeclass = {
cl_props : Context.Rel.t;
(* The method implementaions as projections. *)
- cl_projs : (Name.t * (direction * int option) option * constant option) list;
+ cl_projs : (Name.t * (direction * Vernacexpr.hint_info_expr) option
+ * constant option) list;
cl_strict : bool;
@@ -76,10 +77,9 @@ type typeclasses = typeclass Refmap.t
type instance = {
is_class: global_reference;
- is_pri: int option;
+ is_info: Vernacexpr.hint_info_expr;
(* Sections where the instance should be redeclared,
- -1 for discard, 0 for none, mutable to avoid redeclarations
- when multiple rebuild_object happen. *)
+ -1 for discard, 0 for none. *)
is_global: int;
is_poly: bool;
is_impl: global_reference;
@@ -89,15 +89,15 @@ type instances = (instance Refmap.t) Refmap.t
let instance_impl is = is.is_impl
-let instance_priority is = is.is_pri
+let hint_priority is = is.is_info.Vernacexpr.hint_priority
-let new_instance cl pri glob poly impl =
+let new_instance cl info glob poly impl =
let global =
if glob then Lib.sections_depth ()
else -1
in
{ is_class = cl.cl_impl;
- is_pri = pri ;
+ is_info = info ;
is_global = global ;
is_poly = poly;
is_impl = impl }
@@ -274,7 +274,9 @@ let check_instance env sigma c =
not (Evd.has_undefined evd)
with e when CErrors.noncritical e -> false
-let build_subclasses ~check env sigma glob pri =
+open Vernacexpr
+
+let build_subclasses ~check env sigma glob { hint_priority = pri } =
let _id = Nametab.basename_of_global glob in
let _next_id =
let i = ref (-1) in
@@ -297,24 +299,24 @@ let build_subclasses ~check env sigma glob pri =
match b with
| None -> None
| Some (Backward, _) -> None
- | Some (Forward, pri') ->
+ | Some (Forward, info) ->
let proj = Option.get proj in
let body = it_mkLambda_or_LetIn (mkApp (mkConstU (proj,u), projargs)) rels in
if check && check_instance env sigma body then None
else
- let pri =
- match pri, pri' with
+ let newpri =
+ match pri, info.hint_priority with
| Some p, Some p' -> Some (p + p')
| Some p, None -> Some (p + 1)
| _, _ -> None
in
- Some (ConstRef proj, pri, body)) tc.cl_projs
+ Some (ConstRef proj, { info with hint_priority = newpri }, body)) tc.cl_projs
in
- let declare_proj hints (cref, pri, body) =
+ let declare_proj hints (cref, info, body) =
let path' = cref :: path in
let ty = Retyping.get_type_of env sigma body in
let rest = aux pri body ty path' in
- hints @ (path', pri, body) :: rest
+ hints @ (path', info, body) :: rest
in List.fold_left declare_proj [] projs
in
let term = Universes.constr_of_global_univ (glob,Univ.UContext.instance ctx) in
@@ -368,11 +370,11 @@ let is_local i = Int.equal i.is_global (-1)
let add_instance check inst =
let poly = Global.is_polymorphic inst.is_impl in
add_instance_hint (IsGlobal inst.is_impl) [inst.is_impl] (is_local inst)
- inst.is_pri poly;
+ inst.is_info poly;
List.iter (fun (path, pri, c) -> add_instance_hint (IsConstr c) path
(is_local inst) pri poly)
(build_subclasses ~check:(check && not (isVarRef inst.is_impl))
- (Global.env ()) (Evd.from_env (Global.env ())) inst.is_impl inst.is_pri)
+ (Global.env ()) (Evd.from_env (Global.env ())) inst.is_impl inst.is_info)
let rebuild_instance (action, inst) =
let () = match action with
@@ -404,26 +406,22 @@ let remove_instance i =
Lib.add_anonymous_leaf (instance_input (RemoveInstance, i));
remove_instance_hint i.is_impl
-let declare_instance pri local glob =
+let declare_instance info local glob =
let ty = Global.type_of_global_unsafe glob in
+ let info = Option.default {hint_priority = None; hint_pattern = None} info in
match class_of_constr ty with
| Some (rels, ((tc,_), args) as _cl) ->
- add_instance (new_instance tc pri (not local) (Flags.use_polymorphic_flag ()) glob)
-(* let path, hints = build_subclasses (not local) (Global.env ()) Evd.empty glob in *)
-(* let entries = List.map (fun (path, pri, c) -> (pri, local, path, c)) hints in *)
-(* Auto.add_hints local [typeclasses_db] (Auto.HintsResolveEntry entries); *)
-(* Auto.add_hints local [typeclasses_db] *)
-(* (Auto.HintsCutEntry (PathSeq (PathStar (PathAtom PathAny), path))) *)
+ add_instance (new_instance tc info (not local) (Flags.use_polymorphic_flag ()) glob)
| None -> ()
let add_class cl =
add_class cl;
List.iter (fun (n, inst, body) ->
match inst with
- | Some (Backward, pri) ->
+ | Some (Backward, info) ->
(match body with
| None -> CErrors.error "Non-definable projection can not be declared as a subinstance"
- | Some b -> declare_instance pri false (ConstRef b))
+ | Some b -> declare_instance (Some info) false (ConstRef b))
| _ -> ())
cl.cl_projs
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 2530f5dfae..620bc367bd 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -32,7 +32,7 @@ type typeclass = {
Some may be undefinable due to sorting restrictions or simply undefined if
no name is provided. The [int option option] indicates subclasses whose hint has
the given priority. *)
- cl_projs : (Name.t * (direction * int option) option * constant option) list;
+ cl_projs : (Name.t * (direction * Vernacexpr.hint_info_expr) option * constant option) list;
(** Whether we use matching or full unification during resolution *)
cl_strict : bool;
@@ -50,7 +50,7 @@ val all_instances : unit -> instance list
val add_class : typeclass -> unit
-val new_instance : typeclass -> int option -> bool -> Decl_kinds.polymorphic ->
+val new_instance : typeclass -> Vernacexpr.hint_info_expr -> bool -> Decl_kinds.polymorphic ->
global_reference -> instance
val add_instance : instance -> unit
val remove_instance : instance -> unit
@@ -71,7 +71,7 @@ val class_of_constr : constr -> (Context.Rel.t * (typeclass puniverses * constr
val instance_impl : instance -> global_reference
-val instance_priority : instance -> int option
+val hint_priority : instance -> int option
val is_class : global_reference -> bool
val is_instance : global_reference -> bool
@@ -113,21 +113,22 @@ val classes_transparent_state : unit -> transparent_state
val add_instance_hint_hook :
(global_reference_or_constr -> global_reference list ->
- bool (* local? *) -> int option -> Decl_kinds.polymorphic -> unit) Hook.t
+ bool (* local? *) -> Vernacexpr.hint_info_expr -> Decl_kinds.polymorphic -> unit) Hook.t
val remove_instance_hint_hook : (global_reference -> unit) Hook.t
val add_instance_hint : global_reference_or_constr -> global_reference list ->
- bool -> int option -> Decl_kinds.polymorphic -> unit
+ bool -> Vernacexpr.hint_info_expr -> Decl_kinds.polymorphic -> unit
val remove_instance_hint : global_reference -> unit
val solve_all_instances_hook : (env -> evar_map -> evar_filter -> bool -> bool -> bool -> evar_map) Hook.t
val solve_one_instance_hook : (env -> evar_map -> types -> bool -> open_constr) Hook.t
-val declare_instance : int option -> bool -> global_reference -> unit
+val declare_instance : Vernacexpr.hint_info_expr option -> bool -> global_reference -> unit
(** Build the subinstances hints for a given typeclass object.
check tells if we should check for existence of the
subinstances and add only the missing ones. *)
-val build_subclasses : check:bool -> env -> evar_map -> global_reference -> int option (* priority *) ->
- (global_reference list * int option * constr) list
+val build_subclasses : check:bool -> env -> evar_map -> global_reference ->
+ Vernacexpr.hint_info_expr ->
+ (global_reference list * Vernacexpr.hint_info_expr * constr) list
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 6573bd238c..259318693f 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1220,7 +1220,7 @@ let is_mimick_head ts f =
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)
@@ -1270,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]
@@ -1297,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' =
@@ -1389,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
@@ -1450,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
@@ -1587,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
@@ -1879,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
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 18:11:30 +0000