From 0fad09306982a88ff8d633d36abdc440dd542ab3 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 13 Jun 2017 10:33:56 +0200 Subject: Dualize the unsafe flag of refine into typecheck and make it mandatory. --- plugins/cc/cctac.ml | 2 +- plugins/ltac/extratactics.ml4 | 2 +- plugins/ltac/rewrite.ml | 6 +++--- plugins/omega/coq_omega.ml | 4 ++-- plugins/ssr/ssripats.ml | 2 +- 5 files changed, 8 insertions(+), 8 deletions(-) (limited to 'plugins') diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 4f4e9a851..0f5b80664 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -255,7 +255,7 @@ let app_global_with_holes f args n = Tacticals.New.pf_constr_of_global (Lazy.force f) >>= fun fc -> let env = Proofview.Goal.env gl in let concl = Proofview.Goal.concl gl in - Refine.refine ~unsafe:true begin fun sigma -> + Refine.refine ~typecheck:false begin fun sigma -> let t = Tacmach.New.pf_get_type_of gl fc in let t = Termops.prod_applist sigma t (Array.to_list args) in let ans = mkApp (fc, args) in diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index 18d7b818c..7259faecd 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -365,7 +365,7 @@ let refine_tac ist simple with_classes c = let update = begin fun sigma -> c env sigma end in - let refine = Refine.refine ~unsafe:true update in + let refine = Refine.refine ~typecheck:false update in if simple then refine else refine <*> Tactics.New.reduce_after_refine <*> diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 3927ca7ce..fad181c89 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1539,7 +1539,7 @@ let assert_replacing id newt tac = | d :: rem -> insert_dependent env sigma (LocalAssum (NamedDecl.get_id d, newt)) [] after @ rem in let env' = Environ.reset_with_named_context (val_of_named_context nc) env in - Refine.refine ~unsafe:false begin fun sigma -> + Refine.refine ~typecheck:true begin fun sigma -> let (sigma, ev) = Evarutil.new_evar env' sigma concl in let (sigma, ev') = Evarutil.new_evar env sigma newt in let map d = @@ -1573,7 +1573,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = match clause, prf with | Some id, Some p -> let tac = tclTHENLIST [ - Refine.refine ~unsafe:false (fun h -> (h,p)); + Refine.refine ~typecheck:true (fun h -> (h,p)); Proofview.Unsafe.tclNEWGOALS gls; ] in Proofview.Unsafe.tclEVARS undef <*> @@ -1590,7 +1590,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = let (sigma, ev) = Evarutil.new_evar env sigma newt in (sigma, mkApp (p, [| ev |])) end in - Refine.refine ~unsafe:false make <*> Proofview.Unsafe.tclNEWGOALS gls + Refine.refine ~typecheck:true make <*> Proofview.Unsafe.tclNEWGOALS gls end | None, None -> Proofview.Unsafe.tclEVARS undef <*> diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index fb03948ba..440a10bfb 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -652,7 +652,7 @@ let clever_rewrite_base_poly typ p result theorem = let full = pf_concl gl in let env = pf_env gl in let (abstracted,occ) = abstract_path (project gl) typ (List.rev p) full in - Refine.refine ~unsafe:true begin fun sigma -> + Refine.refine ~typecheck:false begin fun sigma -> let t = applist (mkLambda @@ -688,7 +688,7 @@ let clever_rewrite_gen_nat p result (t,args) = (** Solve using the term the term [t _] *) let refine_app gl t = let open Tacmach.New in - Refine.refine ~unsafe:true begin fun sigma -> + Refine.refine ~typecheck:false begin fun sigma -> let env = pf_env gl in let ht = match EConstr.kind sigma (pf_get_type_of gl t) with | Prod (_, t, _) -> t diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml index 4a9dddd2b..7ae9e3824 100644 --- a/plugins/ssr/ssripats.ml +++ b/plugins/ssr/ssripats.ml @@ -95,7 +95,7 @@ let ssrmkabs id gl = end in Proofview.V82.of_tactic (Proofview.tclTHEN - (Tactics.New.refine step) + (Tactics.New.refine ~typecheck:false step) (Proofview.tclFOCUS 1 3 Proofview.shelve)) gl let ssrmkabstac ids = -- cgit v1.2.3