From 208a0f7bfa5249f9795e6e225f309cbe715c0fad Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Tue, 21 Nov 2006 21:38:49 +0000
Subject: Imported Upstream version 8.1~gamma

---
 pretyping/rawterm.mli | 13 ++++++++++---
 1 file changed, 10 insertions(+), 3 deletions(-)

(limited to 'pretyping/rawterm.mli')

diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 89b13ff0..6c2276d7 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: rawterm.mli 8969 2006-06-22 12:51:04Z msozeau $ i*)
+(*i $Id: rawterm.mli 9226 2006-10-09 16:11:01Z herbelin $ i*)
 
 (*i*)
 open Util
@@ -17,7 +17,8 @@ open Libnames
 open Nametab
 (*i*)
 
-(* Untyped intermediate terms, after ASTs and before constr. *)
+(**********************************************************************)
+(* The kind of patterns that occurs in "match ... with ... end"       *)
 
 (* locs here refers to the ident's location, not whole pat *)
 (* the last argument of PatCstr is a possible alias ident for the pattern *)
@@ -25,7 +26,13 @@ type cases_pattern =
   | PatVar of loc * name
   | PatCstr of loc * constructor * cases_pattern list * name
 
-val pattern_loc : cases_pattern -> loc
+val cases_pattern_loc : cases_pattern -> loc
+
+(**********************************************************************)
+(* Untyped intermediate terms, after constr_expr and before constr    *)
+(* Resolution of names, insertion of implicit arguments placeholder,  *)
+(* and notations are done, but coercions, inference of implicit       *)
+(* arguments and pattern-matching compilation are not                 *)
 
 type patvar = identifier
 
-- 
cgit v1.2.3