From 8d8abed37c87368c2bdb8adde09bc8b69a408787 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Fri, 12 Sep 2008 23:14:34 +0000
Subject: Add a type argument to letin_tac instead of using casts and
 recomputing when one wants a particular type. Rewrite of the unification
 behind [Equations], much more robust but still buggy w.r.t. inaccessible
 patterns.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11399 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/funind/g_indfun.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'contrib/funind')

diff --git a/contrib/funind/g_indfun.ml4 b/contrib/funind/g_indfun.ml4
index d435f51351..020d67f0c5 100644
--- a/contrib/funind/g_indfun.ml4
+++ b/contrib/funind/g_indfun.ml4
@@ -307,7 +307,7 @@ let mkEq typ c1 c2 =
 let poseq_unsafe idunsafe cstr gl =
   let typ = Tacmach.pf_type_of gl cstr in
   tclTHEN
-    (Tactics.letin_tac None (Name idunsafe) cstr allClauses)
+    (Tactics.letin_tac None (Name idunsafe) cstr None allClauses)
     (tclTHENFIRST 
       (Tactics.assert_as true (Util.dummy_loc,IntroAnonymous) (mkEq typ (mkVar idunsafe) cstr)) 
       Tactics.reflexivity)
-- 
cgit v1.2.3