diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/goal.ml | 5 | ||||
| -rw-r--r-- | proofs/refine.ml | 11 | ||||
| -rw-r--r-- | proofs/refine.mli | 8 |
3 files changed, 12 insertions, 12 deletions
diff --git a/proofs/goal.ml b/proofs/goal.ml index 4c598ca29e..7499bc251b 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -86,12 +86,11 @@ module V82 = struct (* Instantiates a goal with an open term *) let partial_solution sigma evk c = (* Check that the goal itself does not appear in the refined term *) - let c = EConstr.Unsafe.to_constr c in let _ = if not (Evarutil.occur_evar_upto sigma evk c) then () - else Pretype_errors.error_occur_check Environ.empty_env sigma evk (EConstr.of_constr c) + else Pretype_errors.error_occur_check Environ.empty_env sigma evk c in - Evd.define evk c sigma + Evd.define evk (EConstr.Unsafe.to_constr c) sigma (* Instantiates a goal with an open term, using name of goal for evk' *) let partial_solution_to sigma evk evk' c = diff --git a/proofs/refine.ml b/proofs/refine.ml index 067764c000..11eabe0a90 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -47,7 +47,7 @@ let typecheck_evar ev env sigma = let typecheck_proof c concl env sigma = let evdref = ref sigma in - let () = Typing.e_check env evdref (EConstr.of_constr c) (EConstr.of_constr concl) in + let () = Typing.e_check env evdref c concl in !evdref let (pr_constrv,pr_constr) = @@ -77,6 +77,7 @@ let make_refine_enter ?(unsafe = true) f = let sigma = Sigma.to_evar_map sigma in let env = Proofview.Goal.env gl in let concl = Proofview.Goal.concl gl in + let concl = EConstr.of_constr concl in (** Save the [future_goals] state to restore them after the refinement. *) let prev_future_goals = Evd.future_goals sigma in @@ -98,9 +99,10 @@ let make_refine_enter ?(unsafe = true) f = let self = Proofview.Goal.goal gl in let _ = if not (Evarutil.occur_evar_upto sigma self c) then () - else Pretype_errors.error_occur_check env sigma self (EConstr.of_constr c) + else Pretype_errors.error_occur_check env sigma self c in (** Proceed to the refinement *) + let c = EConstr.Unsafe.to_constr c in let sigma = match evkmain with | None -> Evd.define self c sigma | Some evk -> @@ -133,23 +135,22 @@ let refine ?(unsafe = true) f = (** Useful definitions *) let with_type env evd c t = - let c = EConstr.of_constr c in let my_type = Retyping.get_type_of env evd c in let my_type = EConstr.of_constr my_type in let j = Environ.make_judge c my_type in let (evd,j') = - Coercion.inh_conv_coerce_to true (Loc.ghost) env evd j (EConstr.of_constr t) + Coercion.inh_conv_coerce_to true (Loc.ghost) env evd j t in evd , j'.Environ.uj_val let refine_casted ?unsafe f = Proofview.Goal.enter { enter = begin fun gl -> let gl = Proofview.Goal.assume gl in let concl = Proofview.Goal.concl gl in + let concl = EConstr.of_constr concl in let env = Proofview.Goal.env gl in let f = { run = fun h -> let Sigma (c, h, p) = f.run h in let sigma, c = with_type env (Sigma.to_evar_map h) c concl in - let c = EConstr.Unsafe.to_constr c in Sigma (c, Sigma.Unsafe.of_evar_map sigma, p) } in refine ?unsafe f diff --git a/proofs/refine.mli b/proofs/refine.mli index 4158e446cc..205b979747 100644 --- a/proofs/refine.mli +++ b/proofs/refine.mli @@ -21,7 +21,7 @@ val pr_constr : (** {7 Refinement primitives} *) -val refine : ?unsafe:bool -> Constr.t Sigma.run -> unit tactic +val refine : ?unsafe:bool -> EConstr.t Sigma.run -> unit tactic (** In [refine ?unsafe 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 @@ -30,16 +30,16 @@ val refine : ?unsafe:bool -> Constr.t Sigma.run -> unit tactic tactic failures. If [unsafe] is [false] (default is [true]) [t] is type-checked beforehand. *) -val refine_one : ?unsafe:bool -> ('a * Constr.t) Sigma.run -> 'a tactic +val refine_one : ?unsafe:bool -> ('a * EConstr.t) Sigma.run -> 'a tactic (** A generalization of [refine] which assumes exactly one goal under focus *) (** {7 Helper functions} *) val with_type : Environ.env -> Evd.evar_map -> - Term.constr -> Term.types -> Evd.evar_map * EConstr.constr + EConstr.constr -> EConstr.types -> Evd.evar_map * EConstr.constr (** [with_type env sigma c t] ensures that [c] is of type [t] inserting a coercion if needed. *) -val refine_casted : ?unsafe:bool -> Constr.t Sigma.run -> unit tactic +val refine_casted : ?unsafe:bool -> EConstr.t Sigma.run -> unit tactic (** Like {!refine} except the refined term is coerced to the conclusion of the current goal. *) |