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.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp/implicit_quantifiers.mli')

diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index dc83e2135c..57eff0b863 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -42,7 +42,7 @@ val free_vars_of_rawconstr : ?bound:Idset.t -> rawconstr -> (Names.identifier *
 
 val make_fresh : Names.Idset.t -> Environ.env -> identifier -> identifier
 
-val implicits_of_rawterm : Rawterm.rawconstr -> (Topconstr.explicitation * (bool * bool)) list
+val implicits_of_rawterm : Rawterm.rawconstr -> (Topconstr.explicitation * (bool * bool * bool)) list
 
 val combine_params_freevar :
   Names.Idset.t -> (global_reference * bool) option * (Names.name * Term.constr option * Term.types) ->
-- 
cgit v1.2.3