aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--interp/constrintern.ml2
-rw-r--r--pretyping/coercion.ml2
-rw-r--r--pretyping/pretyping.ml10
-rw-r--r--pretyping/typeclasses.ml13
-rw-r--r--pretyping/typeclasses.mli10
-rw-r--r--pretyping/unification.ml2
-rw-r--r--proofs/clenvtac.ml2
-rw-r--r--proofs/goal.ml4
-rw-r--r--proofs/goal.mli2
-rw-r--r--tactics/auto.ml21
-rw-r--r--tactics/class_tactics.ml422
-rw-r--r--tactics/refine.ml2
-rw-r--r--toplevel/classes.ml6
-rw-r--r--toplevel/command.ml7
14 files changed, 65 insertions, 40 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 5a8dcac08..304712675 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1854,7 +1854,7 @@ let interp_rawcontext_gen understand_type understand_judgment env bl =
(push_rel d env, d::params, succ n, impls)
| Some b ->
let c = understand_judgment env b in
- let d = (na, Some c.uj_val, c.uj_type) in
+ let d = (na, Some c.uj_val, Termops.refresh_universes c.uj_type) in
(push_rel d env, d::params, succ n, impls))
(env,[],1,[]) (List.rev bl)
in (env, par), impls
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 34eb92fa0..524d9d058 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -323,7 +323,7 @@ let coerce_itf loc env isevars v t c1 =
let saturate_evd env evd =
Typeclasses.resolve_typeclasses
- ~with_goals:false ~split:true ~fail:false env evd
+ ~filter:Typeclasses.no_goals ~split:true ~fail:false env evd
(* appliquer le chemin de coercions p à hj *)
let apply_coercion env sigma p hj typ_cl =
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 4eeb50cd0..bcd2a1ad1 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -109,8 +109,14 @@ let interp_elimination_sort = function
let resolve_evars env evdref fail_evar resolve_classes =
if resolve_classes then
- (evdref := Typeclasses.resolve_typeclasses ~with_goals:false
- ~split:true ~fail:fail_evar env !evdref);
+ (evdref := Typeclasses.resolve_typeclasses
+ ~filter:(if Flags.is_program_mode ()
+ then Typeclasses.no_goals_or_obligations else Typeclasses.no_goals)
+ ~split:true ~fail:fail_evar env !evdref;
+ if Flags.is_program_mode () then (* Try optionally solving the obligations *)
+ evdref := Typeclasses.resolve_typeclasses
+ ~filter:Typeclasses.all_evars ~split:true ~fail:false env !evdref;
+ );
(* Resolve eagerly, potentially making wrong choices *)
evdref := (try consider_remaining_unif_problems
~ts:(Typeclasses.classes_transparent_state ()) env !evdref
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index d76fdc85d..db03112c2 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -500,6 +500,15 @@ let has_typeclasses evd =
let solve_instanciations_problem = ref (fun _ _ _ _ _ -> assert false)
-let resolve_typeclasses ?(with_goals=false) ?(split=true) ?(fail=true) env evd =
+open Evar_kinds
+type evar_filter = Evar_kinds.t -> bool
+
+let all_evars _ = true
+let no_goals = function GoalEvar -> false | _ -> true
+let no_goals_or_obligations = function
+ | GoalEvar | QuestionMark _ -> false
+ | _ -> true
+
+let resolve_typeclasses ?(filter=no_goals) ?(split=true) ?(fail=true) env evd =
if not (has_typeclasses evd) then evd
- else !solve_instanciations_problem env evd with_goals split fail
+ else !solve_instanciations_problem env evd filter split fail
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 411651afe..b51732547 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -87,7 +87,13 @@ val mark_resolvable : evar_info -> evar_info
val mark_resolvables : evar_map -> evar_map
val is_class_evar : evar_map -> evar_info -> bool
-val resolve_typeclasses : ?with_goals:bool -> ?split:bool -> ?fail:bool ->
+(** Filter which evars to consider for resolution. *)
+type evar_filter = Evar_kinds.t -> bool
+val all_evars : evar_filter
+val no_goals : evar_filter
+val no_goals_or_obligations : evar_filter
+
+val resolve_typeclasses : ?filter:evar_filter -> ?split:bool -> ?fail:bool ->
env -> evar_map -> evar_map
val resolve_one_typeclass : env -> evar_map -> types -> open_constr
@@ -102,7 +108,7 @@ val register_remove_instance_hint : (global_reference -> unit) -> unit
val add_instance_hint : constr -> bool -> int option -> unit
val remove_instance_hint : global_reference -> unit
-val solve_instanciations_problem : (env -> evar_map -> bool -> bool -> bool -> evar_map) ref
+val solve_instanciations_problem : (env -> evar_map -> evar_filter -> bool -> bool -> evar_map) ref
val solve_instanciation_problem : (env -> evar_map -> types -> open_constr) ref
val declare_instance : int option -> bool -> global_reference -> unit
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index fd40cca7c..eec9b0bc3 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -967,7 +967,7 @@ let check_types env flags (sigma,_,_ as subst) m n =
let try_resolve_typeclasses env evd flags m n =
if flags.resolve_evars then
- try Typeclasses.resolve_typeclasses ~with_goals:false ~split:false
+ try Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals ~split:false
~fail:true env evd
with e when Typeclasses_errors.unsatisfiable_exception e ->
error_cannot_unify env evd (m, n)
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 3eb665088..3def44178 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -72,7 +72,7 @@ let clenv_refine with_evars ?(with_classes=true) clenv gls =
let clenv = clenv_pose_dependent_evars with_evars clenv in
let evd' =
if with_classes then
- Typeclasses.resolve_typeclasses ~with_goals:true
+ Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars
~fail:(not with_evars) clenv.env clenv.evd
else clenv.evd
in
diff --git a/proofs/goal.ml b/proofs/goal.ml
index cef43c443..9b3e90198 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -162,8 +162,8 @@ module Refinable = struct
(* spiwack: it is not very fine grain since it solves all typeclasses holes,
not only those containing the current goal, or a given term. But it
seems to fit our needs so far. *)
- let resolve_typeclasses ?with_goals ?split ?(fail=false) () env rdefs _ _ =
- rdefs:=Typeclasses.resolve_typeclasses ?with_goals ?split ~fail env !rdefs;
+ let resolve_typeclasses ?filter ?split ?(fail=false) () env rdefs _ _ =
+ rdefs:=Typeclasses.resolve_typeclasses ?filter ?split ~fail env !rdefs;
()
diff --git a/proofs/goal.mli b/proofs/goal.mli
index acda9031b..622ceea74 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -72,7 +72,7 @@ module Refinable : sig
(* [with_type c typ] constrains term [c] to have type [typ]. *)
val with_type : Term.constr -> Term.types -> Term.constr sensitive
- val resolve_typeclasses : ?with_goals:bool -> ?split:bool -> ?fail:bool -> unit -> unit sensitive
+ val resolve_typeclasses : ?filter:Typeclasses.evar_filter -> ?split:bool -> ?fail:bool -> unit -> unit sensitive
(* [constr_of_raw h check_type resolve_classes] is a pretyping function.
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 96cef72b4..0486eec58 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -281,13 +281,19 @@ let rec pp_hints_path = function
| PathEmpty -> str"Ø"
| PathEpsilon -> str"ε"
-let rec subst_hints_path subst hp =
- match hp with
- | PathAtom PathAny -> hp
- | PathAtom (PathHints grs) ->
+let subst_path_atom subst p =
+ match p with
+ | PathAny -> p
+ | PathHints grs ->
let gr' gr = fst (subst_global subst gr) in
let grs' = list_smartmap gr' grs in
- if grs' == grs then hp else PathAtom (PathHints grs')
+ if grs' == grs then p else PathHints grs'
+
+let rec subst_hints_path subst hp =
+ match hp with
+ | PathAtom p ->
+ let p' = subst_path_atom subst p in
+ if p' == p then hp else PathAtom p'
| PathStar p -> let p' = subst_hints_path subst p in
if p' == p then hp else PathStar p'
| PathSeq (p, q) ->
@@ -681,9 +687,10 @@ let subst_autohint (subst,(local,name,hintlist as obj)) =
let tac' = !forward_subst_tactic subst tac in
if tac==tac' then data.code else Extern tac'
in
+ let name' = subst_path_atom subst data.name in
let data' =
- if data.pat==pat' && data.code==code' then data
- else { data with pat = pat'; code = code' }
+ if data.pat==pat' && data.name == name' && data.code==code' then data
+ else { data with pat = pat'; name = name'; code = code' }
in
if k' == k && data' == data then hint else (k',data')
in
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 4553a8fa5..c8fe1a426 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -680,25 +680,21 @@ let resolve_all_evars debug m env p oevd do_split fail =
docomp evd comps
in docomp oevd split
-let initial_select_evars with_goals =
- if with_goals then
- (fun evd ev evi ->
- Typeclasses.is_class_evar evd evi)
- else
- (fun evd ev evi ->
- (snd (Evd.evar_source ev evd) <> Evar_kinds.GoalEvar)
- && Typeclasses.is_class_evar evd evi)
-
-let resolve_typeclass_evars debug m env evd with_goals split fail =
+let initial_select_evars filter =
+ fun evd ev evi ->
+ filter (snd evi.Evd.evar_source) &&
+ Typeclasses.is_class_evar evd evi
+
+let resolve_typeclass_evars debug m env evd filter split fail =
let evd =
try Evarconv.consider_remaining_unif_problems
~ts:(Typeclasses.classes_transparent_state ()) env evd
with _ -> evd
in
- resolve_all_evars debug m env (initial_select_evars with_goals) evd split fail
+ resolve_all_evars debug m env (initial_select_evars filter) evd split fail
-let solve_inst debug depth env evd with_goals split fail =
- resolve_typeclass_evars debug depth env evd with_goals split fail
+let solve_inst debug depth env evd filter split fail =
+ resolve_typeclass_evars debug depth env evd filter split fail
let _ =
Typeclasses.solve_instanciations_problem :=
diff --git a/tactics/refine.ml b/tactics/refine.ml
index 93c4ea57c..07480fc00 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -389,7 +389,7 @@ let rec tcc_aux subst (TH (c,mm,sgp) as _th) gl =
let refine (evd,c) gl =
let sigma = project gl in
- let evd = Typeclasses.resolve_typeclasses ~with_goals:false (pf_env gl) evd in
+ let evd = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals (pf_env gl) evd in
let c = Evarutil.nf_evar evd c in
let (evd,c) = Evarutil.evars_to_metas sigma (evd,c) in
(* Relies on Cast's put on Meta's by evars_to_metas, because it is otherwise
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index b4e44e7d3..dfbc95356 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -172,7 +172,7 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
in
let env' = push_rel_context ctx env in
evars := Evarutil.nf_evar_map !evars;
- evars := resolve_typeclasses ~with_goals:false ~fail:true env !evars;
+ evars := resolve_typeclasses ~filter:Typeclasses.no_goals ~fail:true env !evars;
let sigma = !evars in
let subst = List.map (Evarutil.nf_evar sigma) subst in
if abstract then
@@ -262,10 +262,10 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
in
let _ =
evars := Evarutil.nf_evar_map !evars;
- evars := Typeclasses.resolve_typeclasses ~with_goals:false ~fail:true
+ evars := Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals_or_obligations ~fail:true
env !evars;
(* Try resolving fields that are typeclasses automatically. *)
- evars := Typeclasses.resolve_typeclasses ~with_goals:true ~fail:false
+ evars := Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:false
env !evars
in
let termtype = Evarutil.nf_evar !evars termtype in
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 2f5ed1181..3191279ce 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -290,7 +290,7 @@ let interp_mutual_inductive (paramsl,indl) notations finite =
(* Instantiate evars and check all are resolved *)
let evd = consider_remaining_unif_problems env_params !evdref in
- let evd = Typeclasses.resolve_typeclasses ~with_goals:false ~fail:true env_params evd in
+ let evd = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals ~fail:true env_params evd in
let sigma = evd in
let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map (nf_evar sigma) cl,impsl)) constructors in
let ctx_params = Sign.map_rel_context (nf_evar sigma) ctx_params in
@@ -781,7 +781,7 @@ let interp_recursive isfix fixl notations =
(env,rec_sign,evd), (fixnames,fixdefs,fixtypes), list_combine3 fixctxnames fiximps fixannots
let check_recursive isfix ((env,rec_sign,evd),(fixnames,fixdefs,fixtypes),info) =
- let evd = Typeclasses.resolve_typeclasses ~with_goals:false ~fail:true env evd in
+ let evd = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals ~fail:true env evd in
List.iter (Option.iter (check_evars (push_named_context rec_sign env) Evd.empty evd)) fixdefs;
List.iter (check_evars env Evd.empty evd) fixtypes;
if not (List.mem None fixdefs) then begin
@@ -889,7 +889,8 @@ let do_program_recursive fixkind fixl ntns =
in
(* Program-specific code *)
(* Get the interesting evars, those that were not instanciated *)
- let evd = Typeclasses.resolve_typeclasses ~with_goals:false ~fail:true env evd in
+ let evd = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals_or_obligations ~fail:true env evd in
+ let evd = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals ~fail:false env evd in
(* Solve remaining evars *)
let rec collect_evars id def typ imps =
(* Generalize by the recursive prototypes *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 21:57:26 +0000