From 838326c399c48cd55f15b195340fa92df59817fb Mon Sep 17 00:00:00 2001
From: barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Wed, 8 Sep 2004 18:42:11 +0000
Subject: unification encore...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6085 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/evar_refiner.mli | 4 ----
 1 file changed, 4 deletions(-)

(limited to 'proofs/evar_refiner.mli')

diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index 54646caf8..4766d94cb 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -22,15 +22,11 @@ type wc = named_context sigma (* for a better reading of the following *)
 
 (* Refinement of existential variables. *)
 
-val rc_of_glsigma : goal sigma -> wc
-
 (* A [w_tactic] is a tactic which modifies the a set of evars of which
    a goal depend, either by instantiating one, or by declaring a new
    dependent goal *)
 type w_tactic = wc -> wc
 
-val w_Declare    : evar -> types -> w_tactic
-
 val w_refine :  evar -> Rawterm.rawconstr  -> w_tactic
 
 val instantiate_pf_com :
-- 
cgit v1.2.3