From cf35c36c341d7f1f615b3e11e6aab64a7fa6a5bf Mon Sep 17 00:00:00 2001
From: aspiwack
Date: Tue, 19 Apr 2011 17:11:35 +0000
Subject: Declarative mode: fix escape and return.

The declarative mode should now work almost like in v8.3

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14029 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/decl_mode/decl_proof_instr.mli | 2 --
 1 file changed, 2 deletions(-)

(limited to 'plugins/decl_mode/decl_proof_instr.mli')

diff --git a/plugins/decl_mode/decl_proof_instr.mli b/plugins/decl_mode/decl_proof_instr.mli
index b27939b3ca..1205060aea 100644
--- a/plugins/decl_mode/decl_proof_instr.mli
+++ b/plugins/decl_mode/decl_proof_instr.mli
@@ -19,8 +19,6 @@ val register_automation_tac: tactic -> unit
 
 val automation_tac : tactic
 
-val daimon_subtree: Proof.proof -> Proof.proof
-
 val concl_refiner:
   Termops.meta_type_map -> constr -> Proof_type.goal sigma -> constr
 
-- 
cgit v1.2.3