diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tacticals.ml | 9 | ||||
| -rw-r--r-- | tactics/tactics.ml | 14 |
2 files changed, 15 insertions, 8 deletions
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index fc099f643d..c0fad0026f 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -695,6 +695,8 @@ module New = struct (* Check that holes in arguments have been resolved *) let check_evars env sigma extsigma origsigma = + let reachable = lazy (Evarutil.reachable_from_evars sigma + (Evar.Map.domain (Evd.undefined_map origsigma))) in let rec is_undefined_up_to_restriction sigma evk = if Evd.mem origsigma evk then None else let evi = Evd.find sigma evk in @@ -710,7 +712,12 @@ module New = struct let rest = Evd.fold_undefined (fun evk evi acc -> match is_undefined_up_to_restriction sigma evk with - | Some (evk',evi) -> (evk',evi)::acc + | Some (evk',evi) -> + (* If [evk'] descends from [evk] which descends itself from + an originally undefined evar in [origsigma], it is a not + a fresh undefined hole from [sigma]. *) + if Evar.Set.mem evk (Lazy.force reachable) then acc + else (evk',evi)::acc | _ -> acc) extsigma [] in diff --git a/tactics/tactics.ml b/tactics/tactics.ml index d33f3a5062..686779b1d2 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -5181,14 +5181,14 @@ end (** Tacticals defined directly in term of Proofview *) module New = struct - open Genredexpr - open Locus - let reduce_after_refine = - reduce - (Lazy {rBeta=true;rMatch=true;rFix=true;rCofix=true; - rZeta=false;rDelta=false;rConst=[]}) - {onhyps = Some []; concl_occs = AllOccurrences } + (* For backward compatibility reasons, we do not contract let-ins, but we unfold them. *) + let redfun env t = + let open CClosure in + let flags = RedFlags.red_add_transparent allnolet TransparentState.empty in + clos_norm_flags flags env t + in + reduct_in_concl ~check:false (redfun,DEFAULTcast) let refine ~typecheck c = Refine.refine ~typecheck c <*> |