diff options
Diffstat (limited to 'tactics/class_tactics.ml')
| -rw-r--r-- | tactics/class_tactics.ml | 54 |
1 files changed, 16 insertions, 38 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 73b649e5..29797240 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -18,6 +18,7 @@ open CErrors open Util open Names open Term +open Constr open Termops open EConstr open Tacmach @@ -206,7 +207,7 @@ let clenv_unique_resolver_tac with_evars ~flags clenv' = try Proofview.tclUNIT (clenv_unique_resolver ~flags clenv' gls) with e -> Proofview.tclZERO e in resolve >>= fun clenv' -> - Clenvtac.clenv_refine with_evars ~with_classes:false clenv' + Clenvtac.clenv_refine ~with_evars ~with_classes:false clenv' end let unify_e_resolve poly flags = begin fun gls (c,_,clenv) -> @@ -226,7 +227,7 @@ let unify_resolve_refine poly flags gls ((c, t, ctx),n,clenv) = Refine.refine ~typecheck:false begin fun sigma -> let sigma, term, ty = if poly then - let (subst, ctx) = Universes.fresh_universe_context_set_instance ctx in + let (subst, ctx) = UnivGen.fresh_universe_context_set_instance ctx in let map c = Vars.subst_univs_level_constr subst c in let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in sigma, map c, map t @@ -476,7 +477,7 @@ let is_Prop env sigma concl = match EConstr.kind sigma ty with | Sort s -> begin match ESorts.kind sigma s with - | Prop Null -> true + | Prop -> true | _ -> false end | _ -> false @@ -546,12 +547,7 @@ let make_resolve_hyp env sigma st flags only_classes pri decl = let hints = build_subclasses ~check:false env sigma (VarRef id) empty_hint_info in (List.map_append (fun (path,info,c) -> - let info = - { info with Vernacexpr.hint_pattern = - Option.map (Constrintern.intern_constr_pattern env sigma) - info.Vernacexpr.hint_pattern } - in - make_resolves env sigma ~name:(PathHints path) + make_resolves env sigma ~name:(PathHints path) (true,false,not !Flags.quiet) info false (IsConstr (EConstr.of_constr c,Univ.ContextSet.empty))) hints) @@ -653,17 +649,6 @@ module Search = struct Evd.add sigma gl evi') sigma goals - let fail_if_nonclass info = - Proofview.Goal.enter begin fun gl -> - let sigma = Proofview.Goal.sigma gl in - if is_class_type sigma (Proofview.Goal.concl gl) then - Proofview.tclUNIT () - else (if !typeclasses_debug > 1 then - Feedback.msg_debug (pr_depth info.search_depth ++ - str": failure due to non-class subgoal " ++ - pr_ev sigma (Proofview.Goal.goal gl)); - Proofview.tclZERO NoApplicableEx) end - (** The general hint application tactic. tac1 + tac2 .... The choice of OR or ORELSE is determined depending on the dependencies of the goal and the unique/Prop @@ -708,8 +693,9 @@ module Search = struct let msg = match fst ie with | Pretype_errors.PretypeError (env, evd, Pretype_errors.CannotUnify (x,y,_)) -> - str"Cannot unify " ++ print_constr_env env evd x ++ str" and " ++ - print_constr_env env evd y + str"Cannot unify " ++ + Printer.pr_econstr_env env evd x ++ str" and " ++ + Printer.pr_econstr_env env evd y | ReachedLimitEx -> str "Proof-search reached its limit." | NoApplicableEx -> str "Proof-search failed." | e -> CErrors.iprint ie @@ -802,13 +788,8 @@ module Search = struct in if path_matches derivs [] then aux e tl else - let filter = - if false (* in 8.6, still allow non-class subgoals - info.search_only_classes *) then fail_if_nonclass info - else Proofview.tclUNIT () - in ortac - (with_shelf (tac <*> filter) >>= fun s -> + (with_shelf tac >>= fun s -> let i = !idx in incr idx; result s i None) (fun e' -> if CErrors.noncritical (fst e') then @@ -872,12 +853,9 @@ module Search = struct let search_tac_gl ?st only_classes dep hints depth i sigma gls gl : unit Proofview.tactic = let open Proofview in - if false (* In 8.6, still allow non-class goals only_classes && not (is_class_type sigma (Goal.concl gl)) *) then - Tacticals.New.tclZEROMSG (str"Not a subgoal for a class") - else - let dep = dep || Proofview.unifiable sigma (Goal.goal gl) gls in - let info = make_autogoal ?st only_classes dep (cut_of_hints hints) i gl in - search_tac hints depth 1 info + let dep = dep || Proofview.unifiable sigma (Goal.goal gl) gls in + let info = make_autogoal ?st only_classes dep (cut_of_hints hints) i gl in + search_tac hints depth 1 info let search_tac ?(st=full_transparent_state) only_classes dep hints depth = let open Proofview in @@ -1030,8 +1008,8 @@ module Intpart = Unionfind.Make(Evar.Set)(Evar.Map) let deps_of_constraints cstrs evm p = List.iter (fun (_, _, x, y) -> - let evx = Evarutil.undefined_evars_of_term evm (EConstr.of_constr x) in - let evy = Evarutil.undefined_evars_of_term evm (EConstr.of_constr y) in + let evx = Evarutil.undefined_evars_of_term evm x in + let evy = Evarutil.undefined_evars_of_term evm y in Intpart.union_set (Evar.Set.union evx evy) p) cstrs @@ -1076,7 +1054,7 @@ let error_unresolvable env comp evd = | Some s -> Evar.Set.mem ev s in let fold ev evi (found, accu) = - let ev_class = class_of_constr evd (EConstr.of_constr evi.evar_concl) in + let ev_class = class_of_constr evd evi.evar_concl in if not (Option.is_empty ev_class) && is_part ev then (* focus on one instance if only one was searched for *) if not found then (true, Some ev) @@ -1174,7 +1152,7 @@ let solve_inst env evd filter unique split fail = let _ = Hook.set Typeclasses.solve_all_instances_hook solve_inst -let resolve_one_typeclass env ?(sigma=Evd.empty) gl unique = +let resolve_one_typeclass env ?(sigma=Evd.from_env env) gl unique = let nc, gl, subst, _ = Evarutil.push_rel_context_to_named_context env sigma gl in let (gl,t,sigma) = Goal.V82.mk_goal sigma nc gl Store.empty in |