From 22ca6b0d70bb8b49aaa420f844c75592e5781c21 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 9 May 2017 10:03:37 +0200 Subject: Turn the default behaviour of the refine primitive into the safe one. --- proofs/refine.ml | 6 +++--- proofs/refine.mli | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) (limited to 'proofs') diff --git a/proofs/refine.ml b/proofs/refine.ml index caa6b9fb30..eab053f3a3 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -69,7 +69,7 @@ let add_side_effect env = function let add_side_effects env effects = List.fold_left (fun env eff -> add_side_effect env eff) env effects -let generic_refine ?(unsafe = true) f gl = +let generic_refine ?(unsafe = false) f gl = let gl = Proofview.Goal.assume gl in let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in @@ -134,10 +134,10 @@ let lift c = let make_refine_enter ?unsafe f gl = generic_refine ?unsafe (lift f) gl -let refine_one ?(unsafe = true) f = +let refine_one ?(unsafe = false) f = Proofview.Goal.enter_one (make_refine_enter ~unsafe f) -let refine ?(unsafe = true) f = +let refine ?(unsafe = false) f = let f evd = let (evd,c) = f evd in (evd,((), c)) in diff --git a/proofs/refine.mli b/proofs/refine.mli index f1439f9a13..cede9d4581 100644 --- a/proofs/refine.mli +++ b/proofs/refine.mli @@ -27,7 +27,7 @@ val refine : ?unsafe:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.t) -> unit for the current goal (refine is a goal-dependent tactic), the new holes created by [t] become the new subgoals. Exceptions raised during the interpretation of [t] are caught and result in - tactic failures. If [unsafe] is [false] (default is [true]) [t] is + tactic failures. If [unsafe] is [false] (which is the default) [t] is type-checked beforehand. *) val refine_one : ?unsafe:bool -> (Evd.evar_map -> Evd.evar_map * ('a * EConstr.t)) -> 'a tactic -- cgit v1.2.3 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. --- proofs/refine.ml | 20 ++++++++++---------- proofs/refine.mli | 13 ++++++------- 2 files changed, 16 insertions(+), 17 deletions(-) (limited to 'proofs') diff --git a/proofs/refine.ml b/proofs/refine.ml index eab053f3a3..796b4b8377 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -69,7 +69,7 @@ let add_side_effect env = function let add_side_effects env effects = List.fold_left (fun env eff -> add_side_effect env eff) env effects -let generic_refine ?(unsafe = false) f gl = +let generic_refine ~typecheck f gl = let gl = Proofview.Goal.assume gl in let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in @@ -91,9 +91,9 @@ let generic_refine ?(unsafe = false) f gl = let env = add_side_effects env sideff in (** Check that the introduced evars are well-typed *) let fold accu ev = typecheck_evar ev env accu in - let sigma = if unsafe then sigma else CList.fold_left fold sigma evs in + let sigma = if typecheck then CList.fold_left fold sigma evs else sigma in (** Check that the refined term is typesafe *) - let sigma = if unsafe then sigma else typecheck_proof c concl env sigma in + let sigma = if typecheck then typecheck_proof c concl env sigma else sigma in (** Check that the goal itself does not appear in the refined term *) let self = Proofview.Goal.goal gl in let _ = @@ -132,16 +132,16 @@ let lift c = Proofview.tclUNIT c end -let make_refine_enter ?unsafe f gl = generic_refine ?unsafe (lift f) gl +let make_refine_enter ~typecheck f gl = generic_refine ~typecheck (lift f) gl -let refine_one ?(unsafe = false) f = - Proofview.Goal.enter_one (make_refine_enter ~unsafe f) +let refine_one ~typecheck f = + Proofview.Goal.enter_one (make_refine_enter ~typecheck f) -let refine ?(unsafe = false) f = +let refine ~typecheck f = let f evd = let (evd,c) = f evd in (evd,((), c)) in - Proofview.Goal.enter (make_refine_enter ~unsafe f) + Proofview.Goal.enter (make_refine_enter ~typecheck f) (** Useful definitions *) @@ -153,7 +153,7 @@ let with_type env evd c t = in evd , j'.Environ.uj_val -let refine_casted ?unsafe f = Proofview.Goal.enter begin fun gl -> +let refine_casted ~typecheck f = Proofview.Goal.enter begin fun gl -> let gl = Proofview.Goal.assume gl in let concl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in @@ -161,7 +161,7 @@ let refine_casted ?unsafe f = Proofview.Goal.enter begin fun gl -> let (h, c) = f h in with_type env h c concl in - refine ?unsafe f + refine ~typecheck f end (** {7 solve_constraints} diff --git a/proofs/refine.mli b/proofs/refine.mli index cede9d4581..c1c57ecb8e 100644 --- a/proofs/refine.mli +++ b/proofs/refine.mli @@ -21,19 +21,18 @@ val pr_constr : (** {7 Refinement primitives} *) -val refine : ?unsafe:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.t) -> unit tactic -(** In [refine ?unsafe t], [t] is a term with holes under some +val refine : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.t) -> unit tactic +(** In [refine ~typecheck t], [t] is a term with holes under some [evar_map] context. The term [t] is used as a partial solution for the current goal (refine is a goal-dependent tactic), the new holes created by [t] become the new subgoals. Exceptions raised during the interpretation of [t] are caught and result in - tactic failures. If [unsafe] is [false] (which is the default) [t] is - type-checked beforehand. *) + tactic failures. If [typecheck] is [true] [t] is type-checked beforehand. *) -val refine_one : ?unsafe:bool -> (Evd.evar_map -> Evd.evar_map * ('a * EConstr.t)) -> 'a tactic +val refine_one : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * ('a * EConstr.t)) -> 'a tactic (** A variant of [refine] which assumes exactly one goal under focus *) -val generic_refine : ?unsafe:bool -> ('a * EConstr.t) tactic -> +val generic_refine : typecheck:bool -> ('a * EConstr.t) tactic -> [ `NF ] Proofview.Goal.t -> 'a tactic (** The general version of refine. *) @@ -44,7 +43,7 @@ val with_type : Environ.env -> Evd.evar_map -> (** [with_type env sigma c t] ensures that [c] is of type [t] inserting a coercion if needed. *) -val refine_casted : ?unsafe:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.t) -> unit tactic +val refine_casted : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.t) -> unit tactic (** Like {!refine} except the refined term is coerced to the conclusion of the current goal. *) -- cgit v1.2.3