From 3afaf3dde673d77cacaabc354f008dfbe49a7cee Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 24 Jul 2000 13:39:23 +0000
Subject: Passage à des contextes de vars et de rels pouvant contenir des
 déclarations

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@568 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/refiner.mli | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

(limited to 'proofs/refiner.mli')

diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 5c2b24d7fc..8546b0c73c 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -39,10 +39,6 @@ val frontier : transformation_tactic
 val list_pf : proof_tree -> goal list
 val unTAC : tactic -> goal sigma -> proof_tree sigma
 
-val extract_open_proof : 
-  typed_type signature -> proof_tree -> constr * (int * constr) list
-
-
 (*s Tacticals. *)
 
 (* [tclIDTAC] is the identity tactic *)
@@ -114,7 +110,7 @@ type pftreestate
 val proof_of_pftreestate : pftreestate -> proof_tree
 val cursor_of_pftreestate : pftreestate -> int list
 val is_top_pftreestate : pftreestate -> bool
-val evc_of_pftreestate : pftreestate -> global_constraints
+val evc_of_pftreestate : pftreestate -> evar_declarations
 val top_goal_of_pftreestate : pftreestate -> goal sigma
 val nth_goal_of_pftreestate : int -> pftreestate -> goal sigma
 
@@ -127,6 +123,7 @@ val solve_pftreestate : tactic -> pftreestate -> pftreestate
 val weak_undo_pftreestate : pftreestate -> pftreestate
 
 val mk_pftreestate : goal -> pftreestate
+val extract_open_pftreestate : pftreestate -> constr * (int * typed_type) list
 val extract_pftreestate : pftreestate -> constr
 val first_unproven : pftreestate -> pftreestate
 val last_unproven : pftreestate -> pftreestate
-- 
cgit v1.2.3