diff options
| author | Pierre-Marie Pédrot | 2014-09-04 10:37:01 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-09-04 15:43:33 +0200 |
| commit | 67b8fba4209c407c94ed8d54ec78352397d82f59 (patch) | |
| tree | 5c78c966e95f957002f55ebd2e09ea7bebab83d8 /tactics | |
| parent | 3806d567af6b1feee2c8f196199eee4208a8551d (diff) | |
Proofview refiner is now type-safe by default.
In order not to be too costly, there is an [unsafe] flag to be set if the
tactic does not have to check that the partial proof term is well-typed (to
be used with caution though).
This patch breaks one [fix]-based example in the refine test-suite, but a huge
development like CompCert still goes through.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tactics.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 77876e6262..932bfc5fe7 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -783,7 +783,7 @@ let cut c = let id = next_name_away_with_default "H" Anonymous (Tacmach.New.pf_ids_of_hyps gl) in (** Backward compat: normalize [c]. *) let c = local_strong whd_betaiota sigma c in - Proofview.Refine.refine begin fun h -> + Proofview.Refine.refine ~unsafe:true begin fun h -> let (h, f) = Proofview.Refine.new_evar h env (mkArrow c (Vars.lift 1 concl)) in let (h, x) = Proofview.Refine.new_evar h env c in let f = mkLambda (Name id, c, mkApp (Vars.lift 1 f, [|mkRel 1|])) in @@ -1404,7 +1404,7 @@ let cut_and_apply c = (* let refine_no_check = Profile.profile2 refine_no_checkkey refine_no_check *) let new_exact_no_check c = - Proofview.Refine.refine (fun h -> (h, c)) + Proofview.Refine.refine ~unsafe:true (fun h -> (h, c)) let exact_check c = Proofview.Goal.raw_enter begin fun gl -> @@ -1446,7 +1446,7 @@ let assumption = in if is_same_type then (Proofview.V82.tclEVARS sigma) <*> - Proofview.Refine.refine (fun h -> (h, mkVar id)) + Proofview.Refine.refine ~unsafe:true (fun h -> (h, mkVar id)) else arec gl only_eq rest in let assumption_tac gl = |