aboutsummaryrefslogtreecommitdiffhomepage
path: root/API
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-08-29 14:35:12 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-08-29 14:35:12 +0200
commit8aa7de4ea2660fe370cedab07c1c5dcc19226c8c (patch)
tree0eb6a177c3a14d50173183b0188b5f15b6c425c5 /API
parent75d70664156bf1715b4eb9933a684a344f43467d (diff)
parent7ba6bc4554a642f78f59b996f99d9d6ca2cc2678 (diff)
Merge PR #805: Functional tactics
Diffstat (limited to 'API')
-rw-r--r--API/API.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/API/API.mli b/API/API.mli
index 5804a82f6..1262899c5 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -5241,7 +5241,7 @@ sig
val build_selector :
Environ.env -> Evd.evar_map -> int -> EConstr.constr -> EConstr.types ->
- EConstr.constr -> EConstr.constr -> Evd.evar_map * EConstr.constr
+ EConstr.constr -> EConstr.constr -> EConstr.constr
val replace : EConstr.constr -> EConstr.constr -> unit Proofview.tactic
val general_rewrite :
orientation -> Locus.occurrences -> freeze_evars_flag -> dep_proof_flag ->