From 366fa1bdea12b522c98984f50428ef8aa48cf8d0 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 9 Oct 2006 16:11:01 +0000
Subject: Notations: - prise en compte des variables liées non liées par la
 notation (bug #1186), - test pour affichage des notations aussi sur les
 sous-ensembles   des lieurs multiples (cf notation "#" dans
 output/Notations.v), - extension, correction et uniformisation de quelques
 fonctions sur   les constr_expr et cases_pattern (avec incidences sur
 rawterm.ml,   parsing et contrib/interface).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9226 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/rawterm.ml  |  2 +-
 pretyping/rawterm.mli | 11 +++++++++--
 2 files changed, 10 insertions(+), 3 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index 78e616d98a..e426e299b3 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -26,7 +26,7 @@ type cases_pattern =
   | PatVar of loc * name
   | PatCstr of loc * constructor * cases_pattern list * name
 
-let pattern_loc = function
+let cases_pattern_loc = function
     PatVar(loc,_) -> loc
   | PatCstr(loc,_,_,_) -> loc
 
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index c61c61b0f3..8d1ac2e656 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -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