From ea9a239eefacf85338c1f0ca0d3dc144c7e7f20e Mon Sep 17 00:00:00 2001
From: jforest
Date: Wed, 16 Dec 2009 16:03:38 +0000
Subject: adding an option functional_induction_rewrite_dependent to make
 functional induction using not v8.2 version of subst. By default functional
 induction uses new version of subst

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12592 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/equality.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/equality.mli b/tactics/equality.mli
index bbe8f1e481..b88f376ee2 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -120,7 +120,7 @@ type subst_tactic_flags = {
   only_leibniz : bool;
   rewrite_dependent_proof : bool
 }
-
+val subst_gen : bool -> identifier list -> tactic
 val subst : identifier list -> tactic
 val subst_all : ?flags:subst_tactic_flags -> tactic
 
-- 
cgit v1.2.3