From a0cfa4f118023d35b767a999d5a2ac4b082857b4 Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Fri, 25 Jul 2008 15:12:53 +0200
Subject: Imported Upstream version 8.2~beta3+dfsg

---
 pretyping/pretyping.mli | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

(limited to 'pretyping/pretyping.mli')

diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index b1ed20c2..4f116053 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: pretyping.mli 9141 2006-09-15 10:07:01Z herbelin $ i*)
+(*i $Id: pretyping.mli 11047 2008-06-03 23:08:00Z msozeau $ i*)
 
 (*i*)
 open Names
@@ -18,6 +18,11 @@ open Rawterm
 open Evarutil
 (*i*)
 
+(* An auxiliary function for searching for fixpoint guard indexes *)
+
+val search_guard : 
+    Util.loc -> env -> int list list -> rec_declaration -> int array
+
 type typing_constraint = OfType of types option | IsType
 
 type var_map = (identifier * unsafe_judgment) list
@@ -35,7 +40,7 @@ sig
      unresolved holes as evars and returning the typing contexts of
      these evars. Work as [understand_gen] for the rest. *)
   
-  val understand_tcc :
+  val understand_tcc : ?resolve_classes:bool ->
     evar_map -> env -> ?expected_type:types -> rawconstr -> open_constr
     
   val understand_tcc_evars :
-- 
cgit v1.2.3