1 files changed, 39 insertions, 40 deletions

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 6f4541e9..657478a1 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -24,6 +24,7 @@ open Declarations
 open Univ
 
 module NamedDecl = Context.Named.Declaration
+module RelDecl = Context.Rel.Declaration
 
 (*s Cooking the constants. *)
 
@@ -126,17 +127,13 @@ let expmod_constr cache modlist c =
 	    | Not_found -> Constr.map substrec c)
 
       | Proj (p, c') ->
-          (try 
-	     let p' = share_univs (ConstRef (Projection.constant p)) Univ.Instance.empty modlist in
-	     let make c = Projection.make c (Projection.unfolded p) in
-	     match kind p' with
-	     | Const (p',_) -> mkProj (make p', substrec c')
-	     | App (f, args) -> 
-	       (match kind f with 
-	       | Const (p', _) -> mkProj (make p', substrec c')
-	       | _ -> assert false)
-	     | _ -> assert false
-	   with Not_found -> Constr.map substrec c)
+        let map cst npars =
+          let _, newpars = Mindmap.find cst (snd modlist) in
+          pop_mind cst, npars + Array.length newpars
+        in
+        let p' = try Projection.map_npars map p with Not_found -> p in
+        let c'' = substrec c' in
+        if p == p' && c' == c'' then c else mkProj (p', c'')
 
   | _ -> Constr.map substrec c
 
@@ -144,11 +141,31 @@ let expmod_constr cache modlist c =
   if is_empty_modlist modlist then c
   else substrec c
 
-let abstract_constant_type =
-   List.fold_left (fun c d -> mkNamedProd_wo_LetIn d c)
+(** Transforms a named context into a rel context. Also returns the list of
+    variables [id1 ... idn] that need to be replaced by [Rel 1 ... Rel n] to
+    abstract a term that lived in that context. *)
+let abstract_context hyps =
+  let fold decl (ctx, subst) =
+    let id, decl = match decl with
+    | NamedDecl.LocalDef (id, b, t) ->
+      let b = Vars.subst_vars subst b in
+      let t = Vars.subst_vars subst t in
+      id, RelDecl.LocalDef (Name id, b, t)
+    | NamedDecl.LocalAssum (id, t) ->
+      let t = Vars.subst_vars subst t in
+      id, RelDecl.LocalAssum (Name id, t)
+    in
+    (decl :: ctx, id :: subst)
+  in
+  Context.Named.fold_outside fold hyps ~init:([], [])
+
+let abstract_constant_type t (hyps, subst) =
+  let t = Vars.subst_vars subst t in
+  List.fold_left (fun c d -> mkProd_wo_LetIn d c) t hyps
 
-let abstract_constant_body =
-  List.fold_left (fun c d -> mkNamedLambda_or_LetIn d c)
+let abstract_constant_body c (hyps, subst) =
+  let c = Vars.subst_vars subst c in
+  it_mkLambda_or_LetIn c hyps
 
 type recipe = { from : constant_body; info : Opaqueproof.cooking_info }
 type inline = bool
@@ -156,10 +173,9 @@ type inline = bool
 type result = {
   cook_body : constant_def;
   cook_type : types;
-  cook_proj : projection_body option;
   cook_universes : constant_universes;
   cook_inline : inline;
-  cook_context : Context.Named.t option;
+  cook_context : Constr.named_context option;
 }
 
 let on_body ml hy f = function
@@ -178,6 +194,7 @@ let cook_constr { Opaqueproof.modlist ; abstract = (vars, subst, _) } c =
   let cache = RefTable.create 13 in
   let expmod = expmod_constr_subst cache modlist subst in
   let hyps = Context.Named.map expmod vars in
+  let hyps = abstract_context hyps in
   abstract_constant_body (expmod c) hyps
 
 let lift_univs cb subst auctx0 =
@@ -206,18 +223,19 @@ let lift_univs cb subst auctx0 =
       let auctx' = Univ.subst_univs_level_abstract_universe_context (Univ.make_instance_subst subst) auctx in
       subst, (Polymorphic_const (AUContext.union auctx0 auctx'))
 
-let cook_constant ~hcons env { from = cb; info } =
+let cook_constant ~hcons { from = cb; info } =
   let { Opaqueproof.modlist; abstract } = info in
   let cache = RefTable.create 13 in
   let abstract, usubst, abs_ctx = abstract in
   let usubst, univs = lift_univs cb usubst abs_ctx in
   let expmod = expmod_constr_subst cache modlist usubst in
-  let hyps = Context.Named.map expmod abstract in
+  let hyps0 = Context.Named.map expmod abstract in
+  let hyps = abstract_context hyps0 in
   let map c =
     let c = abstract_constant_body (expmod c) hyps in
     if hcons then Constr.hcons c else c
   in
-  let body = on_body modlist (hyps, usubst, abs_ctx)
+  let body = on_body modlist (hyps0, usubst, abs_ctx)
     map
     cb.const_body
   in
@@ -225,30 +243,11 @@ let cook_constant ~hcons env { from = cb; info } =
     Context.Named.fold_outside (fun decl hyps ->
       List.filter (fun decl' -> not (Id.equal (NamedDecl.get_id decl) (NamedDecl.get_id decl')))
 		  hyps)
-      hyps ~init:cb.const_hyps in
+      hyps0 ~init:cb.const_hyps in
   let typ = abstract_constant_type (expmod cb.const_type) hyps in
-  let projection pb =
-    let c' = abstract_constant_body (expmod pb.proj_body) hyps in
-    let etab = abstract_constant_body (expmod (fst pb.proj_eta)) hyps in
-    let etat = abstract_constant_body (expmod (snd pb.proj_eta)) hyps in
-    let ((mind, _), _), n' =
-      try 
-	let c' = share_univs cache (IndRef (pb.proj_ind,0)) Univ.Instance.empty modlist in
-	  match kind c' with
-	  | App (f,l) -> (destInd f, Array.length l)
-	  | Ind ind -> ind, 0
-	  | _ -> assert false 
-      with Not_found -> (((pb.proj_ind,0),Univ.Instance.empty), 0)
-    in 
-    let ctx, ty' = decompose_prod_n (n' + pb.proj_npars + 1) typ in
-      { proj_ind = mind; proj_npars = pb.proj_npars + n'; proj_arg = pb.proj_arg;
-	proj_eta = etab, etat;
-	proj_type = ty'; proj_body = c' }
-  in
   {
     cook_body = body;
     cook_type = typ;
-    cook_proj = Option.map projection cb.const_proj;
     cook_universes = univs;
     cook_inline = cb.const_inline_code;
     cook_context = Some const_hyps;