From 8cadbeff68559ee4a621f9ac3ed44c5e5da7a8ba Mon Sep 17 00:00:00 2001
From: msozeau
Date: Sat, 28 Mar 2009 21:31:54 +0000
Subject: Rewrite of Program Fixpoint to overcome the previous limitations: -
 The measure can now refer to all the formal arguments - The recursive calls
 can make all the arguments vary as well - Generalized to any relation and
 measure (new syntax {measure m on R}) This relies on an automatic
 curryfication transformation, the real fixpoint combinator is working on a
 sigma type of the arguments. Reduces to the previous impl in case only one
 argument is involved. The patch also introduces a new flag on implicit
 arguments that says if the argument has to be infered (default) or can be
 turned into a subgoal/obligation. Comes with a test-suite file.

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

(limited to 'interp/implicit_quantifiers.ml')

diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index a9d3704471..4495c22c67 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -254,7 +254,7 @@ let implicits_of_rawterm l =
 		    Name id -> Some id
 		  | Anonymous -> None
 	      in
-		(ExplByPos (i, name), (true, true)) :: rest
+		(ExplByPos (i, name), (true, true, true)) :: rest
 	    else rest
       | RLetIn (loc, na, t, b) -> aux i b
       | _ -> []
-- 
cgit v1.2.3