summaryrefslogtreecommitdiff
path: root/plugins/subtac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/subtac')
-rw-r--r--plugins/subtac/eterm.ml17
-rw-r--r--plugins/subtac/g_subtac.ml44
-rw-r--r--plugins/subtac/subtac.ml4
-rw-r--r--plugins/subtac/subtac_cases.ml2
-rw-r--r--plugins/subtac/subtac_classes.ml9
-rw-r--r--plugins/subtac/subtac_coercion.ml107
-rw-r--r--plugins/subtac/subtac_command.ml2
-rw-r--r--plugins/subtac/subtac_obligations.ml25
-rw-r--r--plugins/subtac/subtac_pretyping.ml4
-rw-r--r--plugins/subtac/subtac_pretyping_F.ml33
-rw-r--r--plugins/subtac/subtac_utils.ml11
-rw-r--r--plugins/subtac/subtac_utils.mli1
12 files changed, 122 insertions, 97 deletions
diff --git a/plugins/subtac/eterm.ml b/plugins/subtac/eterm.ml
index 5ed335d0..f4d8b769 100644
--- a/plugins/subtac/eterm.ml
+++ b/plugins/subtac/eterm.ml
@@ -132,18 +132,29 @@ let rec chop_product n t =
| Prod (_, _, b) -> if noccurn 1 b then chop_product (pred n) (Termops.pop b) else None
| _ -> None
-let evar_dependencies evm ev =
+let evars_of_evar_info evi =
+ Intset.union (Evarutil.evars_of_term evi.evar_concl)
+ (Intset.union
+ (match evi.evar_body with
+ | Evar_empty -> Intset.empty
+ | Evar_defined b -> Evarutil.evars_of_term b)
+ (Evarutil.evars_of_named_context (evar_filtered_context evi)))
+
+let evar_dependencies evm oev =
let one_step deps =
Intset.fold (fun ev s ->
let evi = Evd.find evm ev in
- Intset.union (Evarutil.evars_of_evar_info evi) s)
+ let deps' = evars_of_evar_info evi in
+ if Intset.mem oev deps' then
+ raise (Invalid_argument ("Ill-formed evar map: cycle detected for evar " ^ string_of_int oev))
+ else Intset.union deps' s)
deps deps
in
let rec aux deps =
let deps' = one_step deps in
if Intset.equal deps deps' then deps
else aux deps'
- in aux (Intset.singleton ev)
+ in aux (Intset.singleton oev)
let move_after (id, ev, deps as obl) l =
let rec aux restdeps = function
diff --git a/plugins/subtac/g_subtac.ml4 b/plugins/subtac/g_subtac.ml4
index ca1240e5..6a131d39 100644
--- a/plugins/subtac/g_subtac.ml4
+++ b/plugins/subtac/g_subtac.ml4
@@ -75,14 +75,14 @@ type 'a gallina_loc_argtype = (Vernacexpr.vernac_expr located, 'a) Genarg.abstra
let (wit_subtac_gallina_loc : Genarg.tlevel gallina_loc_argtype),
(globwit_subtac_gallina_loc : Genarg.glevel gallina_loc_argtype),
(rawwit_subtac_gallina_loc : Genarg.rlevel gallina_loc_argtype) =
- Genarg.create_arg "subtac_gallina_loc"
+ Genarg.create_arg None "subtac_gallina_loc"
type 'a withtac_argtype = (Tacexpr.raw_tactic_expr option, 'a) Genarg.abstract_argument_type
let (wit_subtac_withtac : Genarg.tlevel withtac_argtype),
(globwit_subtac_withtac : Genarg.glevel withtac_argtype),
(rawwit_subtac_withtac : Genarg.rlevel withtac_argtype) =
- Genarg.create_arg "subtac_withtac"
+ Genarg.create_arg None "subtac_withtac"
VERNAC COMMAND EXTEND Subtac
[ "Program" subtac_gallina_loc(g) ] -> [ Subtac.subtac g ]
diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml
index 710149ae..d626396f 100644
--- a/plugins/subtac/subtac.ml
+++ b/plugins/subtac/subtac.ml
@@ -82,11 +82,9 @@ let start_proof_com env isevars sopt kind (bl,t) hook =
Impargs.declare_manual_implicits (loc = Local) gr ~enriching:true [imps];
hook loc gr)
-let print_subgoals () = Flags.if_verbose (fun () -> msg (Printer.pr_open_subgoals ())) ()
-
let start_proof_and_print env isevars idopt k t hook =
start_proof_com env isevars idopt k t hook;
- print_subgoals ()
+ Vernacentries.print_subgoals ()
let _ = Detyping.set_detype_anonymous (fun loc n -> GVar (loc, id_of_string ("Anonymous_REL_" ^ string_of_int n)))
diff --git a/plugins/subtac/subtac_cases.ml b/plugins/subtac/subtac_cases.ml
index 368d8bac..16d4e21e 100644
--- a/plugins/subtac/subtac_cases.ml
+++ b/plugins/subtac/subtac_cases.ml
@@ -1845,7 +1845,7 @@ let build_dependent_signature env evars avoid tomatchs arsign =
refl_arg :: refl_args,
pred slift,
(Name id, b, t) :: argsign'))
- (env, 0, [], [], slift, []) args argsign
+ (env, neqs, [], [], slift, []) args argsign
in
let eq = mk_JMeq
(lift (nargeqs + slift) appt)
diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml
index c08dd16d..6b3fe718 100644
--- a/plugins/subtac/subtac_classes.ml
+++ b/plugins/subtac/subtac_classes.ml
@@ -52,7 +52,7 @@ let type_ctx_instance evars env ctx inst subst =
| None -> interp_casted_constr_evars evars env (List.hd l) t', List.tl l
| Some b -> substl subst b, l
in
- evars := resolve_typeclasses ~onlyargs:true ~fail:true env !evars;
+ evars := resolve_typeclasses ~filter:Subtac_utils.no_goals_or_obligations ~fail:true env !evars;
let d = na, Some c', t' in
aux (c' :: subst, d :: instctx) l ctx
| [] -> subst
@@ -107,9 +107,10 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p
let i = Nameops.add_suffix (Classes.id_of_class k) "_instance_0" in
Namegen.next_global_ident_away i (Termops.ids_of_context env)
in
+ evars := resolve_typeclasses ~filter:Subtac_utils.no_goals_or_obligations ~fail:true env !evars;
+ let ctx = Evarutil.nf_rel_context_evar !evars ctx
+ and ctx' = Evarutil.nf_rel_context_evar !evars ctx' in
let env' = push_rel_context ctx env in
- evars := Evarutil.nf_evar_map !evars;
- evars := resolve_typeclasses ~onlyargs:false ~fail:true env !evars;
let sigma = !evars in
let subst = List.map (Evarutil.nf_evar sigma) subst in
let props =
@@ -157,6 +158,8 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p
Inl (type_ctx_instance evars (push_rel_context ctx' env') k.cl_props props subst)
in
evars := Evarutil.nf_evar_map !evars;
+ evars := resolve_typeclasses ~filter:Subtac_utils.no_goals_or_obligations ~fail:true env !evars;
+ evars := resolve_typeclasses ~filter:Typeclasses.no_goals ~fail:false env !evars;
let term, termtype =
match subst with
| Inl subst ->
diff --git a/plugins/subtac/subtac_coercion.ml b/plugins/subtac/subtac_coercion.ml
index 74f31a90..eb29bd04 100644
--- a/plugins/subtac/subtac_coercion.ml
+++ b/plugins/subtac/subtac_coercion.ml
@@ -27,6 +27,9 @@ open Subtac_errors
open Eterm
open Pp
+let app_opt env evars f t =
+ whd_betaiota !evars (app_opt f t)
+
let pair_of_array a = (a.(0), a.(1))
let make_name s = Name (id_of_string s)
@@ -80,7 +83,8 @@ module Coercion = struct
| Type _, Prop Null -> Prop Null
| _, Type _ -> s2
- let hnf env isevars c = whd_betadeltaiota env ( !isevars) c
+ let hnf env isevars c = whd_betadeltaiota env isevars c
+ let hnf_nodelta env evars c = whd_betaiota evars c
let lift_args n sign =
let rec liftrec k = function
@@ -90,15 +94,16 @@ module Coercion = struct
liftrec (List.length sign) sign
let rec mu env isevars t =
- let isevars = ref isevars in
let rec aux v =
- let v = hnf env isevars v in
+ let v = hnf env !isevars v in
match disc_subset v with
Some (u, p) ->
let f, ct = aux u in
+ let p = hnf env !isevars p in
(Some (fun x ->
- app_opt f (mkApp ((delayed_force sig_).proj1,
- [| u; p; x |]))),
+ app_opt env isevars
+ f (mkApp ((delayed_force sig_).proj1,
+ [| u; p; x |]))),
ct)
| None -> (None, v)
in aux t
@@ -106,9 +111,8 @@ module Coercion = struct
and coerce loc env isevars (x : Term.constr) (y : Term.constr)
: (Term.constr -> Term.constr) option
=
- let x = nf_evar ( !isevars) x and y = nf_evar ( !isevars) y in
let rec coerce_unify env x y =
- let x = hnf env isevars x and y = hnf env isevars y in
+ let x = hnf env !isevars x and y = hnf env !isevars y in
try
isevars := the_conv_x_leq env x y !isevars;
None
@@ -167,7 +171,7 @@ module Coercion = struct
let env' = push_rel (name', None, a') env in
let c1 = coerce_unify env' (lift 1 a') (lift 1 a) in
(* env, x : a' |- c1 : lift 1 a' > lift 1 a *)
- let coec1 = app_opt c1 (mkRel 1) in
+ let coec1 = app_opt env' isevars c1 (mkRel 1) in
(* env, x : a' |- c1[x] : lift 1 a *)
let c2 = coerce_unify env' (subst1 coec1 (liftn 1 2 b)) b' in
(* env, x : a' |- c2 : b[c1[x]/x]] > b' *)
@@ -177,7 +181,7 @@ module Coercion = struct
Some
(fun f ->
mkLambda (name', a',
- app_opt c2
+ app_opt env' isevars c2
(mkApp (Term.lift 1 f, [| coec1 |])))))
| App (c, l), App (c', l') ->
@@ -220,9 +224,9 @@ module Coercion = struct
Some
(fun x ->
let x, y =
- app_opt c1 (mkApp (existS.proj1,
+ app_opt env' isevars c1 (mkApp (existS.proj1,
[| a; pb; x |])),
- app_opt c2 (mkApp (existS.proj2,
+ app_opt env' isevars c2 (mkApp (existS.proj2,
[| a; pb; x |]))
in
mkApp (existS.intro, [| a'; pb'; x ; y |]))
@@ -240,9 +244,9 @@ module Coercion = struct
Some
(fun x ->
let x, y =
- app_opt c1 (mkApp (prod.proj1,
+ app_opt env isevars c1 (mkApp (prod.proj1,
[| a; b; x |])),
- app_opt c2 (mkApp (prod.proj2,
+ app_opt env isevars c2 (mkApp (prod.proj2,
[| a; b; x |]))
in
mkApp (prod.intro, [| a'; b'; x ; y |]))
@@ -276,7 +280,7 @@ module Coercion = struct
Some (u, p) ->
let c = coerce_unify env u y in
let f x =
- app_opt c (mkApp ((delayed_force sig_).proj1,
+ app_opt env isevars c (mkApp ((delayed_force sig_).proj1,
[| u; p; x |]))
in Some f
| None ->
@@ -285,7 +289,7 @@ module Coercion = struct
let c = coerce_unify env x u in
Some
(fun x ->
- let cx = app_opt c x in
+ let cx = app_opt env isevars c x in
let evar = make_existential loc env isevars (mkApp (p, [| cx |]))
in
(mkApp
@@ -300,7 +304,8 @@ module Coercion = struct
let coerce_itf loc env isevars v t c1 =
let evars = ref isevars in
let coercion = coerce loc env evars t c1 in
- !evars, Option.map (app_opt coercion) v
+ let t = Option.map (app_opt env evars coercion) v in
+ !evars, t
(* Taken from pretyping/coercion.ml *)
@@ -354,34 +359,36 @@ module Coercion = struct
with _ -> anomaly "apply_coercion"
let inh_app_fun env isevars j =
- let t = whd_betadeltaiota env ( isevars) j.uj_type in
+ let isevars = ref isevars in
+ let t = hnf env !isevars j.uj_type in
match kind_of_term t with
- | Prod (_,_,_) -> (isevars,j)
- | Evar ev when not (is_defined_evar isevars ev) ->
- let (isevars',t) = define_evar_as_product isevars ev in
+ | Prod (_,_,_) -> (!isevars,j)
+ | Evar ev when not (is_defined_evar !isevars ev) ->
+ let (isevars',t) = define_evar_as_product !isevars ev in
(isevars',{ uj_val = j.uj_val; uj_type = t })
| _ ->
(try
let t,p =
- lookup_path_to_fun_from env ( isevars) j.uj_type in
- (isevars,apply_coercion env ( isevars) p j t)
+ lookup_path_to_fun_from env !isevars j.uj_type in
+ (!isevars,apply_coercion env !isevars p j t)
with Not_found ->
try
let coercef, t = mu env isevars t in
- (isevars, { uj_val = app_opt coercef j.uj_val; uj_type = t })
+ let res = { uj_val = app_opt env isevars coercef j.uj_val; uj_type = t } in
+ (!isevars, res)
with NoSubtacCoercion | NoCoercion ->
- (isevars,j))
+ (!isevars,j))
let inh_tosort_force loc env isevars j =
try
let t,p = lookup_path_to_sort_from env ( isevars) j.uj_type in
let j1 = apply_coercion env ( isevars) p j t in
- (isevars,type_judgment env (j_nf_evar ( isevars) j1))
+ (isevars, type_judgment env (j_nf_evar ( isevars) j1))
with Not_found ->
error_not_a_type_loc loc env ( isevars) j
let inh_coerce_to_sort loc env isevars j =
- let typ = whd_betadeltaiota env ( isevars) j.uj_type in
+ let typ = hnf env isevars j.uj_type in
match kind_of_term typ with
| Sort s -> (isevars,{ utj_val = j.uj_val; utj_type = s })
| Evar ev when not (is_defined_evar isevars ev) ->
@@ -391,15 +398,19 @@ module Coercion = struct
inh_tosort_force loc env isevars j
let inh_coerce_to_base loc env isevars j =
- let typ = whd_betadeltaiota env ( isevars) j.uj_type in
+ let isevars = ref isevars in
+ let typ = hnf env !isevars j.uj_type in
let ct, typ' = mu env isevars typ in
- isevars, { uj_val = app_opt ct j.uj_val;
- uj_type = typ' }
+ let res =
+ { uj_val = app_opt env isevars ct j.uj_val;
+ uj_type = typ' }
+ in !isevars, res
let inh_coerce_to_prod loc env isevars t =
- let typ = whd_betadeltaiota env ( isevars) (snd t) in
+ let isevars = ref isevars in
+ let typ = hnf env !isevars (snd t) in
let _, typ' = mu env isevars typ in
- isevars, (fst t, typ')
+ !isevars, (fst t, typ')
let inh_coerce_to_fail env evd rigidonly v t c1 =
if rigidonly & not (Heads.is_rigid env c1 && Heads.is_rigid env t)
@@ -452,23 +463,23 @@ module Coercion = struct
(* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *)
let inh_conv_coerce_to_gen rigidonly loc env evd cj ((n, t) as _tycon) =
match n with
- None ->
- let (evd', val') =
- try
- inh_conv_coerce_to_fail loc env evd rigidonly
- (Some (nf_evar evd cj.uj_val))
- (nf_evar evd cj.uj_type) (nf_evar evd t)
- with NoCoercion ->
- let sigma = evd in
- try
- coerce_itf loc env evd (Some cj.uj_val) cj.uj_type t
- with NoSubtacCoercion ->
- error_actual_type_loc loc env sigma cj t
- in
- let val' = match val' with Some v -> v | None -> assert(false) in
- (evd',{ uj_val = val'; uj_type = t })
- | Some (init, cur) ->
- (evd, cj)
+ | None ->
+ let cj = { cj with uj_type = hnf_nodelta env evd cj.uj_type }
+ and t = hnf_nodelta env evd t in
+ let (evd', val') =
+ try
+ inh_conv_coerce_to_fail loc env evd rigidonly
+ (Some cj.uj_val) cj.uj_type t
+ with NoCoercion ->
+ (try
+ coerce_itf loc env evd (Some cj.uj_val) cj.uj_type t
+ with NoSubtacCoercion ->
+ error_actual_type_loc loc env evd cj t)
+ in
+ let val' = match val' with Some v -> v | None -> assert(false) in
+ (evd',{ uj_val = val'; uj_type = t })
+ | Some (init, cur) ->
+ (evd, cj)
let inh_conv_coerce_to = inh_conv_coerce_to_gen false
let inh_conv_coerce_rigid_to = inh_conv_coerce_to_gen true
diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml
index ecae6759..ced390aa 100644
--- a/plugins/subtac/subtac_command.ml
+++ b/plugins/subtac/subtac_command.ml
@@ -458,7 +458,7 @@ let interp_recursive fixkind l =
(* Instantiate evars and check all are resolved *)
let evd = Evarconv.consider_remaining_unif_problems env_rec !evdref in
let evd = Typeclasses.resolve_typeclasses
- ~onlyargs:true ~split:true ~fail:false env_rec evd
+ ~filter:Typeclasses.no_goals ~split:true ~fail:false env_rec evd
in
let evd = Evarutil.nf_evar_map evd in
let fixdefs = List.map (nf_evar evd) fixdefs in
diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml
index 64d9f72c..6a5878b3 100644
--- a/plugins/subtac/subtac_obligations.ml
+++ b/plugins/subtac/subtac_obligations.ml
@@ -445,12 +445,12 @@ let deps_remaining obls deps =
else x :: acc)
deps []
-let has_dependencies obls n =
- let res = ref false in
+let dependencies obls n =
+ let res = ref Intset.empty in
Array.iteri
(fun i obl ->
if i <> n && Intset.mem n obl.obl_deps then
- res := true)
+ res := Intset.add i !res)
obls;
!res
@@ -502,8 +502,9 @@ let rec solve_obligation prg num tac =
in
match res with
| Remain n when n > 0 ->
- if has_dependencies obls num then
- ignore(auto_solve_obligations (Some prg.prg_name) None)
+ let deps = dependencies obls num in
+ if deps <> Intset.empty then
+ ignore(auto_solve_obligations (Some prg.prg_name) None ~oblset:deps)
| _ -> ());
trace (str "Started obligation " ++ int user_num ++ str " proof: " ++
Subtac_utils.my_print_constr (Global.env ()) obl.obl_type);
@@ -553,14 +554,18 @@ and solve_obligation_by_tac prg obls i tac =
| Util.Anomaly _ as e -> raise e
| e -> false
-and solve_prg_obligations prg tac =
+and solve_prg_obligations prg ?oblset tac =
let obls, rem = prg.prg_obligations in
let rem = ref rem in
let obls' = Array.copy obls in
+ let p = match oblset with
+ | None -> (fun _ -> true)
+ | Some s -> (fun i -> Intset.mem i s)
+ in
let _ =
Array.iteri (fun i x ->
- if solve_obligation_by_tac prg obls' i tac then
- decr rem)
+ if p i && solve_obligation_by_tac prg obls' i tac then
+ decr rem)
obls'
in
update_obls prg obls' !rem
@@ -582,9 +587,9 @@ and try_solve_obligation n prg tac =
and try_solve_obligations n tac =
try ignore (solve_obligations n tac) with NoObligations _ -> ()
-and auto_solve_obligations n tac : progress =
+and auto_solve_obligations n ?oblset tac : progress =
Flags.if_verbose msgnl (str "Solving obligations automatically...");
- try solve_prg_obligations (get_prog_err n) tac with NoObligations _ -> Dependent
+ try solve_prg_obligations (get_prog_err n) ?oblset tac with NoObligations _ -> Dependent
open Pp
let show_obligations_of_prg ?(msg=true) prg =
diff --git a/plugins/subtac/subtac_pretyping.ml b/plugins/subtac/subtac_pretyping.ml
index 7c0d1232..e56fa4f5 100644
--- a/plugins/subtac/subtac_pretyping.ml
+++ b/plugins/subtac/subtac_pretyping.ml
@@ -67,8 +67,8 @@ let interp env isevars c tycon =
let _ = isevars := Evarutil.nf_evar_map !isevars in
let evd = consider_remaining_unif_problems env !isevars in
(* let unevd = undefined_evars evd in *)
- let unevd' = Typeclasses.resolve_typeclasses ~onlyargs:true ~split:true ~fail:true env evd in
- let unevd' = Typeclasses.resolve_typeclasses ~onlyargs:false ~split:true ~fail:false env unevd' in
+ let unevd' = Typeclasses.resolve_typeclasses ~filter:Subtac_utils.no_goals_or_obligations ~split:true ~fail:true env evd in
+ let unevd' = Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars ~split:true ~fail:false env unevd' in
let evm = unevd' in
isevars := unevd';
nf_evar evm j.uj_val, nf_evar evm j.uj_type
diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml
index d5d427c7..9a4e1883 100644
--- a/plugins/subtac/subtac_pretyping_F.ml
+++ b/plugins/subtac/subtac_pretyping_F.ml
@@ -88,7 +88,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
(* coerce to tycon if any *)
let inh_conv_coerce_to_tycon loc env evdref j = function
- | None -> j_nf_evar !evdref j
+ | None -> j
| Some t -> evd_comb2 (Coercion.inh_conv_coerce_to loc env) evdref j t
let push_rels vars env = List.fold_right push_rel vars env
@@ -323,7 +323,9 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
else tycon
in
match ty with
- | Some (_, t) when Subtac_coercion.disc_subset t = None -> ty
+ | Some (_, t) ->
+ if Subtac_coercion.disc_subset (whd_betadeltaiota env !evdref t) = None then ty
+ else None
| _ -> None
in
let fj = pretype ftycon env evdref lvar f in
@@ -340,13 +342,12 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
Coercion.inh_conv_coerces_to loc env !evdref resty ty) tycon;
let evd, (_, _, tycon) = split_tycon loc env !evdref tycon in
evdref := evd;
- let hj = pretype (mk_tycon (nf_evar !evdref c1)) env evdref lvar c in
+ let hj = pretype (mk_tycon c1) env evdref lvar c in
let value, typ = applist (j_val resj, [j_val hj]), subst1 hj.uj_val c2 in
- let typ' = nf_evar !evdref typ in
apply_rec env (n+1)
- { uj_val = nf_evar !evdref value;
- uj_type = nf_evar !evdref typ' }
- (Option.map (fun (abs, c) -> abs, nf_evar !evdref c) tycon) rest
+ { uj_val = value;
+ uj_type = typ }
+ (Option.map (fun (abs, c) -> abs, c) tycon) rest
| _ ->
let hj = pretype empty_tycon env evdref lvar c in
@@ -354,9 +355,9 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
(join_loc floc argloc) env !evdref
resj [hj]
in
- let resj = j_nf_evar !evdref (apply_rec env 1 fj ftycon args) in
+ let resj = apply_rec env 1 fj ftycon args in
let resj =
- match kind_of_term resj.uj_val with
+ match kind_of_term (whd_evar !evdref resj.uj_val) with
| App (f,args) when isInd f or isConst f ->
let sigma = !evdref in
let c = mkApp (f,Array.map (whd_evar sigma) args) in
@@ -508,10 +509,9 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in
let pred = nf_evar !evdref pred in
let p = nf_evar !evdref p in
- (* msgnl (str "Pred is: " ++ Termops.print_constr_env env pred);*)
let f cs b =
let n = rel_context_length cs.cs_args in
- let pi = lift n pred in (* liftn n 2 pred ? *)
+ let pi = lift n pred in
let pi = beta_applist (pi, [build_dependent_constructor cs]) in
let csgn =
if not !allow_anonymous_refs then
@@ -525,7 +525,6 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
cs.cs_args
in
let env_c = push_rels csgn env in
-(* msgnl (str "Pi is: " ++ Termops.print_constr_env env_c pi); *)
let bj = pretype (mk_tycon pi) env_c evdref lvar b in
it_mkLambda_or_LetIn bj.uj_val cs.cs_args in
let b1 = f cstrs.(0) b1 in
@@ -551,8 +550,6 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
| CastConv (k,t) ->
let tj = pretype_type empty_valcon env evdref lvar t in
let cj = pretype (mk_tycon tj.utj_val) env evdref lvar c in
- (* User Casts are for helping pretyping, experimentally not to be kept*)
- (* ... except for Correctness *)
let v = mkCast (cj.uj_val, k, tj.utj_val) in
{ uj_val = v; uj_type = tj.utj_val }
in
@@ -600,9 +597,9 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
in
if resolve_classes then
(try
- evdref := Typeclasses.resolve_typeclasses ~onlyargs:true
+ evdref := Typeclasses.resolve_typeclasses ~filter:Subtac_utils.no_goals_or_obligations
~split:true ~fail:true env !evdref;
- evdref := Typeclasses.resolve_typeclasses ~onlyargs:false
+ evdref := Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars
~split:true ~fail:false env !evdref
with e -> if fail_evar then raise e else ());
evdref := consider_remaining_unif_problems env !evdref;
@@ -647,8 +644,8 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
let understand_type sigma env c =
snd (ise_pretype_gen true false true sigma env ([],[]) IsType c)
- let understand_ltac expand_evar sigma env lvar kind c =
- ise_pretype_gen expand_evar false true sigma env lvar kind c
+ let understand_ltac ?(resolve_classes=false) expand_evar sigma env lvar kind c =
+ ise_pretype_gen expand_evar false resolve_classes sigma env lvar kind c
let understand_tcc ?(resolve_classes=true) sigma env ?expected_type:exptyp c =
ise_pretype_gen true false resolve_classes sigma env ([],[]) (OfType exptyp) c
diff --git a/plugins/subtac/subtac_utils.ml b/plugins/subtac/subtac_utils.ml
index 28bbdd35..fbb44811 100644
--- a/plugins/subtac/subtac_utils.ml
+++ b/plugins/subtac/subtac_utils.ml
@@ -161,12 +161,11 @@ let print_args env args =
Array.fold_right (fun a acc -> my_print_constr env a ++ spc () ++ acc) args (str "")
let make_existential loc ?(opaque = Define true) env isevars c =
- let evar = Evarutil.e_new_evar isevars env ~src:(loc, QuestionMark opaque) c in
- let (key, args) = destEvar evar in
- (try trace (str "Constructed evar " ++ int key ++ str " applied to args: " ++
- print_args env args ++ str " for type: "++
- my_print_constr env c) with _ -> ());
- evar
+ Evarutil.e_new_evar isevars env ~src:(loc, QuestionMark opaque) c
+
+let no_goals_or_obligations = function
+ | GoalEvar | QuestionMark _ -> false
+ | _ -> true
let make_existential_expr loc env c =
let key = Evarutil.new_untyped_evar () in
diff --git a/plugins/subtac/subtac_utils.mli b/plugins/subtac/subtac_utils.mli
index de96cc60..112b1795 100644
--- a/plugins/subtac/subtac_utils.mli
+++ b/plugins/subtac/subtac_utils.mli
@@ -82,6 +82,7 @@ val app_opt : ('a -> 'a) option -> 'a -> 'a
val print_args : env -> constr array -> std_ppcmds
val make_existential : loc -> ?opaque:obligation_definition_status ->
env -> evar_map ref -> types -> constr
+val no_goals_or_obligations : Typeclasses.evar_filter
val make_existential_expr : loc -> 'a -> 'b -> constr_expr
val string_of_hole_kind : hole_kind -> string
val evars_of_term : evar_map -> evar_map -> constr -> evar_map
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 22:15:23 +0000