From 68191dcce820a8135a84e716bddb7cf78476c360 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Mon, 31 Mar 2014 19:26:40 +0200
Subject: Removing the Change_evar refiner rule.

---
 proofs/refiner.mli | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'proofs/refiner.mli')

diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index db2c081d1..012209410 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -27,9 +27,6 @@ val refiner : rule -> tactic
 
 (** {6 Tacticals. } *)
 
-(** [tclNORMEVAR] forces propagation of evar constraints *)
-val tclNORMEVAR       : tactic
-
 (** [tclIDTAC] is the identity tactic without message printing*)
 val tclIDTAC          : tactic
 val tclIDTAC_MESSAGE  : Pp.std_ppcmds -> tactic
-- 
cgit v1.2.3