From ac776b4660e95577eb6742200d882b8cf683cc10 Mon Sep 17 00:00:00 2001 From: aspiwack Date: Thu, 10 Feb 2011 10:10:58 +0000 Subject: Started to fix the declarative proof mode (C-zar). Everything seems to work fine in CoqIDE (except escape/return and the daimon which are not entirely ported). However, there is some problem causing proof general to fail when using goto or evaluate buffer (evaluate next phrase works fine though), as well as coqc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13817 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 0a2ab571f..b27939b3c 100644 --- a/plugins/decl_mode/decl_proof_instr.mli +++ b/plugins/decl_mode/decl_proof_instr.mli @@ -109,5 +109,3 @@ val init_tree: (int option * Declarations.recarg Rtree.t) array -> (Names.Idset.t * Decl_mode.split_tree) option) -> Decl_mode.split_tree - -val set_refine : (Evd.open_constr -> Proof_type.tactic) -> unit -- cgit v1.2.3