summaryrefslogtreecommitdiff
path: root/contrib/funind/functional_principles_proofs.mli
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/funind/functional_principles_proofs.mli')
-rw-r--r--contrib/funind/functional_principles_proofs.mli3
1 files changed, 1 insertions, 2 deletions
diff --git a/contrib/funind/functional_principles_proofs.mli b/contrib/funind/functional_principles_proofs.mli
index 35da5d50..62eb528e 100644
--- a/contrib/funind/functional_principles_proofs.mli
+++ b/contrib/funind/functional_principles_proofs.mli
@@ -16,5 +16,4 @@ val prove_principle_for_gen :
Tacmach.tactic
-val is_pte : rel_declaration -> bool
-val do_observe : unit -> bool
+(* val is_pte : rel_declaration -> bool *)