From 33a25f335839886cc205946bdc198ebab3b386de Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Mon, 9 Dec 2002 08:51:59 +0000
Subject: Option pour rendre les vérifications du refiner optionnelle
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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

(limited to 'proofs/evar_refiner.mli')

diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index b0dd5e4f4..55c7282c2 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -30,8 +30,6 @@ val rc_of_glsigma : goal sigma -> wc
    dependent goal *)
 type w_tactic = wc -> wc
 
-val local_Constraints : tactic
-
 val startWalk : goal sigma -> wc * (wc -> tactic)
 
 val extract_decl : evar -> w_tactic
-- 
cgit v1.2.3