aboutsummaryrefslogtreecommitdiff
path: root/plugins/firstorder/sequent.mli
diff options
context:
space:
mode:
authorMaxime Dénès2020-05-14 16:33:15 +0200
committerMaxime Dénès2020-05-14 16:33:15 +0200
commit81fba800a97955368791df115e807cde66eff19c (patch)
treec0cb601061912a95a8b5ad031f0378a1e479320b /plugins/firstorder/sequent.mli
parent8dd5c47007817c104d57a449409a6b9c6f8ef12e (diff)
parent101d898869ffa07fc772b303e3dbb7ecd860386b (diff)
Merge PR #11922: No more local reduction functions in Reductionops.
Reviewed-by: Matafou Ack-by: SkySkimmer Reviewed-by: gares
Diffstat (limited to 'plugins/firstorder/sequent.mli')
-rw-r--r--plugins/firstorder/sequent.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli
index 3a5da6ad14..bba89c823c 100644
--- a/plugins/firstorder/sequent.mli
+++ b/plugins/firstorder/sequent.mli
@@ -39,7 +39,7 @@ val deepen: t -> t
val record: h_item -> t -> t
-val lookup: Evd.evar_map -> h_item -> t -> bool
+val lookup: Environ.env -> Evd.evar_map -> h_item -> t -> bool
val add_formula : Environ.env -> Evd.evar_map -> side -> GlobRef.t -> constr -> t -> t