diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/class_tactics.ml | 8 | ||||
| -rw-r--r-- | tactics/tactics.ml | 9 |
2 files changed, 11 insertions, 6 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 1672b7bd13..f9f8e8715e 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -1500,9 +1500,11 @@ let head_of_constr h c = let c = head_of_constr c in letin_tac None (Name h) c None Locusops.allHyps -let not_evar c = match kind_of_term c with -| Evar _ -> Tacticals.New.tclFAIL 0 (str"Evar") -| _ -> Proofview.tclUNIT () +let not_evar c = + Proofview.tclEVARMAP >>= fun sigma -> + match Evarutil.kind_of_term_upto sigma c with + | Evar _ -> Tacticals.New.tclFAIL 0 (str"Evar") + | _ -> Proofview.tclUNIT () let is_ground c gl = if Evarutil.is_ground_term (project gl) c then tclIDTAC gl diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 7519339cab..b54624f897 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -871,14 +871,17 @@ let reduction_clause redexp cl = (None, bind_red_expr_occurrences occs nbcl redexp)) cl let reduce redexp cl = + let trace () = Pp.(hov 2 (Pptactic.pr_atomic_tactic (Global.env()) (TacReduce (redexp,cl)))) in + Proofview.Trace.name_tactic trace begin Proofview.Goal.enter { enter = begin fun gl -> - let cl = concrete_clause_of (fun () -> Tacmach.New.pf_ids_of_hyps gl) cl in - let redexps = reduction_clause redexp cl in + let cl' = concrete_clause_of (fun () -> Tacmach.New.pf_ids_of_hyps gl) cl in + let redexps = reduction_clause redexp cl' in let check = match redexp with Fold _ | Pattern _ -> true | _ -> false in Tacticals.New.tclMAP (fun (where,redexp) -> e_reduct_option ~check (Redexpr.reduction_of_red_expr (Tacmach.New.pf_env gl) redexp) where) redexps end } + end (* Unfolding occurrences of a constant *) @@ -4945,7 +4948,7 @@ module New = struct let reduce_after_refine = reduce (Lazy {rBeta=true;rMatch=true;rFix=true;rCofix=true;rZeta=false;rDelta=false;rConst=[]}) - {onhyps=None; concl_occs=AllOccurrences } + {onhyps=Some []; concl_occs=AllOccurrences } let refine ?unsafe c = Refine.refine ?unsafe c <*> |