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
---
 parsing/g_constr.ml4 | 2 +-
 parsing/ppconstr.ml  | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'parsing')

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 9c8632a6d3..835d66434d 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -293,7 +293,7 @@ GEXTEND Gram
         (match p with
           | CPatAtom (_, Some r) -> CPatCstr (loc, r, lp)
           | _ -> Util.user_err_loc 
-              (cases_pattern_loc p, "compound_pattern",
+              (cases_pattern_expr_loc p, "compound_pattern",
                Pp.str "Constructor expected"))
       | p = pattern; "as"; id = ident ->
 	  CPatAlias (loc, p, id) ]
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 4ac2cbe9e0..a003c14059 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -178,7 +178,7 @@ let rec pr_patt sep inh p =
   | CPatPrim (_,p) -> pr_prim_token p, latom
   | CPatDelimiters (_,k,p) -> pr_delimiters k (pr_patt mt lsimple p), 1
   in
-  let loc = cases_pattern_loc p in
+  let loc = cases_pattern_expr_loc p in
   pr_with_comments loc
     (sep() ++ if prec_less prec inh then strm else surround strm)
 
-- 
cgit v1.2.3