Imported Upstream version 8.0pl3upstream/8.0pl3

3 files changed, 44 insertions, 24 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 6692dca5..25167865 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: constrextern.ml,v 1.85.2.2 2004/07/16 19:30:22 herbelin Exp $ *)
+(* $Id: constrextern.ml,v 1.85.2.7 2006/01/05 12:00:35 herbelin Exp $ *)
 
 (*i*)
 open Pp
@@ -1333,7 +1333,8 @@ and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function
                       subst in
 		  insert_pat_delimiters (make_pat_notation loc ntn l) key)
           | SynDefRule kn ->
- 	      CPatAtom (loc,Some (Qualid (loc, shortest_qualid_of_syndef kn)))
+	      let qid = shortest_qualid_of_syndef vars kn in
+ 	      CPatAtom (loc,Some (Qualid (loc, qid)))
       with
 	  No_match -> extern_symbol_pattern allscopes vars t rules
 
@@ -1494,21 +1495,38 @@ let rec share_fix_binders n rbl ty def =
     | _ -> List.rev rbl, ty, def
 
 (**********************************************************************)
+(* mapping rawterms to numerals (in presence of coercions, choose the *)
+(* one with no delimiter if possible)                                 *)
+
+let extern_possible_numeral scopes r =
+  try
+    let (sc,n) = uninterp_numeral r in
+    match Symbols.availability_of_numeral sc (make_current_scopes scopes) with
+    | None -> None
+    | Some key -> Some (insert_delimiters (CNumeral(loc_of_rawconstr r,n)) key)
+  with No_match ->
+    None
+
+let extern_optimal_numeral scopes r r' =
+  let c = extern_possible_numeral scopes r in
+  let c' = if r==r' then None else extern_possible_numeral scopes r' in
+  match c,c' with
+  | Some n, (Some (CDelimiters _) | None) | _, Some n -> n
+  | _ -> raise No_match
+
+(**********************************************************************)
 (* mapping rawterms to constr_expr                                    *)
 
 let rec extern inctx scopes vars r =
+  let r' = remove_coercions inctx r in
   try 
     if !Options.raw_print or !print_no_symbol then raise No_match;
-    extern_numeral (Rawterm.loc_of_rawconstr r)
-      scopes (Symbols.uninterp_numeral r)
+    extern_optimal_numeral scopes r r'
   with No_match ->
-
-  let r = remove_coercions inctx r in
-
   try 
     if !Options.raw_print or !print_no_symbol then raise No_match;
-    extern_symbol scopes vars r (Symbols.uninterp_notations r)
-  with No_match -> match r with
+    extern_symbol scopes vars r' (Symbols.uninterp_notations r')
+  with No_match -> match r' with
   | RRef (loc,ref) ->
       extern_global loc (implicits_of_global_out ref)
         (extern_reference loc vars ref)
@@ -1605,13 +1623,15 @@ let rec extern inctx scopes vars r =
 
   | RLetTuple (loc,nal,(na,typopt),tm,b) ->
       CLetTuple (loc,nal,
-        (Some na,option_app (extern_type scopes (add_vname vars na)) typopt),
+        (option_app (fun _ -> na) typopt,
+         option_app (extern_type scopes (add_vname vars na)) typopt),
         sub_extern false scopes vars tm,
         extern false scopes (List.fold_left add_vname vars nal) b)
 
   | RIf (loc,c,(na,typopt),b1,b2) ->
       CIf (loc,sub_extern false scopes vars c,
-        (Some na,option_app (extern_type scopes (add_vname vars na)) typopt),
+        (option_app (fun _ -> na) typopt,
+         option_app (extern_type scopes (add_vname vars na)) typopt),
         sub_extern false scopes vars b1, sub_extern false scopes vars b2)
 
   | RRec (loc,fk,idv,blv,tyv,bv) ->
@@ -1709,11 +1729,6 @@ and extern_eqn inctx scopes vars (loc,ids,pl,c) =
   (loc,List.map (extern_cases_pattern_in_scope scopes vars) pl,
    extern inctx scopes vars c)
 
-and extern_numeral loc scopes (sc,n) =
-  match Symbols.availability_of_numeral sc (make_current_scopes scopes) with
-    | None -> raise No_match
-    | Some key -> insert_delimiters (CNumeral (loc,n)) key
-
 and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
   | [] -> raise No_match
   | (keyrule,pat,n as rule)::rules ->
@@ -1745,7 +1760,7 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
                       subst in
 	          insert_delimiters (make_notation loc ntn l) key)
           | SynDefRule kn ->
-              CRef (Qualid (loc, shortest_qualid_of_syndef kn)) in
+              CRef (Qualid (loc, shortest_qualid_of_syndef vars kn)) in
  	if args = [] then e 
 	else
 	  (* TODO: compute scopt for the extra args, in case, head is a ref *)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 222ea23b..bacdb387 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: constrintern.ml,v 1.58.2.6 2004/11/22 14:21:23 herbelin Exp $ *)
+(* $Id: constrintern.ml,v 1.58.2.7 2005/11/19 10:34:35 herbelin Exp $ *)
 
 open Pp
 open Util
@@ -621,10 +621,10 @@ let merge_impargs l args =
 
 let check_projection isproj nargs r = 
   match (r,isproj) with
-  | RRef (loc, ref), Some nth ->
+  | RRef (loc, ref), Some _ ->
       (try
-	let n = Recordops.find_projection_nparams ref in
-	if nargs < nth then 
+	let n = Recordops.find_projection_nparams ref + 1 in
+	if nargs < n then 
 	  user_err_loc (loc,"",str "Projection has not enough parameters");
       with Not_found -> 
 	user_err_loc
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index ef887d88..ceda2b47 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: syntax_def.ml,v 1.6.2.1 2004/07/16 19:30:23 herbelin Exp $ *)
+(* $Id: syntax_def.ml,v 1.6.2.2 2006/01/03 20:33:31 herbelin Exp $ *)
 
 open Util
 open Pp
@@ -39,10 +39,15 @@ let load_syntax_constant i ((sp,kn),(local,c,onlyparse)) =
   add_syntax_constant kn c;
   Nametab.push_syntactic_definition (Nametab.Until i) sp kn;
   if not onlyparse then
+    (* Declare it to be used as (long) name *)
     Symbols.declare_uninterpretation (Symbols.SynDefRule kn) ([],c)
 
-let open_syntax_constant i ((sp,kn),c) =
-  Nametab.push_syntactic_definition (Nametab.Exactly i) sp kn
+let open_syntax_constant i ((sp,kn),(_,c,onlyparse)) =
+  Nametab.push_syntactic_definition (Nametab.Exactly i) sp kn;
+  if not onlyparse then
+    (* Redeclare it to be used as (short) name in case an other (distfix)
+       notation was declared inbetween *)
+    Symbols.declare_uninterpretation (Symbols.SynDefRule kn) ([],c)
 
 let cache_syntax_constant d =
   load_syntax_constant 1 d