aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/auto.ml2
-rw-r--r--tactics/class_tactics.ml48
-rw-r--r--tactics/eqschemes.ml2
-rw-r--r--tactics/equality.ml2
-rw-r--r--tactics/hints.ml2
-rw-r--r--tactics/hipattern.ml10
-rw-r--r--tactics/tacticals.ml6
-rw-r--r--tactics/tactics.ml8
8 files changed, 48 insertions, 32 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml
index b76c0a96ae..e213965485 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -139,7 +139,7 @@ let conclPattern concl pat tac =
try
Proofview.tclUNIT (Constr_matching.matches env sigma pat concl)
with Constr_matching.PatternMatchingFailure ->
- Tacticals.New.tclZEROMSG (str "conclPattern")
+ Tacticals.New.tclZEROMSG (str "pattern-matching failed")
in
Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 46d66b9d06..672f9cffb5 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -226,16 +226,22 @@ let e_give_exact flags poly (c,clenv) =
Sigma.Unsafe.of_pair (Clenvtac.unify ~flags t1 <*> exact_no_check c, sigma)
end }
+let clenv_unique_resolver_tac with_evars ~flags clenv' =
+ Proofview.Goal.enter { enter = begin fun gls ->
+ let resolve =
+ 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'
+ end }
+
let unify_e_resolve poly flags = { enter = begin fun gls (c,_,clenv) ->
let clenv', c = connect_hint_clenv poly c clenv gls in
- let clenv' = clenv_unique_resolver ~flags clenv' gls in
- Clenvtac.clenv_refine true ~with_classes:false clenv'
- end }
+ clenv_unique_resolver_tac true ~flags clenv' end }
let unify_resolve poly flags = { enter = begin fun gls (c,_,clenv) ->
let clenv', _ = connect_hint_clenv poly c clenv gls in
- let clenv' = clenv_unique_resolver ~flags clenv' gls in
- Clenvtac.clenv_refine false ~with_classes:false clenv'
+ clenv_unique_resolver_tac false ~flags clenv'
end }
(** Application of a lemma using [refine] instead of the old [w_unify] *)
@@ -691,7 +697,7 @@ module V85 = struct
let merge_failures x y =
match x, y with
| _, ReachedLimit
- | ReachedLimit, _ -> ReachedLimit
+ | ReachedLimit, _ -> ReachedLimit
| NotApplicable, NotApplicable -> NotApplicable
let or_tac (x : 'a tac) (y : 'a tac) : 'a tac =
@@ -1004,9 +1010,9 @@ module Search = struct
(** In the proof engine failures are represented as exceptions *)
exception ReachedLimitEx
- exception NotApplicableEx
+ exception NoApplicableEx
- (** ReachedLimitEx has priority over NotApplicableEx to handle
+ (** ReachedLimitEx has priority over NoApplicableEx to handle
iterative deepening: it should fail when no hints are applicable,
but go to a deeper depth otherwise. *)
let merge_exceptions e e' =
@@ -1042,7 +1048,7 @@ module Search = struct
Feedback.msg_debug (pr_depth info.search_depth ++
str": failure due to non-class subgoal " ++
pr_ev sigma (Proofview.Goal.goal gl));
- Proofview.tclZERO NotApplicableEx) }
+ Proofview.tclZERO NoApplicableEx) }
(** The general hint application tactic.
tac1 + tac2 .... The choice of OR or ORELSE is determined
@@ -1078,14 +1084,24 @@ module Search = struct
let derivs = path_derivate info.search_cut name in
let pr_error ie =
if !typeclasses_debug > 1 then
- let msg =
- pr_depth (!idx :: info.search_depth) ++ str": " ++
+ let idx = if fst ie == NoApplicableEx then pred !idx else !idx in
+ let header =
+ pr_depth (idx :: info.search_depth) ++ str": " ++
Lazy.force pp ++
(if !foundone != true then
str" on" ++ spc () ++ pr_ev s (Proofview.Goal.goal (Proofview.Goal.assume gl))
else mt ())
in
- Feedback.msg_debug (msg ++ str " failed with " ++ CErrors.iprint ie)
+ 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
+ | ReachedLimitEx -> str "Proof-search reached its limit."
+ | NoApplicableEx -> str "Proof-search failed."
+ | e -> CErrors.iprint ie
+ in
+ Feedback.msg_debug (header ++ str " failed with: " ++ msg)
else ()
in
let tac_of gls i j = Goal.enter { enter = fun gl' ->
@@ -1196,10 +1212,10 @@ module Search = struct
str" possibilities");
match e with
| (ReachedLimitEx,ie) -> Proofview.tclZERO ~info:ie ReachedLimitEx
- | (_,ie) -> Proofview.tclZERO ~info:ie NotApplicableEx
+ | (_,ie) -> Proofview.tclZERO ~info:ie NoApplicableEx
in
- if backtrack then aux (NotApplicableEx,Exninfo.null) poss
- else tclONCE (aux (NotApplicableEx,Exninfo.null) poss)
+ if backtrack then aux (NoApplicableEx,Exninfo.null) poss
+ else tclONCE (aux (NoApplicableEx,Exninfo.null) poss)
let hints_tac hints info kont : unit Proofview.tactic =
Proofview.Goal.enter
@@ -1303,7 +1319,7 @@ module Search = struct
match e with
| ReachedLimitEx ->
Tacticals.New.tclFAIL 0 (str"Proof search reached its limit")
- | NotApplicableEx ->
+ | NoApplicableEx ->
Tacticals.New.tclFAIL 0 (str"Proof search failed" ++
(if Option.is_empty depth then mt()
else str" without reaching its limit"))
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index bcd31cb7e7..507ff10eea 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -632,7 +632,7 @@ let fix_r2l_forward_rew_scheme (c, ctx') =
(EConstr.of_constr (applist (c,
Context.Rel.to_extended_list mkRel 3 indargs @ [mkRel 1;mkRel 3;mkRel 2]))))))))
in c', ctx'
- | _ -> anomaly (Pp.str "Ill-formed non-dependent left-to-right rewriting scheme")
+ | _ -> anomaly (Pp.str "Ill-formed non-dependent left-to-right rewriting scheme.")
(**********************************************************************)
(* Build the right-to-left rewriting lemma for conclusion associated *)
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 268daf6b62..d64cc38eff 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1211,7 +1211,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
else
let (a,p_i_minus_1) = match whd_beta_stack !evdref p_i with
| (_sigS,[a;p]) -> (a, p)
- | _ -> anomaly ~label:"sig_clausal_form" (Pp.str "should be a sigma type") in
+ | _ -> anomaly ~label:"sig_clausal_form" (Pp.str "should be a sigma type.") in
let ev = Evarutil.e_new_evar env evdref a in
let rty = beta_applist sigma (p_i_minus_1,[ev]) in
let tuple_tail = sigrec_clausal_form (siglen-1) rty in
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 48a7b3f75c..70e62eabac 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -912,7 +912,7 @@ let make_resolve_hyp env sigma decl =
(c, NamedDecl.get_type decl, Univ.ContextSet.empty)]
with
| Failure _ -> []
- | e when Logic.catchable_exception e -> anomaly (Pp.str "make_resolve_hyp")
+ | e when Logic.catchable_exception e -> anomaly (Pp.str "make_resolve_hyp.")
(* REM : in most cases hintname = id *)
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 2ba18ceb42..4db744224a 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -260,7 +260,7 @@ let mkGProd id c1 c2 = CAst.make @@
let mkGArrow c1 c2 = CAst.make @@
GProd (Anonymous, Explicit, c1, c2)
let mkGVar id = CAst.make @@ GVar (Id.of_string id)
-let mkGPatVar id = CAst.make @@ GPatVar((false, Id.of_string id))
+let mkGPatVar id = CAst.make @@ GPatVar(Evar_kinds.FirstOrderPatVar (Id.of_string id))
let mkGRef r = CAst.make @@ GRef (Lazy.force r, None)
let mkGAppRef r args = mkGApp (mkGRef r) args
@@ -340,7 +340,7 @@ let match_arrow_pattern sigma t =
match Id.Map.bindings result with
| [(m1,arg);(m2,mind)] ->
assert (Id.equal m1 meta1 && Id.equal m2 meta2); (arg, mind)
- | _ -> anomaly (Pp.str "Incorrect pattern matching")
+ | _ -> anomaly (Pp.str "Incorrect pattern matching.")
let match_with_imp_term sigma c =
match EConstr.kind sigma c with
@@ -471,7 +471,7 @@ let match_eq_nf gls eqn (ref, hetero) =
| [(m1,t);(m2,x);(m3,y)] ->
assert (Id.equal m1 meta1 && Id.equal m2 meta2 && Id.equal m3 meta3);
(t,pf_whd_all gls x,pf_whd_all gls y)
- | _ -> anomaly ~label:"match_eq" (Pp.str "an eq pattern should match 3 terms")
+ | _ -> anomaly ~label:"match_eq" (Pp.str "an eq pattern should match 3 terms.")
let dest_nf_eq gls eqn =
try
@@ -499,7 +499,7 @@ let coq_sig_pattern =
let match_sigma sigma t =
match Id.Map.bindings (matches sigma (Lazy.force coq_sig_pattern) t) with
| [(_,a); (_,p)] -> (a,p)
- | _ -> anomaly (Pp.str "Unexpected pattern")
+ | _ -> anomaly (Pp.str "Unexpected pattern.")
let is_matching_sigma sigma t = is_matching sigma (Lazy.force coq_sig_pattern) t
@@ -545,7 +545,7 @@ let match_eqdec sigma t =
match Id.Map.bindings subst with
| [(_,typ);(_,c1);(_,c2)] ->
eqonleft, Lazy.force op, c1, c2, typ
- | _ -> anomaly (Pp.str "Unexpected pattern")
+ | _ -> anomaly (Pp.str "Unexpected pattern.")
(* Patterns "~ ?" and "? -> False" *)
let coq_not_pattern = lazy (mkPattern (mkGAppRef coq_not_ref [mkGHole]))
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index c495b5ece2..a7eadc3c3e 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -238,7 +238,7 @@ let compute_constructor_signatures isrec ((_,k as ity),u) =
end
| LetIn (_,_,_,c), rest -> false :: analrec c rest
| _, [] -> []
- | _ -> anomaly (Pp.str "compute_constructor_signatures")
+ | _ -> anomaly (Pp.str "compute_constructor_signatures.")
in
let (mib,mip) = Global.lookup_inductive ity in
let n = mib.mind_nparams in
@@ -613,7 +613,7 @@ module New = struct
let indmv =
match EConstr.kind elimclause.evd (last_arg elimclause.evd elimclause.templval.Evd.rebus) with
| Meta mv -> mv
- | _ -> anomaly (str"elimination")
+ | _ -> anomaly (str"elimination.")
in
let pmv =
let p, _ = decompose_app elimclause.evd elimclause.templtyp.Evd.rebus in
@@ -700,7 +700,7 @@ module New = struct
let make_elim_branch_assumptions ba hyps =
let assums =
try List.rev (List.firstn ba.nassums hyps)
- with Failure _ -> anomaly (Pp.str "make_elim_branch_assumptions") in
+ with Failure _ -> anomaly (Pp.str "make_elim_branch_assumptions.") in
{ ba = ba; assums = assums }
let elim_on_ba tac ba =
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 2a9928a3aa..a93a86d3a3 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1246,7 +1246,7 @@ let cut c =
let error_uninstantiated_metas t clenv =
let t = EConstr.Unsafe.to_constr t in
let na = meta_name clenv.evd (List.hd (Metaset.elements (metavars_of t))) in
- let id = match na with Name id -> id | _ -> anomaly (Pp.str "unnamed dependent meta")
+ let id = match na with Name id -> id | _ -> anomaly (Pp.str "unnamed dependent meta.")
in user_err (str "Cannot find an instance for " ++ pr_id id ++ str".")
let check_unresolved_evars_of_metas sigma clenv =
@@ -1305,13 +1305,13 @@ let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true)
let last_arg sigma c = match EConstr.kind sigma c with
| App (f,cl) ->
Array.last cl
- | _ -> anomaly (Pp.str "last_arg")
+ | _ -> anomaly (Pp.str "last_arg.")
let nth_arg sigma i c =
if Int.equal i (-1) then last_arg sigma c else
match EConstr.kind sigma c with
| App (f,cl) -> cl.(i)
- | _ -> anomaly (Pp.str "nth_arg")
+ | _ -> anomaly (Pp.str "nth_arg.")
let index_of_ind_arg sigma t =
let rec aux i j t = match EConstr.kind sigma t with
@@ -4705,7 +4705,7 @@ let elim_scheme_type elim t =
clenv_unify ~flags:(elim_flags ()) Reduction.CUMUL t
(clenv_meta_type clause mv) clause in
Clenvtac.res_pf clause' ~flags:(elim_flags ()) ~with_evars:false
- | _ -> anomaly (Pp.str "elim_scheme_type")
+ | _ -> anomaly (Pp.str "elim_scheme_type.")
end }
let elim_type t =
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 07:10:08 +0000