1 files changed, 130 insertions, 104 deletions

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 9ba5949a..0dc5a9ba 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -14,6 +14,7 @@ open Pp
 open CErrors
 open Util
 open Names
+open Constr
 open Term
 open EConstr
 open Vars
@@ -26,7 +27,6 @@ open Libnames
 open Globnames
 open Nametab
 open Mod_subst
-open Misctypes
 open Decl_kinds
 open Context.Named.Declaration
 open Ltac_pretype
@@ -36,7 +36,7 @@ type _ delay =
 | Later : [ `thunk ] delay
 
 (** Should we keep details of universes during detyping ? *)
-let print_universes = Flags.univ_print
+let print_universes = ref false
 
 (** If true, prints local context of evars, whatever print_arguments *)
 let print_evar_arguments = ref false
@@ -87,7 +87,7 @@ let encode_tuple ({CAst.loc} as r) =
 
 module PrintingInductiveMake =
   functor (Test : sig
-     val encode : reference -> inductive
+     val encode : qualid -> inductive
      val member_message : Pp.t -> bool -> Pp.t
      val field : string
      val title : string
@@ -501,13 +501,104 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl =
       let eqnl = detype_eqns constructs constagsl bl in
       GCases (tag,pred,[tomatch,(alias,aliastyp)],eqnl)
 
+let rec share_names detype n l avoid env sigma c t =
+  match EConstr.kind sigma c, EConstr.kind sigma t with
+    (* factorize even when not necessary to have better presentation *)
+    | Lambda (na,t,c), Prod (na',t',c') ->
+        let na = match (na,na') with
+            Name _, _ -> na
+          | _, Name _ -> na'
+          | _ -> na in
+        let t' = detype avoid env sigma t in
+        let id = next_name_away na avoid in
+        let avoid = Id.Set.add id avoid and env = add_name (Name id) None t env in
+        share_names detype (n-1) ((Name id,Explicit,None,t')::l) avoid env sigma c c'
+    (* May occur for fix built interactively *)
+    | LetIn (na,b,t',c), _ when n > 0 ->
+        let t'' = detype avoid env sigma t' in
+        let b' = detype avoid env sigma b in
+        let id = next_name_away na avoid in
+        let avoid = Id.Set. add id avoid and env = add_name (Name id) (Some b) t' env in
+        share_names detype n ((Name id,Explicit,Some b',t'')::l) avoid env sigma c (lift 1 t)
+    (* Only if built with the f/n notation or w/o let-expansion in types *)
+    | _, LetIn (_,b,_,t) when n > 0 ->
+        share_names detype n l avoid env sigma c (subst1 b t)
+    (* If it is an open proof: we cheat and eta-expand *)
+    | _, Prod (na',t',c') when n > 0 ->
+        let t'' = detype avoid env sigma t' in
+        let id = next_name_away na' avoid in
+        let avoid = Id.Set.add id avoid and env = add_name (Name id) None t' env in
+        let appc = mkApp (lift 1 c,[|mkRel 1|]) in
+        share_names detype (n-1) ((Name id,Explicit,None,t'')::l) avoid env sigma appc c'
+    (* If built with the f/n notation: we renounce to share names *)
+    | _ ->
+        if n>0 then Feedback.msg_debug (strbrk "Detyping.detype: cannot factorize fix enough");
+        let c = detype avoid env sigma c in
+        let t = detype avoid env sigma t in
+        (List.rev l,c,t)
+
+let rec share_pattern_names detype n l avoid env sigma c t =
+  let open Pattern in
+  if n = 0 then
+    let c = detype avoid env sigma c in
+    let t = detype avoid env sigma t in
+    (List.rev l,c,t)
+  else match c, t with
+    | PLambda (na,t,c), PProd (na',t',c') ->
+        let na = match (na,na') with
+            Name _, _ -> na
+          | _, Name _ -> na'
+          | _ -> na in
+        let t' = detype avoid env sigma t in
+        let id = next_name_away na avoid in
+        let avoid = Id.Set.add id avoid in
+        let env = Name id :: env in
+        share_pattern_names detype (n-1) ((Name id,Explicit,None,t')::l) avoid env sigma c c'
+    | _ ->
+        if n>0 then Feedback.msg_debug (strbrk "Detyping.detype: cannot factorize fix enough");
+        let c = detype avoid env sigma c in
+        let t = detype avoid env sigma t in
+        (List.rev l,c,t)
+
+let detype_fix detype avoid env sigma (vn,_ as nvn) (names,tys,bodies) =
+  let def_avoid, def_env, lfi =
+    Array.fold_left2
+      (fun (avoid, env, l) na ty ->
+         let id = next_name_away na avoid in
+         (Id.Set.add id avoid, add_name (Name id) None ty env, id::l))
+      (avoid, env, []) names tys in
+  let n = Array.length tys in
+  let v = Array.map3
+    (fun c t i -> share_names detype (i+1) [] def_avoid def_env sigma c (lift n t))
+    bodies tys vn in
+  GRec(GFix (Array.map (fun i -> Some i, GStructRec) (fst nvn), snd nvn),Array.of_list (List.rev lfi),
+       Array.map (fun (bl,_,_) -> bl) v,
+       Array.map (fun (_,_,ty) -> ty) v,
+       Array.map (fun (_,bd,_) -> bd) v)
+
+let detype_cofix detype avoid env sigma n (names,tys,bodies) =
+  let def_avoid, def_env, lfi =
+    Array.fold_left2
+      (fun (avoid, env, l) na ty ->
+         let id = next_name_away na avoid in
+         (Id.Set.add id avoid, add_name (Name id) None ty env, id::l))
+      (avoid, env, []) names tys in
+  let ntys = Array.length tys in
+  let v = Array.map2
+    (fun c t -> share_names detype 0 [] def_avoid def_env sigma c (lift ntys t))
+    bodies tys in
+  GRec(GCoFix n,Array.of_list (List.rev lfi),
+       Array.map (fun (bl,_,_) -> bl) v,
+       Array.map (fun (_,_,ty) -> ty) v,
+       Array.map (fun (_,bd,_) -> bd) v)
+
 let detype_universe sigma u =
   let fn (l, n) = Some (Termops.reference_of_level sigma l, n) in
   Univ.Universe.map fn u
 
 let detype_sort sigma = function
-  | Prop Null -> GProp
-  | Prop Pos -> GSet
+  | Prop -> GProp
+  | Set -> GSet
   | Type u ->
     GType
       (if !print_universes
@@ -584,13 +675,12 @@ and detype_r d flags avoid env sigma t =
         (Array.map_to_list (detype d flags avoid env sigma) args)
     | Const (sp,u) -> GRef (ConstRef sp, detype_instance sigma u)
     | Proj (p,c) ->
-      let noparams () = 
-	let pb = Environ.lookup_projection p (snd env) in
-	let pars = pb.Declarations.proj_npars in
-	let hole = DAst.make @@ GHole(Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None) in
-	let args = List.make pars hole in
- 	  GApp (DAst.make @@ GRef (ConstRef (Projection.constant p), None),
-		(args @ [detype d flags avoid env sigma c]))
+      let noparams () =
+        let pars = Projection.npars p in
+        let hole = DAst.make @@ GHole(Evar_kinds.InternalHole,Namegen.IntroAnonymous,None) in
+        let args = List.make pars hole in
+        GApp (DAst.make @@ GRef (ConstRef (Projection.constant p), None),
+              (args @ [detype d flags avoid env sigma c]))
       in
       if fst flags || !Flags.in_debugger || !Flags.in_toplevel then
 	try noparams ()
@@ -603,8 +693,9 @@ and detype_r d flags avoid env sigma t =
 	  (** Print the compatibility match version *)
 	  let c' = 
 	    try 
-	      let pb = Environ.lookup_projection p (snd env) in
-	      let body = pb.Declarations.proj_body in
+              let ind = Projection.inductive p in
+              let bodies = Inductiveops.legacy_match_projection (snd env) ind in
+              let body = bodies.(Projection.arg p) in
 	      let ty = Retyping.get_type_of (snd env) sigma c in
 	      let ((ind,u), args) = Inductiveops.find_mrectype (snd env) sigma ty in
 	      let body' = strip_lam_assum body in
@@ -660,76 +751,8 @@ and detype_r d flags avoid env sigma t =
 	  (ci.ci_ind,ci.ci_pp_info.style,
 	   ci.ci_pp_info.cstr_tags,ci.ci_pp_info.ind_tags)
           p c bl
-    | Fix (nvn,recdef) -> detype_fix d flags avoid env sigma nvn recdef
-    | CoFix (n,recdef) -> detype_cofix d flags avoid env sigma n recdef
-
-and detype_fix d flags avoid env sigma (vn,_ as nvn) (names,tys,bodies) =
-  let def_avoid, def_env, lfi =
-    Array.fold_left2
-      (fun (avoid, env, l) na ty ->
-	 let id = next_name_away na avoid in
-	 (Id.Set.add id avoid, add_name (Name id) None ty env, id::l))
-      (avoid, env, []) names tys in
-  let n = Array.length tys in
-  let v = Array.map3
-    (fun c t i -> share_names d flags (i+1) [] def_avoid def_env sigma c (lift n t))
-    bodies tys vn in
-  GRec(GFix (Array.map (fun i -> Some i, GStructRec) (fst nvn), snd nvn),Array.of_list (List.rev lfi),
-       Array.map (fun (bl,_,_) -> bl) v,
-       Array.map (fun (_,_,ty) -> ty) v,
-       Array.map (fun (_,bd,_) -> bd) v)
-
-and detype_cofix d flags avoid env sigma n (names,tys,bodies) =
-  let def_avoid, def_env, lfi =
-    Array.fold_left2
-      (fun (avoid, env, l) na ty ->
-	 let id = next_name_away na avoid in
-	 (Id.Set.add id avoid, add_name (Name id) None ty env, id::l))
-      (avoid, env, []) names tys in
-  let ntys = Array.length tys in
-  let v = Array.map2
-    (fun c t -> share_names d flags 0 [] def_avoid def_env sigma c (lift ntys t))
-    bodies tys in
-  GRec(GCoFix n,Array.of_list (List.rev lfi),
-       Array.map (fun (bl,_,_) -> bl) v,
-       Array.map (fun (_,_,ty) -> ty) v,
-       Array.map (fun (_,bd,_) -> bd) v)
-
-and share_names d flags n l avoid env sigma c t =
-  match EConstr.kind sigma c, EConstr.kind sigma t with
-    (* factorize even when not necessary to have better presentation *)
-    | Lambda (na,t,c), Prod (na',t',c') ->
-        let na = match (na,na') with
-            Name _, _ -> na
-          | _, Name _ -> na'
-          | _ -> na in
-        let t' = detype d flags avoid env sigma t in
-	let id = next_name_away na avoid in
-        let avoid = Id.Set.add id avoid and env = add_name (Name id) None t env in
-        share_names d flags (n-1) ((Name id,Explicit,None,t')::l) avoid env sigma c c'
-    (* May occur for fix built interactively *)
-    | LetIn (na,b,t',c), _ when n > 0 ->
-        let t'' = detype d flags avoid env sigma t' in
-        let b' = detype d flags avoid env sigma b in
-	let id = next_name_away na avoid in
-        let avoid = Id.Set. add id avoid and env = add_name (Name id) (Some b) t' env in
-        share_names d flags n ((Name id,Explicit,Some b',t'')::l) avoid env sigma c (lift 1 t)
-    (* Only if built with the f/n notation or w/o let-expansion in types *)
-    | _, LetIn (_,b,_,t) when n > 0 ->
-	share_names d flags n l avoid env sigma c (subst1 b t)
-    (* If it is an open proof: we cheat and eta-expand *)
-    | _, Prod (na',t',c') when n > 0 ->
-        let t'' = detype d flags avoid env sigma t' in
-	let id = next_name_away na' avoid in
-        let avoid = Id.Set.add id avoid and env = add_name (Name id) None t' env in
-        let appc = mkApp (lift 1 c,[|mkRel 1|]) in
-        share_names d flags (n-1) ((Name id,Explicit,None,t'')::l) avoid env sigma appc c'
-    (* If built with the f/n notation: we renounce to share names *)
-    | _ ->
-        if n>0 then Feedback.msg_debug (strbrk "Detyping.detype: cannot factorize fix enough");
-        let c = detype d flags avoid env sigma c in
-        let t = detype d flags avoid env sigma t in
-        (List.rev l,c,t)
+    | Fix (nvn,recdef) -> detype_fix (detype d flags) avoid env sigma nvn recdef
+    | CoFix (n,recdef) -> detype_cofix (detype d flags) avoid env sigma n recdef
 
 and detype_eqns d flags avoid env sigma ci computable constructs consnargsl bl =
   try
@@ -902,7 +925,7 @@ let rec subst_cases_pattern subst = DAst.map (function
   | PatVar _ as pat -> pat
   | PatCstr (((kn,i),j),cpl,n) as pat ->
       let kn' = subst_mind subst kn
-      and cpl' = List.smartmap (subst_cases_pattern subst) cpl in
+      and cpl' = List.Smart.map (subst_cases_pattern subst) cpl in
 	if kn' == kn && cpl' == cpl then pat else
 	  PatCstr (((kn',i),j),cpl',n)
   )
@@ -911,9 +934,11 @@ let (f_subst_genarg, subst_genarg_hook) = Hook.make ()
 
 let rec subst_glob_constr subst = DAst.map (function
   | GRef (ref,u) as raw ->
-      let ref',t = subst_global subst ref in
-	if ref' == ref then raw else
-         DAst.get (detype Now false Id.Set.empty (Global.env()) Evd.empty (EConstr.of_constr t))
+    let ref',t = subst_global subst ref in
+    if ref' == ref then raw else
+      let env = Global.env () in
+      let evd = Evd.from_env env in
+      DAst.get (detype Now false Id.Set.empty env evd (EConstr.of_constr t))
 
   | GSort _
   | GVar _
@@ -922,7 +947,7 @@ let rec subst_glob_constr subst = DAst.map (function
 
   | GApp (r,rl) as raw ->
       let r' = subst_glob_constr subst r
-      and rl' = List.smartmap (subst_glob_constr subst) rl in
+      and rl' = List.Smart.map (subst_glob_constr subst) rl in
 	if r' == r && rl' == rl then raw else
 	  GApp(r',rl')
 
@@ -939,25 +964,25 @@ let rec subst_glob_constr subst = DAst.map (function
   | GLetIn (n,r1,t,r2) as raw ->
       let r1' = subst_glob_constr subst r1 in
       let r2' = subst_glob_constr subst r2 in
-      let t' = Option.smartmap (subst_glob_constr subst) t in
+      let t' = Option.Smart.map (subst_glob_constr subst) t in
 	if r1' == r1 && t == t' && r2' == r2 then raw else
 	  GLetIn (n,r1',t',r2')
 
   | GCases (sty,rtno,rl,branches) as raw ->
     let open CAst in
-      let rtno' = Option.smartmap (subst_glob_constr subst) rtno
-      and rl' = List.smartmap (fun (a,x as y) ->
+      let rtno' = Option.Smart.map (subst_glob_constr subst) rtno
+      and rl' = List.Smart.map (fun (a,x as y) ->
         let a' = subst_glob_constr subst a in
         let (n,topt) = x in
-        let topt' = Option.smartmap
+        let topt' = Option.Smart.map
           (fun ({loc;v=((sp,i),y)} as t) ->
             let sp' = subst_mind subst sp in
             if sp == sp' then t else CAst.(make ?loc ((sp',i),y))) topt in
         if a == a' && topt == topt' then y else (a',(n,topt'))) rl
-      and branches' = List.smartmap
+      and branches' = List.Smart.map
                         (fun ({loc;v=(idl,cpl,r)} as branch) ->
 			   let cpl' =
-			     List.smartmap (subst_cases_pattern subst) cpl
+                             List.Smart.map (subst_cases_pattern subst) cpl
 			   and r' = subst_glob_constr subst r in
 			     if cpl' == cpl && r' == r then branch else
                                CAst.(make ?loc (idl,cpl',r')))
@@ -967,14 +992,14 @@ let rec subst_glob_constr subst = DAst.map (function
 	  GCases (sty,rtno',rl',branches')
 
   | GLetTuple (nal,(na,po),b,c) as raw ->
-      let po' = Option.smartmap (subst_glob_constr subst) po
+      let po' = Option.Smart.map (subst_glob_constr subst) po
       and b' = subst_glob_constr subst b
       and c' = subst_glob_constr subst c in
 	if po' == po && b' == b && c' == c then raw else
           GLetTuple (nal,(na,po'),b',c')
 
   | GIf (c,(na,po),b1,b2) as raw ->
-      let po' = Option.smartmap (subst_glob_constr subst) po
+      let po' = Option.Smart.map (subst_glob_constr subst) po
       and b1' = subst_glob_constr subst b1
       and b2' = subst_glob_constr subst b2
       and c' = subst_glob_constr subst c in
@@ -982,12 +1007,12 @@ let rec subst_glob_constr subst = DAst.map (function
           GIf (c',(na,po'),b1',b2')
 
   | GRec (fix,ida,bl,ra1,ra2) as raw ->
-      let ra1' = Array.smartmap (subst_glob_constr subst) ra1
-      and ra2' = Array.smartmap (subst_glob_constr subst) ra2 in
-      let bl' = Array.smartmap
-        (List.smartmap (fun (na,k,obd,ty as dcl) ->
+      let ra1' = Array.Smart.map (subst_glob_constr subst) ra1
+      and ra2' = Array.Smart.map (subst_glob_constr subst) ra2 in
+      let bl' = Array.Smart.map
+        (List.Smart.map (fun (na,k,obd,ty as dcl) ->
           let ty' = subst_glob_constr subst ty in
-          let obd' = Option.smartmap (subst_glob_constr subst) obd in
+          let obd' = Option.Smart.map (subst_glob_constr subst) obd in
           if ty'==ty && obd'==obd then dcl else (na,k,obd',ty')))
         bl in
 	if ra1' == ra1 && ra2' == ra2 && bl'==bl then raw else
@@ -1000,14 +1025,15 @@ let rec subst_glob_constr subst = DAst.map (function
       if nref == ref then knd else Evar_kinds.ImplicitArg (nref, i, b)
     | _ -> knd
     in
-    let nsolve = Option.smartmap (Hook.get f_subst_genarg subst) solve in
+    let nsolve = Option.Smart.map (Hook.get f_subst_genarg subst) solve in
     if nsolve == solve && nknd == knd then raw
     else GHole (nknd, naming, nsolve)
 
   | GCast (r1,k) as raw ->
       let r1' = subst_glob_constr subst r1 in
-      let k' = Miscops.smartmap_cast_type (subst_glob_constr subst) k in
+      let k' = smartmap_cast_type (subst_glob_constr subst) k in
       if r1' == r1 && k' == k then raw else GCast (r1',k')
+
   )
 
 (* Utilities to transform kernel cases to simple pattern-matching problem *)