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
---
 interp/constrextern.ml | 14 +++++++++++---
 1 file changed, 11 insertions(+), 3 deletions(-)

(limited to 'interp/constrextern.ml')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 600392811b..d386622946 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -405,7 +405,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
     match availability_of_prim_token sc scopes with
     | None -> raise No_match
     | Some key ->
-      let loc = pattern_loc pat in
+      let loc = cases_pattern_loc pat in
       insert_pat_alias loc (insert_pat_delimiters loc (CPatPrim(loc,p)) key) na
   with No_match ->
   try 
@@ -754,7 +754,11 @@ and extern_typ (_,scopes) =
 
 and sub_extern inctx (_,scopes) = extern inctx (None,scopes)
 
-and factorize_prod scopes vars aty = function
+and factorize_prod scopes vars aty c =
+  try 
+    if !Options.raw_print or !print_no_symbol then raise No_match;
+    ([],extern_symbol scopes vars c (uninterp_notations c))
+  with No_match -> match c with
   | RProd (loc,(Name id as na),ty,c)
       when same aty (extern_typ scopes vars (anonymize_if_reserved na ty))
 	& not (occur_var_constr_expr id aty) (* avoid na in ty escapes scope *)
@@ -762,7 +766,11 @@ and factorize_prod scopes vars aty = function
            ((loc,Name id)::nal,c)
   | c -> ([],extern_typ scopes vars c)
 
-and factorize_lambda inctx scopes vars aty = function
+and factorize_lambda inctx scopes vars aty c =
+  try 
+    if !Options.raw_print or !print_no_symbol then raise No_match;
+    ([],extern_symbol scopes vars c (uninterp_notations c))
+  with No_match -> match c with
   | RLambda (loc,na,ty,c)
       when same aty (extern_typ scopes vars (anonymize_if_reserved na ty))
 	& not (occur_name na aty) (* To avoid na in ty' escapes scope *)
-- 
cgit v1.2.3