Imported Upstream version 8.4~betaupstream/8.4_beta

1 files changed, 174 insertions, 209 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index dc339622..193b38dd 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: constrextern.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 (*i*)
 open Pp
 open Util
@@ -23,7 +21,7 @@ open Environ
 open Libnames
 open Impargs
 open Topconstr
-open Rawterm
+open Glob_term
 open Pattern
 open Nametab
 open Notation
@@ -31,7 +29,7 @@ open Reserve
 open Detyping
 (*i*)
 
-(* Translation from rawconstr to front constr *)
+(* Translation from glob_constr to front constr *)
 
 (**********************************************************************)
 (* Parametrization                                                    *)
@@ -76,6 +74,49 @@ let without_symbols f = Flags.with_option print_no_symbol f
 let with_meta_as_hole f = Flags.with_option print_meta_as_hole f
 
 (**********************************************************************)
+(* Control printing of records *)
+
+let is_record indsp =
+  try
+    let _ = Recordops.lookup_structure indsp in
+    true
+  with Not_found -> false
+
+let encode_record r =
+  let indsp = global_inductive r in
+  if not (is_record indsp) then
+    user_err_loc (loc_of_reference r,"encode_record",
+    str "This type is not a structure type.");
+  indsp
+
+module PrintingRecordRecord =
+  PrintingInductiveMake (struct
+    let encode = encode_record
+    let field = "Record"
+    let title = "Types leading to pretty-printing using record notation: "
+    let member_message s b =
+      str "Terms of " ++ s ++
+      str
+      (if b then " are printed using record notation"
+      else " are not printed using record notation")
+  end)
+
+module PrintingRecordConstructor =
+  PrintingInductiveMake (struct
+    let encode = encode_record
+    let field = "Constructor"
+    let title = "Types leading to pretty-printing using constructor form: "
+    let member_message s b =
+      str "Terms of " ++ s ++
+      str
+      (if b then " are printed using constructor form"
+      else " are not printed using constructor form")
+  end)
+
+module PrintingRecord = Goptions.MakeRefTable(PrintingRecordRecord)
+module PrintingConstructor = Goptions.MakeRefTable(PrintingRecordConstructor)
+
+(**********************************************************************)
 (* Various externalisation functions *)
 
 let insert_delimiters e = function
@@ -117,6 +158,8 @@ let rec check_same_pattern p1 p2 =
         check_same_pattern a1 a2
     | CPatCstr(_,c1,a1), CPatCstr(_,c2,a2) when c1=c2 ->
         List.iter2 check_same_pattern a1 a2
+    | CPatCstrExpl(_,c1,a1), CPatCstrExpl(_,c2,a2) when c1=c2 ->
+        List.iter2 check_same_pattern a1 a2
     | CPatAtom(_,r1), CPatAtom(_,r2) when r1=r2 -> ()
     | CPatPrim(_,i1), CPatPrim(_,i2) when i1=i2 -> ()
     | CPatDelimiters(_,s1,e1), CPatDelimiters(_,s2,e2) when s1=s2 ->
@@ -204,82 +247,13 @@ and check_same_fix_binder bl1 bl2 =
 
 let same c d = try check_same_type c d; true with _ -> false
 
-(* Idem for rawconstr *)
-
-let array_iter2 f v1 v2 =
-  List.iter2 f (Array.to_list v1) (Array.to_list v2)
-
-let rec same_patt p1 p2 =
-  match p1, p2 with
-      PatVar(_,na1), PatVar(_,na2) -> if na1<>na2 then failwith "PatVar"
-    | PatCstr(_,c1,pl1,al1), PatCstr(_,c2,pl2,al2) ->
-        if c1<>c2 || al1 <> al2 then failwith "PatCstr";
-        List.iter2 same_patt pl1 pl2
-    | _ -> failwith "same_patt"
-
-let rec same_raw c d =
-  match c,d with
-   | RRef(_,gr1), RRef(_,gr2) -> if gr1<>gr2 then failwith "RRef"
-   | RVar(_,id1), RVar(_,id2) -> if id1<>id2 then failwith "RVar"
-   | REvar(_,e1,a1), REvar(_,e2,a2) ->
-       if e1 <> e2 then failwith "REvar";
-       Option.iter2(List.iter2 same_raw) a1 a2
-  | RPatVar(_,pv1), RPatVar(_,pv2) -> if pv1<>pv2 then failwith "RPatVar"
-  | RApp(_,f1,a1), RApp(_,f2,a2) ->
-      List.iter2 same_raw (f1::a1) (f2::a2)
-  | RLambda(_,na1,bk1,t1,m1), RLambda(_,na2,bk2,t2,m2) ->
-      if na1 <> na2 then failwith "RLambda";
-      same_raw t1 t2; same_raw m1 m2
-  | RProd(_,na1,bk1,t1,m1), RProd(_,na2,bk2,t2,m2) ->
-      if na1 <> na2 then failwith "RProd";
-      same_raw t1 t2; same_raw m1 m2
-  | RLetIn(_,na1,t1,m1), RLetIn(_,na2,t2,m2) ->
-      if na1 <> na2 then failwith "RLetIn";
-      same_raw t1 t2; same_raw m1 m2
-  | RCases(_,_,_,c1,b1), RCases(_,_,_,c2,b2) ->
-      List.iter2
-        (fun (t1,(al1,oind1)) (t2,(al2,oind2)) ->
-          same_raw t1 t2;
-          if al1 <> al2 then failwith "RCases";
-          Option.iter2(fun (_,i1,_,nl1) (_,i2,_,nl2) ->
-            if i1<>i2 || nl1 <> nl2 then failwith "RCases") oind1 oind2) c1 c2;
-      List.iter2 (fun (_,_,pl1,b1) (_,_,pl2,b2) ->
-        List.iter2 same_patt pl1 pl2;
-        same_raw b1 b2) b1 b2
-  | RLetTuple(_,nl1,_,b1,c1), RLetTuple(_,nl2,_,b2,c2) ->
-      if nl1<>nl2 then failwith "RLetTuple";
-      same_raw b1 b2;
-      same_raw c1 c2
-  | RIf(_,b1,_,t1,e1),RIf(_,b2,_,t2,e2) ->
-      same_raw b1 b2; same_raw t1 t2; same_raw e1 e2
-  | RRec(_,fk1,na1,bl1,ty1,def1), RRec(_,fk2,na2,bl2,ty2,def2) ->
-      if fk1 <> fk2 || na1 <> na2 then failwith "RRec";
-      array_iter2
-        (List.iter2 (fun (na1,bk1,bd1,ty1) (na2,bk2,bd2,ty2) ->
-          if na1<>na2 then failwith "RRec";
-          Option.iter2 same_raw bd1 bd2;
-          same_raw ty1 ty2)) bl1 bl2;
-      array_iter2 same_raw ty1 ty2;
-      array_iter2 same_raw def1 def2
-  | RSort(_,s1), RSort(_,s2) -> if s1<>s2 then failwith "RSort"
-  | RHole _, _ -> ()
-  | _, RHole _ -> ()
-  | RCast(_,c1,_),r2 -> same_raw c1 r2
-  | r1, RCast(_,c2,_) -> same_raw r1 c2
-  | RDynamic(_,d1), RDynamic(_,d2) -> if d1<>d2 then failwith"RDynamic"
-  | _ -> failwith "same_raw"
-
-let same_rawconstr c d =
-  try same_raw c d; true
-  with Failure _ | Invalid_argument _ -> false
-
 (**********************************************************************)
 (* mapping patterns to cases_pattern_expr                                *)
 
 let has_curly_brackets ntn =
   String.length ntn >= 6 & (String.sub ntn 0 6 = "{ _ } " or
     String.sub ntn (String.length ntn - 6) 6 = " { _ }" or
-    string_string_contains ntn " { _ } ")
+    string_string_contains ~where:ntn ~what:" { _ } ")
 
 let rec wildcards ntn n =
   if n = String.length ntn then []
@@ -347,7 +321,7 @@ let mkPat loc qid l =
   (* Normally irrelevant test with v8 syntax, but let's do it anyway *)
   if l = [] then CPatAtom (loc,Some qid) else CPatCstr (loc,qid,l)
 
- (* Better to use extern_rawconstr composed with injection/retraction ?? *)
+ (* Better to use extern_glob_constr composed with injection/retraction ?? *)
 let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
   try
     if !Flags.raw_print or !print_no_symbol then raise No_match;
@@ -370,7 +344,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
       let args = List.map (extern_cases_pattern_in_scope scopes vars) args in
       let p =
 	try
-	  if !Flags.raw_print then raise Exit;
+          if !Flags.raw_print then raise Exit;
 	  let projs = Recordops.lookup_projections (fst cstrsp) in
 	  let rec ip projs args acc =
 	    match projs with
@@ -464,8 +438,11 @@ let is_projection nargs = function
 
 let is_hole = function CHole _ -> true | _ -> false
 
-let is_significant_implicit a impl tail =
-  not (is_hole a) or (tail = [] & not (List.for_all is_status_implicit impl))
+let is_significant_implicit a =
+  not (is_hole a)
+
+let is_needed_for_correct_partial_application tail imp =
+  tail = [] & not (maximal_insertion_of imp)
 
 (* Implicit args indexes are in ascending order *)
 (* inctx is useful only if there is a last argument to be deduced from ctxt *)
@@ -477,8 +454,9 @@ let explicitize loc inctx impl (cf,f) args =
         let visible =
           !Flags.raw_print or
           (!print_implicits & !print_implicits_explicit_args) or
+          (is_needed_for_correct_partial_application tail imp) or
 	  (!print_implicits_defensive &
-	   is_significant_implicit a impl tail &
+	   is_significant_implicit a &
 	   not (is_inferable_implicit inctx n imp))
 	in
         if visible then
@@ -532,7 +510,7 @@ let rec extern_args extern scopes env args subscopes =
 	extern argscopes env a :: extern_args extern scopes env args subscopes
 
 let rec remove_coercions inctx = function
-  | RApp (loc,RRef (_,r),args) as c
+  | GApp (loc,GRef (_,r),args) as c
       when  not (!Flags.raw_print or !print_coercions)
       ->
       let nargs = List.length args in
@@ -551,22 +529,17 @@ let rec remove_coercions inctx = function
 		 been confused with ordinary application or would have need
                  a surrounding context and the coercion to funclass would
                  have been made explicit to match *)
-	      if l = [] then a' else RApp (loc,a',l)
+	      if l = [] then a' else GApp (loc,a',l)
 	  | _ -> c
       with Not_found -> c)
   | c -> c
 
 let rec flatten_application = function
-  | RApp (loc,RApp(_,a,l'),l) -> flatten_application (RApp (loc,a,l'@l))
+  | GApp (loc,GApp(_,a,l'),l) -> flatten_application (GApp (loc,a,l'@l))
   | a -> a
 
-let rec rename_rawconstr_var id0 id1 = function
-    RRef(loc,VarRef id) when id=id0 -> RRef(loc,VarRef id1)
-  | RVar(loc,id) when id=id0 -> RVar(loc,id1)
-  | c -> map_rawconstr (rename_rawconstr_var id0 id1) c
-
 (**********************************************************************)
-(* mapping rawterms to numerals (in presence of coercions, choose the *)
+(* mapping glob_constr to numerals (in presence of coercions, choose the *)
 (* one with no delimiter if possible)                                 *)
 
 let extern_possible_prim_token scopes r =
@@ -574,7 +547,7 @@ let extern_possible_prim_token scopes r =
     let (sc,n) = uninterp_prim_token r in
     match availability_of_prim_token n sc scopes with
     | None -> None
-    | Some key -> Some (insert_delimiters (CPrim (loc_of_rawconstr r,n)) key)
+    | Some key -> Some (insert_delimiters (CPrim (loc_of_glob_constr r,n)) key)
   with No_match ->
     None
 
@@ -586,12 +559,12 @@ let extern_optimal_prim_token scopes r r' =
   | _ -> raise No_match
 
 (**********************************************************************)
-(* mapping rawterms to constr_expr                                    *)
+(* mapping glob_constr to constr_expr                                    *)
 
-let extern_rawsort = function
-  | RProp _ as s -> s
-  | RType (Some _) as s when !print_universes -> s
-  | RType _ -> RType None
+let extern_glob_sort = function
+  | GProp _ as s -> s
+  | GType (Some _) as s when !print_universes -> s
+  | GType _ -> GType None
 
 let rec extern inctx scopes vars r =
   let r' = remove_coercions inctx r in
@@ -604,31 +577,37 @@ let rec extern inctx scopes vars r =
     if !Flags.raw_print or !print_no_symbol then raise No_match;
     extern_symbol scopes vars r'' (uninterp_notations r'')
   with No_match -> match r' with
-  | RRef (loc,ref) ->
+  | GRef (loc,ref) ->
       extern_global loc (select_stronger_impargs (implicits_of_global ref))
         (extern_reference loc vars ref)
 
-  | RVar (loc,id) -> CRef (Ident (loc,id))
+  | GVar (loc,id) -> CRef (Ident (loc,id))
 
-  | REvar (loc,n,None) when !print_meta_as_hole -> CHole (loc, None)
+  | GEvar (loc,n,None) when !print_meta_as_hole -> CHole (loc, None)
 
-  | REvar (loc,n,l) ->
+  | GEvar (loc,n,l) ->
       extern_evar loc n (Option.map (List.map (extern false scopes vars)) l)
 
-  | RPatVar (loc,n) ->
+  | GPatVar (loc,n) ->
       if !print_meta_as_hole then CHole (loc, None) else CPatVar (loc,n)
 
-  | RApp (loc,f,args) ->
+  | GApp (loc,f,args) ->
       (match f with
-	 | RRef (rloc,ref) ->
+	 | GRef (rloc,ref) ->
 	     let subscopes = find_arguments_scope ref in
 	     let args =
 	       extern_args (extern true) (snd scopes) vars args subscopes in
 	     begin
 	       try
-		 if !Flags.raw_print then raise Exit;
+                 if !Flags.raw_print then raise Exit;
 		 let cstrsp = match ref with ConstructRef c -> c | _ -> raise Not_found in
 		 let struc = Recordops.lookup_structure (fst cstrsp) in
+                 if PrintingRecord.active (fst cstrsp) then
+                   ()
+                 else if PrintingConstructor.active (fst cstrsp) then
+                   raise Exit
+                 else if not !Flags.record_print then
+                   raise Exit;
 		 let projs = struc.Recordops.s_PROJ in
 		 let locals = struc.Recordops.s_PROJKIND in
 		 let rec cut args n =
@@ -666,66 +645,66 @@ let rec extern inctx scopes vars r =
 	     explicitize loc inctx [] (None,sub_extern false scopes vars f)
                (List.map (sub_extern true scopes vars) args))
 
-  | RProd (loc,Anonymous,_,t,c) ->
+  | GProd (loc,Anonymous,_,t,c) ->
       (* Anonymous product are never factorized *)
       CArrow (loc,extern_typ scopes vars t, extern_typ scopes vars c)
 
-  | RLetIn (loc,na,t,c) ->
+  | GLetIn (loc,na,t,c) ->
       CLetIn (loc,(loc,na),sub_extern false scopes vars t,
               extern inctx scopes (add_vname vars na) c)
 
-  | RProd (loc,na,bk,t,c) ->
+  | GProd (loc,na,bk,t,c) ->
       let t = extern_typ scopes vars (anonymize_if_reserved na t) in
       let (idl,c) = factorize_prod scopes (add_vname vars na) t c in
       CProdN (loc,[(dummy_loc,na)::idl,Default bk,t],c)
 
-  | RLambda (loc,na,bk,t,c) ->
+  | GLambda (loc,na,bk,t,c) ->
       let t = extern_typ scopes vars (anonymize_if_reserved na t) in
       let (idl,c) = factorize_lambda inctx scopes (add_vname vars na) t c in
       CLambdaN (loc,[(dummy_loc,na)::idl,Default bk,t],c)
 
-  | RCases (loc,sty,rtntypopt,tml,eqns) ->
+  | GCases (loc,sty,rtntypopt,tml,eqns) ->
       let vars' =
 	List.fold_right (name_fold Idset.add)
 	  (cases_predicate_names tml) vars in
       let rtntypopt' = Option.map (extern_typ scopes vars') rtntypopt in
       let tml = List.map (fun (tm,(na,x)) ->
         let na' = match na,tm with
-            Anonymous, RVar (_,id) when
-              rtntypopt<>None & occur_rawconstr id (Option.get rtntypopt)
+            Anonymous, GVar (_,id) when
+              rtntypopt<>None & occur_glob_constr id (Option.get rtntypopt)
               -> Some (dummy_loc,Anonymous)
           | Anonymous, _ -> None
-          | Name id, RVar (_,id') when id=id' -> None
+          | Name id, GVar (_,id') when id=id' -> None
           | Name _, _ -> Some (dummy_loc,na) in
 	(sub_extern false scopes vars tm,
 	(na',Option.map (fun (loc,ind,n,nal) ->
 	  let params = list_tabulate
-	    (fun _ -> RHole (dummy_loc,Evd.InternalHole)) n in
+	    (fun _ -> GHole (dummy_loc,Evd.InternalHole)) n in
 	  let args = List.map (function
-	    | Anonymous -> RHole (dummy_loc,Evd.InternalHole)
-	    | Name id -> RVar (dummy_loc,id)) nal in
-	  let t = RApp (dummy_loc,RRef (dummy_loc,IndRef ind),params@args) in
+	    | Anonymous -> GHole (dummy_loc,Evd.InternalHole)
+	    | Name id -> GVar (dummy_loc,id)) nal in
+	  let t = GApp (dummy_loc,GRef (dummy_loc,IndRef ind),params@args) in
 	  (extern_typ scopes vars t)) x))) tml in
       let eqns = List.map (extern_eqn inctx scopes vars) eqns in
       CCases (loc,sty,rtntypopt',tml,eqns)
 
-  | RLetTuple (loc,nal,(na,typopt),tm,b) ->
+  | GLetTuple (loc,nal,(na,typopt),tm,b) ->
       CLetTuple (loc,List.map (fun na -> (dummy_loc,na)) nal,
         (Option.map (fun _ -> (dummy_loc,na)) typopt,
          Option.map (extern_typ scopes (add_vname vars na)) typopt),
         sub_extern false scopes vars tm,
         extern inctx scopes (List.fold_left add_vname vars nal) b)
 
-  | RIf (loc,c,(na,typopt),b1,b2) ->
+  | GIf (loc,c,(na,typopt),b1,b2) ->
       CIf (loc,sub_extern false scopes vars c,
         (Option.map (fun _ -> (dummy_loc,na)) typopt,
          Option.map (extern_typ scopes (add_vname vars na)) typopt),
         sub_extern inctx scopes vars b1, sub_extern inctx scopes vars b2)
 
-  | RRec (loc,fk,idv,blv,tyv,bv) ->
+  | GRec (loc,fk,idv,blv,tyv,bv) ->
       let vars' = Array.fold_right Idset.add idv vars in
       (match fk with
-	 | RFix (nv,n) ->
+	 | GFix (nv,n) ->
 	     let listdecl =
 	       Array.mapi (fun i fi ->
                  let (bl,ty,def) = blv.(i), tyv.(i), bv.(i) in
@@ -742,7 +721,7 @@ let rec extern inctx scopes vars r =
                   extern false scopes vars1 def)) idv
 	     in
 	     CFix (loc,(loc,idv.(n)),Array.to_list listdecl)
-	 | RCoFix n ->
+	 | GCoFix n ->
 	     let listdecl =
                Array.mapi (fun i fi ->
                  let (_,ids,bl) = extern_local_binder scopes vars blv.(i) in
@@ -753,17 +732,15 @@ let rec extern inctx scopes vars r =
 	     in
 	     CCoFix (loc,(loc,idv.(n)),Array.to_list listdecl))
 
-  | RSort (loc,s) -> CSort (loc,extern_rawsort s)
+  | GSort (loc,s) -> CSort (loc,extern_glob_sort s)
 
-  | RHole (loc,e) -> CHole (loc, Some e)
+  | GHole (loc,e) -> CHole (loc, Some e)
 
-  | RCast (loc,c, CastConv (k,t)) ->
+  | GCast (loc,c, CastConv (k,t)) ->
       CCast (loc,sub_extern true scopes vars c, CastConv (k,extern_typ scopes vars t))
-  | RCast (loc,c, CastCoerce) ->
+  | GCast (loc,c, CastCoerce) ->
       CCast (loc,sub_extern true scopes vars c, CastCoerce)
 
-  | RDynamic (loc,d) -> CDynamic (loc,d)
-
 and extern_typ (_,scopes) =
   extern true (Some Notation.type_scope,scopes)
 
@@ -774,7 +751,7 @@ and factorize_prod scopes vars aty c =
     if !Flags.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),bk,ty,c)
+  | GProd (loc,(Name id as na),bk,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 *)
 	-> let (nal,c) = factorize_prod scopes (Idset.add id vars) aty c in
@@ -786,7 +763,7 @@ and factorize_lambda inctx scopes vars aty c =
     if !Flags.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,bk,ty,c)
+  | GLambda (loc,na,bk,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 *)
 	-> let (nal,c) =
@@ -822,33 +799,40 @@ and extern_eqn inctx scopes vars (loc,ids,pl,c) =
 and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
   | [] -> raise No_match
   | (keyrule,pat,n as _rule)::rules ->
-      let loc = Rawterm.loc_of_rawconstr t in
+      let loc = Glob_term.loc_of_glob_constr t in
       try
 	(* Adjusts to the number of arguments expected by the notation *)
 	let (t,args,argsscopes,argsimpls) = match t,n with
-	  | RApp (_,(RRef (_,ref) as f),args), Some n
+	  | GApp (_,f,args), Some n
 	      when List.length args >= n ->
 	      let args1, args2 = list_chop n args in
-	      let subscopes =
-		try list_skipn n (find_arguments_scope ref) with _ -> [] in
-	      let impls =
-		let impls =
-		  select_impargs_size
-		    (List.length args) (implicits_of_global ref) in
-		try list_skipn n impls with _ -> [] in
-	      (if n = 0 then f else RApp (dummy_loc,f,args1)),
+              let subscopes, impls =
+                match f with
+                | GRef (_,ref) ->
+	          let subscopes =
+		    try list_skipn n (find_arguments_scope ref) with _ -> [] in
+	          let impls =
+		    let impls =
+		      select_impargs_size
+		        (List.length args) (implicits_of_global ref) in
+		    try list_skipn n impls with _ -> [] in
+                  subscopes,impls
+                | _ ->
+                  [], [] in
+	      (if n = 0 then f else GApp (dummy_loc,f,args1)),
 	      args2, subscopes, impls
-	  | RApp (_,(RRef (_,ref) as f),args), None ->
+	  | GApp (_,(GRef (_,ref) as f),args), None ->
 	      let subscopes = find_arguments_scope ref in
 	      let impls =
 		  select_impargs_size
 		    (List.length args) (implicits_of_global ref) in
 	      f, args, subscopes, impls
-	  | RRef _, Some 0 -> RApp (dummy_loc,t,[]), [], [], []
+	  | GRef _, Some 0 -> GApp (dummy_loc,t,[]), [], [], []
           | _, None -> t, [], [], []
           | _ -> raise No_match in
 	(* Try matching ... *)
-	let terms,termlists,binders = match_aconstr t pat in
+	let terms,termlists,binders =
+          match_aconstr !print_universes t pat in
 	(* Try availability of interpretation ... *)
         let e =
           match keyrule with
@@ -888,16 +872,16 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
 	  No_match -> extern_symbol allscopes vars t rules
 
 and extern_recursion_order scopes vars = function
-    RStructRec -> CStructRec
-  | RWfRec c -> CWfRec (extern true scopes vars c)
-  | RMeasureRec (m,r) -> CMeasureRec (extern true scopes vars m,
+    GStructRec -> CStructRec
+  | GWfRec c -> CWfRec (extern true scopes vars c)
+  | GMeasureRec (m,r) -> CMeasureRec (extern true scopes vars m,
 				     Option.map (extern true scopes vars) r)
 
 
-let extern_rawconstr vars c =
+let extern_glob_constr vars c =
   extern false (None,[]) vars c
 
-let extern_rawtype vars c =
+let extern_glob_type vars c =
   extern_typ (None,[]) vars c
 
 (******************************************************************)
@@ -920,89 +904,70 @@ let extern_constr at_top env t =
 let extern_type at_top env t =
   let avoid = if at_top then ids_of_context env else [] in
   let r = Detyping.detype at_top avoid (names_of_rel_context env) t in
-  extern_rawtype (vars_of_env env) r
+  extern_glob_type (vars_of_env env) r
 
-let extern_sort s = extern_rawsort (detype_sort s)
+let extern_sort s = extern_glob_sort (detype_sort s)
 
 (******************************************************************)
 (* Main translation function from pattern -> constr_expr *)
 
-let rec raw_of_pat env = function
-  | PRef ref -> RRef (loc,ref)
-  | PVar id -> RVar (loc,id)
-  | PEvar (n,l) -> REvar (loc,n,Some (array_map_to_list (raw_of_pat env) l))
+let any_any_branch =
+  (* | _ => _ *)
+  (loc,[],[PatVar (loc,Anonymous)],GHole (loc,Evd.InternalHole))
+
+let rec glob_of_pat env = function
+  | PRef ref -> GRef (loc,ref)
+  | PVar id -> GVar (loc,id)
+  | PEvar (n,l) -> GEvar (loc,n,Some (array_map_to_list (glob_of_pat env) l))
   | PRel n ->
       let id = try match lookup_name_of_rel n env with
 	| Name id   -> id
 	| Anonymous ->
-	    anomaly "rawconstr_of_pattern: index to an anonymous variable"
+	    anomaly "glob_constr_of_pattern: index to an anonymous variable"
       with Not_found -> id_of_string ("_UNBOUND_REL_"^(string_of_int n)) in
-      RVar (loc,id)
-  | PMeta None -> RHole (loc,Evd.InternalHole)
-  | PMeta (Some n) -> RPatVar (loc,(false,n))
+      GVar (loc,id)
+  | PMeta None -> GHole (loc,Evd.InternalHole)
+  | PMeta (Some n) -> GPatVar (loc,(false,n))
   | PApp (f,args) ->
-      RApp (loc,raw_of_pat env f,array_map_to_list (raw_of_pat env) args)
+      GApp (loc,glob_of_pat env f,array_map_to_list (glob_of_pat env) args)
   | PSoApp (n,args) ->
-      RApp (loc,RPatVar (loc,(true,n)),
-        List.map (raw_of_pat env) args)
+      GApp (loc,GPatVar (loc,(true,n)),
+        List.map (glob_of_pat env) args)
   | PProd (na,t,c) ->
-      RProd (loc,na,Explicit,raw_of_pat env t,raw_of_pat (na::env) c)
+      GProd (loc,na,Explicit,glob_of_pat env t,glob_of_pat (na::env) c)
   | PLetIn (na,t,c) ->
-      RLetIn (loc,na,raw_of_pat env t, raw_of_pat (na::env) c)
+      GLetIn (loc,na,glob_of_pat env t, glob_of_pat (na::env) c)
   | PLambda (na,t,c) ->
-      RLambda (loc,na,Explicit,raw_of_pat env t, raw_of_pat (na::env) c)
+      GLambda (loc,na,Explicit,glob_of_pat env t, glob_of_pat (na::env) c)
   | PIf (c,b1,b2) ->
-      RIf (loc, raw_of_pat env c, (Anonymous,None),
-           raw_of_pat env b1, raw_of_pat env b2)
-  | PCase ((LetStyle,[|n|],ind,None),PMeta None,tm,[|b|]) ->
-      let nal,b = it_destRLambda_or_LetIn_names n (raw_of_pat env b) in
-      RLetTuple (loc,nal,(Anonymous,None),raw_of_pat env tm,b)
-  | PCase (_,PMeta None,tm,[||]) ->
-      RCases (loc,RegularStyle,None,[raw_of_pat env tm,(Anonymous,None)],[])
-  | PCase ((_,cstr_nargs,indo,ind_nargs),p,tm,bv) ->
-      let brs = Array.to_list (Array.map (raw_of_pat env) bv) in
-      let brns = Array.to_list cstr_nargs in
-        (* ind is None only if no branch and no return type *)
-      let ind = Option.get indo in
-      let mat = simple_cases_matrix_of_branches ind brns brs in
-      let indnames,rtn =
-	if p = PMeta None then (Anonymous,None),None
-	else
-	  let nparams,n = Option.get ind_nargs in
-	  return_type_of_predicate ind nparams n (raw_of_pat env p) in
-      RCases (loc,RegularStyle,rtn,[raw_of_pat env tm,indnames],mat)
+      GIf (loc, glob_of_pat env c, (Anonymous,None),
+           glob_of_pat env b1, glob_of_pat env b2)
+  | PCase ({cip_style=LetStyle; cip_ind_args=None},PMeta None,tm,[(0,n,b)]) ->
+      let nal,b = it_destRLambda_or_LetIn_names n (glob_of_pat env b) in
+      GLetTuple (loc,nal,(Anonymous,None),glob_of_pat env tm,b)
+  | PCase (info,p,tm,bl) ->
+      let mat = match bl, info.cip_ind with
+	| [], _ -> []
+	| _, Some ind ->
+	  let bl' = List.map (fun (i,n,c) -> (i,n,glob_of_pat env c)) bl in
+	  simple_cases_matrix_of_branches ind bl'
+	| _, None -> anomaly "PCase with some branches but unknown inductive"
+      in
+      let mat = if info.cip_extensible then mat @ [any_any_branch] else mat
+      in
+      let indnames,rtn = match p, info.cip_ind, info.cip_ind_args with
+	| PMeta None, _, _ -> (Anonymous,None),None
+	| _, Some ind, Some (nparams,nargs) ->
+	  return_type_of_predicate ind nparams nargs (glob_of_pat env p)
+	| _ -> anomaly "PCase with non-trivial predicate but unknown inductive"
+      in
+      GCases (loc,RegularStyle,rtn,[glob_of_pat env tm,indnames],mat)
   | PFix f -> Detyping.detype false [] env (mkFix f)
   | PCoFix c -> Detyping.detype false [] env (mkCoFix c)
-  | PSort s -> RSort (loc,s)
-
-and raw_of_eqn env constr construct_nargs branch =
-  let make_pat x env b ids =
-    let avoid = List.fold_right (name_fold (fun x l -> x::l)) env [] in
-    let id = next_name_away_with_default "x" x avoid in
-    PatVar (dummy_loc,Name id),(Name id)::env,id::ids
-  in
-  let rec buildrec ids patlist env n b =
-    if n=0 then
-      (dummy_loc, ids,
-       [PatCstr(dummy_loc, constr, List.rev patlist,Anonymous)],
-       raw_of_pat env b)
-    else
-      match b with
-	| PLambda (x,_,b) ->
-	    let pat,new_env,new_ids = make_pat x env b ids in
-            buildrec new_ids (pat::patlist) new_env (n-1) b
-
-	| PLetIn (x,_,b) ->
-	    let pat,new_env,new_ids = make_pat x env b ids in
-            buildrec new_ids (pat::patlist) new_env (n-1) b
-
-	| _ ->
-	    error "Unsupported branch in case-analysis while printing pattern."
-  in
-  buildrec [] [] env construct_nargs branch
+  | PSort s -> GSort (loc,s)
 
 let extern_constr_pattern env pat =
-  extern true (None,[]) Idset.empty (raw_of_pat env pat)
+  extern true (None,[]) Idset.empty (glob_of_pat env pat)
 
 let extern_rel_context where env sign =
   let a = detype_rel_context where [] (names_of_rel_context env) sign in