aboutsummaryrefslogtreecommitdiff
path: root/API/API.mli
diff options
context:
space:
mode:
Diffstat (limited to 'API/API.mli')
-rw-r--r--API/API.mli4
1 files changed, 2 insertions, 2 deletions
diff --git a/API/API.mli b/API/API.mli
index 20a637c1fa..5a833d08ad 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -4100,7 +4100,7 @@ sig
module New :
sig
- val refine : ?unsafe:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.constr) -> unit Proofview.tactic
+ val refine : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.constr) -> unit Proofview.tactic
val reduce_after_refine : unit Proofview.tactic
end
module Simple :
@@ -4490,7 +4490,7 @@ end
module Refine :
sig
- val refine : ?unsafe:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.t) -> unit Proofview.tactic
+ val refine : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.t) -> unit Proofview.tactic
val solve_constraints : unit Proofview.tactic
end