diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/class_tactics.ml4 | 1 | ||||
| -rw-r--r-- | tactics/refine.ml | 2 | ||||
| -rw-r--r-- | tactics/rewrite.ml4 | 5 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 2 | ||||
| -rw-r--r-- | tactics/tacticals.ml | 1 | ||||
| -rw-r--r-- | tactics/tacticals.mli | 1 |
6 files changed, 7 insertions, 5 deletions
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index 8f548210b..9146d02c5 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -452,7 +452,6 @@ let resolve_all_evars debug m env p oevd do_split fail = if fail then (* Unable to satisfy the constraints. *) let evm = if do_split then select_evars comp evd else evd in - let evm = Evarutil.nf_evars evm in let _, ev = Evd.fold (fun ev evi (b,acc) -> (* focus on one instance if only one was searched for *) diff --git a/tactics/refine.ml b/tactics/refine.ml index f1ecc4da9..ff644c143 100644 --- a/tactics/refine.ml +++ b/tactics/refine.ml @@ -372,7 +372,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 (pf_env gl) evd in + let evd = Typeclasses.resolve_typeclasses ~onlyargs:true (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/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index 213dcc8d2..7260f1fd7 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -834,8 +834,9 @@ let cl_rewrite_clause_aux ?(abs=None) strat goal_meta clause gl = with | Stdpp.Exc_located (_, TypeClassError (env, (UnsatisfiableConstraints _ as e))) | TypeClassError (env, (UnsatisfiableConstraints _ as e)) -> - tclFAIL 0 (str"setoid rewrite failed: unable to satisfy the rewriting constraints." - ++ fnl () ++ Himsg.explain_typeclass_error env e) gl) + Refiner.tclFAIL_lazy 0 + (lazy (str"setoid rewrite failed: unable to satisfy the rewriting constraints." + ++ fnl () ++ Himsg.explain_typeclass_error env e)) gl) | Some None -> tclFAIL 0 (str"setoid rewrite failed: no progress made") gl | None -> raise Not_found diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index c21a4c080..0942fde83 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1918,7 +1918,7 @@ and eval_with_fail ist is_lazy goal tac = with | FailError (0,s) | Stdpp.Exc_located(_, FailError (0,s)) | Stdpp.Exc_located(_,LtacLocated (_,FailError (0,s))) -> - raise (Eval_fail s) + raise (Eval_fail (Lazy.force s)) | FailError (lvl,s) -> raise (FailError (lvl - 1, s)) | Stdpp.Exc_located(s,FailError (lvl,s')) -> raise (Stdpp.Exc_located(s,FailError (lvl - 1, s'))) diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index ab7120b8b..2b69d7233 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -59,6 +59,7 @@ let tclINFO = Refiner.tclINFO let tclCOMPLETE = Refiner.tclCOMPLETE let tclAT_LEAST_ONCE = Refiner.tclAT_LEAST_ONCE let tclFAIL = Refiner.tclFAIL +let tclFAIL_lazy = Refiner.tclFAIL_lazy let tclDO = Refiner.tclDO let tclPROGRESS = Refiner.tclPROGRESS let tclWEAK_PROGRESS = Refiner.tclWEAK_PROGRESS diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index fe6dd2d64..762c7dc76 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -53,6 +53,7 @@ val tclINFO : tactic -> tactic val tclCOMPLETE : tactic -> tactic val tclAT_LEAST_ONCE : tactic -> tactic val tclFAIL : int -> std_ppcmds -> tactic +val tclFAIL_lazy : int -> std_ppcmds Lazy.t -> tactic val tclDO : int -> tactic -> tactic val tclPROGRESS : tactic -> tactic val tclWEAK_PROGRESS : tactic -> tactic |