aboutsummaryrefslogtreecommitdiff
path: root/API
diff options
context:
space:
mode:
authorMaxime Dénès2017-10-13 11:17:47 +0200
committerMaxime Dénès2017-10-13 11:17:47 +0200
commitf8975f9fce08c7d43e6e57be980cfa36635969a9 (patch)
tree6f5ea799e9ccc9e70354125a0bcd5977c1a10997 /API
parent57bca928a3c0f7dc2582a4ffb8855ed668afdea2 (diff)
parent4e016b91f59d3bb13681a53c35fbf4a979140b83 (diff)
Merge PR #1103: Take Suggest Proof Using outside the kernel.
Diffstat (limited to 'API')
-rw-r--r--API/API.mli1
1 files changed, 0 insertions, 1 deletions
diff --git a/API/API.mli b/API/API.mli
index 04c69b025f..879323a37d 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -4914,7 +4914,6 @@ module G_proofs :
sig
val hint : Vernacexpr.hints_expr Pcoq.Gram.entry
- val hint_proof_using : 'a Pcoq.Gram.entry -> 'a option -> 'a option
end