Efficiently generate the pretyping contexts.

We used to recompute all fresh named contexts for evars before this patch in
the push_rel_context_to_named_context function. This was incurring a linear
penalty and a memory explosion due to the reallocation of many arrays. Now, we
rather remember the context between evar creations by sharing it in the pretyping
environment.

This can be considered as a fix for bug #4964 even though we might do better.

3 files changed, 230 insertions, 125 deletions

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index b63391913..bd86f4bd2 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -290,78 +290,107 @@ let make_pure_subst evi args =
  *   we have the property that u and phi(t) are convertible in env.
  *)
 
+let csubst_subst (k, s) c =
+  let rec subst n c = match Constr.kind c with
+  | Rel m ->
+    if m <= n then c
+    else if m - n <= k then Int.Map.find (k - m + n) s
+    else mkRel (m - k)
+  | _ -> Constr.map_with_binders succ subst n c
+  in
+  if k = 0 then c else subst 0 c
+
 let subst2 subst vsubst c =
-  substl subst (replace_vars vsubst c)
+  csubst_subst subst (replace_vars vsubst c)
 
-let push_rel_context_to_named_context env typ =
-  (* compute the instances relative to the named context and rel_context *)
+let next_ident_away id avoid =
+  let avoid id = Id.Set.mem id avoid in
+  next_ident_away_from id avoid
+
+let next_name_away na avoid =
+  let avoid id = Id.Set.mem id avoid in
+  let id = match na with Name id -> id | Anonymous -> default_non_dependent_ident in
+  next_ident_away_from id avoid
+
+type csubst = int * Constr.t Int.Map.t
+
+let empty_csubst = (0, Int.Map.empty)
+
+type ext_named_context =
+  csubst * (Id.t * Constr.constr) list *
+  Id.Set.t * Context.Named.t
+
+let push_var id (n, s) =
+  let s = Int.Map.add n (mkVar id) s in
+  (succ n, s)
+
+let push_rel_decl_to_named_context decl (subst, vsubst, avoid, nc) =
   let open Context.Named.Declaration in
-  let ids = List.map get_id (named_context env) in
-  let inst_vars = List.map mkVar ids in
-  let inst_rels = List.rev (rel_list 0 (nb_rel env)) in
   let replace_var_named_declaration id0 id decl =
     let id' = get_id decl in
     let id' = if Id.equal id0 id' then id else id' in
     let vsubst = [id0 , mkVar id] in
     decl |> set_id id' |> map_constr (replace_vars vsubst)
   in
-  let replace_var_named_context id0 id  env =
-    let nc = Environ.named_context env in
-    let nc' = List.map (replace_var_named_declaration id0 id) nc in
-    Environ.reset_with_named_context (val_of_named_context nc') env
-  in
   let extract_if_neq id = function
     | Anonymous -> None
     | Name id' when id_ord id id' = 0 -> None
     | Name id' -> Some id'
   in
+  let open Context.Rel.Declaration in
+  let (na, c, t) = to_tuple decl in
+  let open Context.Named.Declaration in
+  let id =
+    (* ppedrot: we want to infer nicer names for the refine tactic, but
+        keeping at the same time backward compatibility in other code
+        using this function. For now, we only attempt to preserve the
+        old behaviour of Program, but ultimately, one should do something
+        about this whole name generation problem. *)
+    if Flags.is_program_mode () then next_name_away na avoid
+    else
+      (** id_of_name_using_hdchar only depends on the rel context which is empty
+          here *)
+      next_ident_away (id_of_name_using_hdchar empty_env t na) avoid
+  in
+  match extract_if_neq id na with
+  | Some id0 when not (is_section_variable id0) ->
+      (* spiwack: if [id<>id0], rather than introducing a new
+          binding named [id], we will keep [id0] (the name given
+          by the user) and rename [id0] into [id] in the named
+          context. Unless [id] is a section variable. *)
+      let subst = (fst subst, Int.Map.map (replace_vars [id0,mkVar id]) (snd subst)) in
+      let vsubst = (id0,mkVar id)::vsubst in
+      let d = match c with
+        | None -> LocalAssum (id0, subst2 subst vsubst t)
+        | Some c -> LocalDef (id0, subst2 subst vsubst c, subst2 subst vsubst t)
+      in
+      let nc = List.map (replace_var_named_declaration id0 id) nc in
+      (push_var id0 subst, vsubst, Id.Set.add id avoid, d :: nc)
+  | _ ->
+      (* spiwack: if [id0] is a section variable renaming it is
+          incorrect. We revert to a less robust behaviour where
+          the new binder has name [id]. Which amounts to the same
+          behaviour than when [id=id0]. *)
+      let d = match c with
+        | None -> LocalAssum (id, subst2 subst vsubst t)
+        | Some c -> LocalDef (id, subst2 subst vsubst c, subst2 subst vsubst t)
+      in
+      (push_var id subst, vsubst, Id.Set.add id avoid, d :: nc)
+
+let push_rel_context_to_named_context env typ =
+  (* compute the instances relative to the named context and rel_context *)
+  let open Context.Named.Declaration in
+  let ids = List.map get_id (named_context env) in
+  let avoid = List.fold_right Id.Set.add ids Id.Set.empty in
+  let inst_vars = List.map mkVar ids in
+  let inst_rels = List.rev (rel_list 0 (nb_rel env)) in
   (* move the rel context to a named context and extend the named instance *)
   (* with vars of the rel context *)
   (* We do keep the instances corresponding to local definition (see above) *)
   let (subst, vsubst, _, env) =
-    Context.Rel.fold_outside
-      (fun decl (subst, vsubst, avoid, env) ->
-        let open Context.Rel.Declaration in
-        let na = get_name decl in
-	let c = get_value decl in
-	let t = get_type decl in
-        let open Context.Named.Declaration in
-        let id =
-          (* ppedrot: we want to infer nicer names for the refine tactic, but
-             keeping at the same time backward compatibility in other code
-             using this function. For now, we only attempt to preserve the
-             old behaviour of Program, but ultimately, one should do something
-             about this whole name generation problem. *)
-          if Flags.is_program_mode () then next_name_away na avoid
-          else next_ident_away (id_of_name_using_hdchar env t na) avoid
-        in
-        match extract_if_neq id na with
-        | Some id0 when not (is_section_variable id0) ->
-            (* spiwack: if [id<>id0], rather than introducing a new
-               binding named [id], we will keep [id0] (the name given
-               by the user) and rename [id0] into [id] in the named
-               context. Unless [id] is a section variable. *)
-            let subst = List.map (replace_vars [id0,mkVar id]) subst in
-            let vsubst = (id0,mkVar id)::vsubst in
-            let d = match c with
-              | None -> LocalAssum (id0, subst2 subst vsubst t)
-              | Some c -> LocalDef (id0, subst2 subst vsubst c, subst2 subst vsubst t)
-            in
-            let env = replace_var_named_context id0  id env in
-            (mkVar id0 :: subst, vsubst, id::avoid, push_named d env)
-        | _ ->
-            (* spiwack: if [id0] is a section variable renaming it is
-               incorrect. We revert to a less robust behaviour where
-               the new binder has name [id]. Which amounts to the same
-               behaviour than when [id=id0]. *)
-            let d = match c with
-              | None -> LocalAssum (id, subst2 subst vsubst t)
-              | Some c -> LocalDef (id, subst2 subst vsubst c, subst2 subst vsubst t)
-            in
-	    (mkVar id :: subst, vsubst, id::avoid, push_named d env)
-      )
-      (rel_context env) ~init:([], [], ids, env) in
-  (named_context_val env, subst2 subst vsubst typ, inst_rels@inst_vars, subst, vsubst)
+    Context.Rel.fold_outside push_rel_decl_to_named_context
+      (rel_context env) ~init:(empty_csubst, [], avoid, named_context env) in
+  (val_of_named_context env, subst2 subst vsubst typ, inst_rels@inst_vars, subst, vsubst)
 
 (*------------------------------------*
  * Entry points to define new evars   *
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 111d0f3e8..c0c81442d 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -199,8 +199,20 @@ val clear_hyps_in_evi : env -> evar_map ref -> named_context_val -> types ->
 val clear_hyps2_in_evi : env -> evar_map ref -> named_context_val -> types -> types ->
   Id.Set.t -> named_context_val * types * types
 
+type csubst
+
+val empty_csubst : csubst
+val csubst_subst : csubst -> Constr.t -> Constr.t
+
+type ext_named_context =
+  csubst * (Id.t * Constr.constr) list *
+  Id.Set.t * Context.Named.t
+
+val push_rel_decl_to_named_context :
+  Context.Rel.Declaration.t -> ext_named_context -> ext_named_context
+
 val push_rel_context_to_named_context : Environ.env -> types ->
-  named_context_val * types * constr list * constr list * (identifier*constr) list
+  named_context_val * types * constr list * csubst * (identifier*constr) list
 
 val generalize_evar_over_rels : evar_map -> existential -> types * constr list
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 187eba16b..1ef96e034 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -68,6 +68,61 @@ open Inductiveops
 
 (************************************************************************)
 
+module ExtraEnv =
+struct
+
+type t = {
+  env : Environ.env;
+  extra : Evarutil.ext_named_context Lazy.t;
+  (** Delay the computation of the evar extended environment *)
+}
+
+let get_extra env =
+  let open Context.Named.Declaration in
+  let ids = List.map get_id (named_context env) in
+  let avoid = List.fold_right Id.Set.add ids Id.Set.empty in
+  Context.Rel.fold_outside push_rel_decl_to_named_context
+    (Environ.rel_context env) ~init:(empty_csubst, [], avoid, named_context env)
+
+let make_env env = { env = env; extra = lazy (get_extra env) }
+let rel_context env = rel_context env.env
+
+let push_rel d env = {
+  env = push_rel d env.env;
+  extra = lazy (push_rel_decl_to_named_context d (Lazy.force env.extra));
+}
+
+let pop_rel_context n env = make_env (pop_rel_context n env.env)
+
+let push_rel_context ctx env = {
+  env = push_rel_context ctx env.env;
+  extra = lazy (List.fold_right push_rel_decl_to_named_context ctx (Lazy.force env.extra));
+}
+
+let lookup_named id env = lookup_named id env.env
+
+let e_new_evar env evdref ?src ?naming typ =
+  let subst2 subst vsubst c = csubst_subst subst (replace_vars vsubst c) in
+  let open Context.Named.Declaration in
+  let inst_vars = List.map (fun d -> mkVar (get_id d)) (named_context env.env) in
+  let inst_rels = List.rev (rel_list 0 (nb_rel env.env)) in
+  let (subst, vsubst, _, nc) = Lazy.force env.extra in
+  let typ' = subst2 subst vsubst typ in
+  let instance = inst_rels @ inst_vars in
+  let sign = val_of_named_context nc in
+  let sigma = Sigma.Unsafe.of_evar_map !evdref in
+  let Sigma (e, sigma, _) = new_evar_instance sign sigma typ' ?src ?naming instance in
+  evdref := Sigma.to_evar_map sigma;
+  e
+
+let push_rec_types (lna,typarray,_) env =
+  let ctxt = Array.map2_i (fun i na t -> Context.Rel.Declaration.LocalAssum (na, lift i t)) lna typarray in
+  Array.fold_left (fun e assum -> push_rel assum e) env ctxt
+
+end
+
+open ExtraEnv
+
 (* An auxiliary function for searching for fixpoint guard indexes *)
 
 exception Found of int array
@@ -302,9 +357,9 @@ let evar_type_fixpoint loc env evdref lna lar vdefj =
   let lt = Array.length vdefj in
     if Int.equal (Array.length lar) lt then
       for i = 0 to lt-1 do
-        if not (e_cumul env evdref (vdefj.(i)).uj_type
+        if not (e_cumul env.ExtraEnv.env evdref (vdefj.(i)).uj_type
 		  (lift lt lar.(i))) then
-          error_ill_typed_rec_body_loc loc env !evdref
+          error_ill_typed_rec_body_loc loc env.ExtraEnv.env !evdref
             i lna vdefj lar
       done
 
@@ -312,7 +367,7 @@ let evar_type_fixpoint loc env evdref lna lar vdefj =
 let inh_conv_coerce_to_tycon resolve_tc loc env evdref j = function
   | None -> j
   | Some t ->
-      evd_comb2 (Coercion.inh_conv_coerce_to resolve_tc loc env) evdref j t
+      evd_comb2 (Coercion.inh_conv_coerce_to resolve_tc loc env.ExtraEnv.env) evdref j t
 
 let check_instance loc subst = function
   | [] -> ()
@@ -361,7 +416,7 @@ let invert_ltac_bound_name lvar env id0 id =
 		       str " which is not bound in current context.")
 
 let protected_get_type_of env sigma c =
-  try Retyping.get_type_of ~lax:true env sigma c
+  try Retyping.get_type_of ~lax:true env.ExtraEnv.env sigma c
   with Retyping.RetypeError _ ->
     errorlabstrm ""
       (str "Cannot reinterpret " ++ quote (print_constr c) ++
@@ -444,7 +499,7 @@ let pretype_global loc rigid env evd gr us =
 		   str " universe instances must be greater or equal to Set.");
 	 evd, Some (Univ.Instance.of_array (Array.of_list (List.rev l')))
   in
-    Evd.fresh_global ~loc ~rigid ?names:instance env evd gr
+    Evd.fresh_global ~loc ~rigid ?names:instance env.ExtraEnv.env evd gr
 
 let pretype_ref loc evdref env ref us =
   match ref with
@@ -459,7 +514,7 @@ let pretype_ref loc evdref env ref us =
   | ref ->
     let evd, c = pretype_global loc univ_flexible env !evdref ref us in
     let () = evdref := evd in
-    let ty = Typing.unsafe_type_of env evd c in
+    let ty = Typing.unsafe_type_of env.ExtraEnv.env evd c in
       make_judge c ty
 
 let judge_of_Type loc evd s =
@@ -477,7 +532,7 @@ let pretype_sort loc evdref = function
 let new_type_evar env evdref loc =
   let sigma = Sigma.Unsafe.of_evar_map !evdref in
   let Sigma ((e, _), sigma, _) =
-    Evarutil.new_type_evar env sigma
+    Evarutil.new_type_evar env.ExtraEnv.env sigma
       univ_flexible_alg ~src:(loc,Evar_kinds.InternalHole)
   in
   evdref := Sigma.to_evar_map sigma;
@@ -489,7 +544,7 @@ let (f_genarg_interp, genarg_interp_hook) = Hook.make ()
 (* in environment [env], with existential variables [evdref] and *)
 (* the type constraint tycon *)
 
-let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var_map) t =
+let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdref (lvar : ltac_var_map) t =
   let inh_conv_coerce_to_tycon = inh_conv_coerce_to_tycon resolve_tc in
   let pretype_type = pretype_type k0 resolve_tc in
   let pretype = pretype k0 resolve_tc in
@@ -515,7 +570,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_
       let hyps = evar_filtered_context (Evd.find !evdref evk) in
       let args = pretype_instance k0 resolve_tc env evdref lvar loc hyps evk inst in
       let c = mkEvar (evk, args) in
-      let j = (Retyping.get_judgment_of env !evdref c) in
+      let j = (Retyping.get_judgment_of env.ExtraEnv.env !evdref c) in
 	inh_conv_coerce_to_tycon loc env evdref j tycon
 
   | GPatVar (loc,(someta,n)) ->
@@ -544,7 +599,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_
         | None ->
           new_type_evar env evdref loc in
       let ist = lvar.ltac_genargs in
-      let (c, sigma) = Hook.get f_genarg_interp ty env !evdref ist arg in
+      let (c, sigma) = Hook.get f_genarg_interp ty env.ExtraEnv.env !evdref ist arg in
       let () = evdref := sigma in
       { uj_val = c; uj_type = ty }
 
@@ -578,7 +633,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_
  	let fixi = match fixkind with
 	  | GFix (vn,i) -> i
 	  | GCoFix i -> i
-	in e_conv env evdref ftys.(fixi) t
+	in e_conv env.ExtraEnv.env evdref ftys.(fixi) t
       | None -> true
     in
       (* Note: bodies are not used by push_rec_types, so [||] is safe *)
@@ -617,12 +672,12 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_
 	  let fixdecls = (names,ftys,fdefs) in
           let indexes =
             search_guard
-              loc env possible_indexes fixdecls
+              loc env.ExtraEnv.env possible_indexes fixdecls
           in
 	    make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i)
 	| GCoFix i ->
 	  let cofix = (i,(names,ftys,fdefs)) in
-            (try check_cofix env cofix
+            (try check_cofix env.ExtraEnv.env cofix
              with reraise ->
                let (e, info) = CErrors.push reraise in
                let info = Loc.add_loc info loc in
@@ -652,7 +707,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_
 	    if Int.equal npars 0 then []
 	    else
 	      try
-	  	let IndType (indf, args) = find_rectype env !evdref ty in
+	  	let IndType (indf, args) = find_rectype env.ExtraEnv.env !evdref ty in
 	  	let ((ind',u'),pars) = dest_ind_family indf in
 	  	  if eq_ind ind ind' then pars
 	  	  else (* Let the usual code throw an error *) []
@@ -661,9 +716,9 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_
     in
     let app_f = 
       match kind_of_term fj.uj_val with
-      | Const (p, u) when Environ.is_projection p env ->
+      | Const (p, u) when Environ.is_projection p env.ExtraEnv.env ->
 	let p = Projection.make p false in
-	let pb = Environ.lookup_projection p env in
+	let pb = Environ.lookup_projection p env.ExtraEnv.env in
 	let npars = pb.Declarations.proj_npars in
 	  fun n -> 
 	    if n == npars + 1 then fun _ v -> mkProj (p, v)
@@ -674,8 +729,8 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_
       | [] -> resj
       | c::rest ->
 	let argloc = loc_of_glob_constr c in
-	let resj = evd_comb1 (Coercion.inh_app_fun resolve_tc env) evdref resj in
-        let resty = whd_all env !evdref resj.uj_type in
+	let resj = evd_comb1 (Coercion.inh_app_fun resolve_tc env.ExtraEnv.env) evdref resj in
+        let resty = whd_all env.ExtraEnv.env !evdref resj.uj_type in
       	  match kind_of_term resty with
 	  | Prod (na,c1,c2) ->
 	    let tycon = Some c1 in
@@ -684,7 +739,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_
 	      match candargs with
 	      | [] -> [], j_val hj
 	      | arg :: args -> 
-		if e_conv env evdref (j_val hj) arg then
+		if e_conv env.ExtraEnv.env evdref (j_val hj) arg then
 		  args, nf_evar !evdref (j_val hj)
 		else [], j_val hj
 	    in
@@ -695,7 +750,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_
 	  | _ ->
 	    let hj = pretype empty_tycon env evdref lvar c in
 	      error_cant_apply_not_functional_loc
-		(Loc.merge floc argloc) env !evdref
+		(Loc.merge floc argloc) env.ExtraEnv.env !evdref
 	      	resj [hj]
     in
     let resj = apply_rec env 1 fj candargs args in
@@ -703,13 +758,13 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_
       match evar_kind_of_term !evdref resj.uj_val with
       | App (f,args) ->
         let f = whd_evar !evdref f in
-          if is_template_polymorphic env f then
+          if is_template_polymorphic env.ExtraEnv.env f then
 	    (* Special case for inductive type applications that must be 
 	       refreshed right away. *)
 	    let sigma = !evdref in
 	    let c = mkApp (f,Array.map (whd_evar sigma) args) in
-	    let c = evd_comb1 (Evarsolve.refresh_universes (Some true) env) evdref c in
-	    let t = Retyping.get_type_of env !evdref c in
+	    let c = evd_comb1 (Evarsolve.refresh_universes (Some true) env.ExtraEnv.env) evdref c in
+	    let t = Retyping.get_type_of env.ExtraEnv.env !evdref c in
 	      make_judge c (* use this for keeping evars: resj.uj_val *) t
 	  else resj
       | _ -> resj 
@@ -722,11 +777,11 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_
 	match tycon with
 	| None -> evd, tycon
 	| Some ty ->
-	  let evd, ty' = Coercion.inh_coerce_to_prod loc env evd ty in
+	  let evd, ty' = Coercion.inh_coerce_to_prod loc env.ExtraEnv.env evd ty in
 	    evd, Some ty')
       evdref tycon
     in
-    let (name',dom,rng) = evd_comb1 (split_tycon loc env) evdref tycon' in
+    let (name',dom,rng) = evd_comb1 (split_tycon loc env.ExtraEnv.env) evdref tycon' in
     let dom_valcon = valcon_of_tycon dom in
     let j = pretype_type dom_valcon env evdref lvar c1 in
     (* The name specified by ltac is used also to create bindings. So
@@ -735,7 +790,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_
     let var = LocalAssum (name, j.utj_val) in
     let j' = pretype rng (push_rel var env) evdref lvar c2 in
     let name = ltac_interp_name lvar name in
-    let resj = judge_of_abstraction env (orelse_name name name') j j' in
+    let resj = judge_of_abstraction env.ExtraEnv.env (orelse_name name name') j j' in
       inh_conv_coerce_to_tycon loc env evdref resj tycon
 
   | GProd(loc,name,bk,c1,c2)        ->
@@ -749,13 +804,13 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_
           { j with utj_val = lift 1 j.utj_val }
       | Name _ ->
         let var = (name,j.utj_val) in
-        let env' = push_rel_assum var env in
+        let env' = ExtraEnv.make_env (push_rel_assum var env.ExtraEnv.env) in
           pretype_type empty_valcon env' evdref lvar c2
     in
     let name = ltac_interp_name lvar name in
     let resj =
       try
-        judge_of_product env name j j'
+        judge_of_product env.ExtraEnv.env name j j'
       with TypeError _ as e ->
         let (e, info) = CErrors.push e in
         let info = Loc.add_loc info loc in
@@ -771,7 +826,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_
       | _ -> pretype empty_tycon env evdref lvar c1
     in
     let t = evd_comb1 (Evarsolve.refresh_universes
-      ~onlyalg:true ~status:Evd.univ_flexible (Some false) env)
+      ~onlyalg:true ~status:Evd.univ_flexible (Some false) env.ExtraEnv.env)
       evdref j.uj_type in
     (* The name specified by ltac is used also to create bindings. So
        the substitution must also be applied on variables before they are
@@ -786,12 +841,12 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_
   | GLetTuple (loc,nal,(na,po),c,d) ->
     let cj = pretype empty_tycon env evdref lvar c in
     let (IndType (indf,realargs)) =
-      try find_rectype env !evdref cj.uj_type
+      try find_rectype env.ExtraEnv.env !evdref cj.uj_type
       with Not_found ->
 	let cloc = loc_of_glob_constr c in
-	  error_case_not_inductive_loc cloc env !evdref cj
+	  error_case_not_inductive_loc cloc env.ExtraEnv.env !evdref cj
     in
-    let cstrs = get_constructors env indf in
+    let cstrs = get_constructors env.ExtraEnv.env indf in
     if not (Int.equal (Array.length cstrs) 1) then
       user_err_loc (loc,"",str "Destructing let is only for inductive types" ++
 	str " with one constructor.");
@@ -800,7 +855,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_
       user_err_loc (loc,"", str "Destructing let on this type expects " ++ 
 	int cs.cs_nargs ++ str " variables.");
     let fsign, record = 
-      match get_projections env indf with
+      match get_projections env.ExtraEnv.env indf with
       | None ->
 	 List.map2 set_name (List.rev nal) cs.cs_args, false
       | Some ps ->
@@ -821,36 +876,36 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_
         let nal = List.rev nal in
         let fsign = List.map2 set_name nal fsign in
 	let f = it_mkLambda_or_LetIn f fsign in
-	let ci = make_case_info env (fst ind) LetStyle in
+	let ci = make_case_info env.ExtraEnv.env (fst ind) LetStyle in
 	  mkCase (ci, p, cj.uj_val,[|f|]) 
       else it_mkLambda_or_LetIn f fsign
     in
     let env_f = push_rel_context fsign env in
       (* Make dependencies from arity signature impossible *)
     let arsgn =
-      let arsgn,_ = get_arity env indf in
+      let arsgn,_ = get_arity env.ExtraEnv.env indf in
 	if not !allow_anonymous_refs then
 	  List.map (set_name Anonymous) arsgn
 	else arsgn
     in
-      let psign = LocalAssum (na, build_dependent_inductive env indf) :: arsgn in
+      let psign = LocalAssum (na, build_dependent_inductive env.ExtraEnv.env indf) :: arsgn in
       let nar = List.length arsgn in
 	  (match po with
 	  | Some p ->
 	    let env_p = push_rel_context psign env in
 	    let pj = pretype_type empty_valcon env_p evdref lvar p in
 	    let ccl = nf_evar !evdref pj.utj_val in
-	    let psign = make_arity_signature env true indf in (* with names *)
+	    let psign = make_arity_signature env.ExtraEnv.env true indf in (* with names *)
 	    let p = it_mkLambda_or_LetIn ccl psign in
 	    let inst =
 	      (Array.to_list cs.cs_concl_realargs)
 	      @[build_dependent_constructor cs] in
 	    let lp = lift cs.cs_nargs p in
-	    let fty = hnf_lam_applist env !evdref lp inst in
+	    let fty = hnf_lam_applist env.ExtraEnv.env !evdref lp inst in
 	    let fj = pretype (mk_tycon fty) env_f evdref lvar d in
 	    let v =
 	      let ind,_ = dest_ind_family indf in
-		Typing.check_allowed_sort env !evdref ind cj.uj_val p;
+		Typing.check_allowed_sort env.ExtraEnv.env !evdref ind cj.uj_val p;
 		obj ind p cj.uj_val fj.uj_val
 	    in
 	      { uj_val = v; uj_type = substl (realargs@[cj.uj_val]) ccl }
@@ -863,37 +918,37 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_
 	      if noccur_between 1 cs.cs_nargs ccl then
 		lift (- cs.cs_nargs) ccl
 	      else
-		error_cant_find_case_type_loc loc env !evdref
+		error_cant_find_case_type_loc loc env.ExtraEnv.env !evdref
 		  cj.uj_val in
 		 (* let ccl = refresh_universes ccl in *)
 	    let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in
 	    let v =
 	      let ind,_ = dest_ind_family indf in
-		Typing.check_allowed_sort env !evdref ind cj.uj_val p;
+		Typing.check_allowed_sort env.ExtraEnv.env !evdref ind cj.uj_val p;
 		obj ind p cj.uj_val fj.uj_val
 	    in { uj_val = v; uj_type = ccl })
 
   | GIf (loc,c,(na,po),b1,b2) ->
     let cj = pretype empty_tycon env evdref lvar c in
     let (IndType (indf,realargs)) =
-      try find_rectype env !evdref cj.uj_type
+      try find_rectype env.ExtraEnv.env !evdref cj.uj_type
       with Not_found ->
 	let cloc = loc_of_glob_constr c in
-	  error_case_not_inductive_loc cloc env !evdref cj in
-    let cstrs = get_constructors env indf in
+	  error_case_not_inductive_loc cloc env.ExtraEnv.env !evdref cj in
+    let cstrs = get_constructors env.ExtraEnv.env indf in
       if not (Int.equal (Array.length cstrs) 2) then
         user_err_loc (loc,"",
 		      str "If is only for inductive types with two constructors.");
 
       let arsgn =
-	let arsgn,_ = get_arity env indf in
+	let arsgn,_ = get_arity env.ExtraEnv.env indf in
 	  if not !allow_anonymous_refs then
 	      (* Make dependencies from arity signature impossible *)
 	    List.map (set_name Anonymous) arsgn
 	  else arsgn
       in
       let nar = List.length arsgn in
-      let psign = LocalAssum (na, build_dependent_inductive env indf) :: arsgn in
+      let psign = LocalAssum (na, build_dependent_inductive env.ExtraEnv.env indf) :: arsgn in
       let pred,p = match po with
 	| Some p ->
 	  let env_p = push_rel_context psign env in
@@ -931,9 +986,9 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_
       let b2 = f cstrs.(1) b2 in
       let v =
 	let ind,_ = dest_ind_family indf in
-	let ci = make_case_info env (fst ind) IfStyle in
+	let ci = make_case_info env.ExtraEnv.env (fst ind) IfStyle in
 	let pred = nf_evar !evdref pred in
-	  Typing.check_allowed_sort env !evdref ind cj.uj_val pred;
+	  Typing.check_allowed_sort env.ExtraEnv.env !evdref ind cj.uj_val pred;
 	  mkCase (ci, pred, cj.uj_val, [|b1;b2|])
       in
       let cj = { uj_val = v; uj_type = p } in
@@ -941,20 +996,20 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_
 
   | GCases (loc,sty,po,tml,eqns) ->
     Cases.compile_cases loc sty
-      ((fun vtyc env evdref -> pretype vtyc env evdref lvar),evdref)
-      tycon env (* loc *) (po,tml,eqns)
+      ((fun vtyc env evdref -> pretype vtyc (make_env env) evdref lvar),evdref)
+      tycon env.ExtraEnv.env (* loc *) (po,tml,eqns)
 
   | GCast (loc,c,k) ->
     let cj =
       match k with
       | CastCoerce ->
 	let cj = pretype empty_tycon env evdref lvar c in
-	  evd_comb1 (Coercion.inh_coerce_to_base loc env) evdref cj
+	  evd_comb1 (Coercion.inh_coerce_to_base loc env.ExtraEnv.env) evdref cj
       | CastConv t | CastVM t | CastNative t ->
 	let k = (match k with CastVM _ -> VMcast | CastNative _ -> NATIVEcast | _ -> DEFAULTcast) in
 	let tj = pretype_type empty_valcon env evdref lvar t in
         let tval = evd_comb1 (Evarsolve.refresh_universes
-                             ~onlyalg:true ~status:Evd.univ_flexible (Some false) env)
+                             ~onlyalg:true ~status:Evd.univ_flexible (Some false) env.ExtraEnv.env)
                           evdref tj.utj_val in
 	let tval = nf_evar !evdref tval in
 	let cj, tval = match k with
@@ -962,22 +1017,22 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_
  	    let cj = pretype empty_tycon env evdref lvar c in
 	    let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tval in
 	      if not (occur_existential cty || occur_existential tval) then
-		let (evd,b) = Reductionops.vm_infer_conv env !evdref cty tval in
+		let (evd,b) = Reductionops.vm_infer_conv env.ExtraEnv.env !evdref cty tval in
 		if b then (evdref := evd; cj, tval)
 		else
-		  error_actual_type_loc loc env !evdref cj tval 
-                      (ConversionFailed (env,cty,tval))
+		  error_actual_type_loc loc env.ExtraEnv.env !evdref cj tval 
+                      (ConversionFailed (env.ExtraEnv.env,cty,tval))
 	      else user_err_loc (loc,"",str "Cannot check cast with vm: " ++
 		str "unresolved arguments remain.")
 	  | NATIVEcast ->
  	    let cj = pretype empty_tycon env evdref lvar c in
 	    let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tval in
             begin
-	      let (evd,b) = Nativenorm.native_infer_conv env !evdref cty tval in
+	      let (evd,b) = Nativenorm.native_infer_conv env.ExtraEnv.env !evdref cty tval in
 	      if b then (evdref := evd; cj, tval)
 	      else
-                error_actual_type_loc loc env !evdref cj tval 
-                  (ConversionFailed (env,cty,tval))
+                error_actual_type_loc loc env.ExtraEnv.env !evdref cj tval 
+                  (ConversionFailed (env.ExtraEnv.env,cty,tval))
             end
 	  | _ -> 
  	    pretype (mk_tycon tval) env evdref lvar c, tval
@@ -998,11 +1053,11 @@ and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update =
       with Not_found ->
       try
         let (n,_,t') = lookup_rel_id id (rel_context env) in
-        if is_conv env !evdref t t' then mkRel n, update else raise Not_found
+        if is_conv env.ExtraEnv.env !evdref t t' then mkRel n, update else raise Not_found
       with Not_found ->
       try
         let t' = lookup_named id env |> get_type in
-        if is_conv env !evdref t t' then mkVar id, update else raise Not_found
+        if is_conv env.ExtraEnv.env !evdref t t' then mkVar id, update else raise Not_found
       with Not_found ->
         user_err_loc (loc,"",str "Cannot interpret " ++
           pr_existential_key !evdref evk ++
@@ -1013,17 +1068,17 @@ and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update =
   Array.map_of_list snd subst
 
 (* [pretype_type valcon env evdref lvar c] coerces [c] into a type *)
-and pretype_type k0 resolve_tc valcon env evdref lvar = function
+and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function
   | GHole (loc, knd, naming, None) ->
       (match valcon with
        | Some v ->
            let s =
 	     let sigma =  !evdref in
-	     let t = Retyping.get_type_of env sigma v in
-	       match kind_of_term (whd_all env sigma t) with
+	     let t = Retyping.get_type_of env.ExtraEnv.env sigma v in
+	       match kind_of_term (whd_all env.ExtraEnv.env sigma t) with
                | Sort s -> s
                | Evar ev when is_Type (existential_type sigma ev) ->
-		   evd_comb1 (define_evar_as_sort env) evdref ev
+		   evd_comb1 (define_evar_as_sort env.ExtraEnv.env) evdref ev
                | _ -> anomaly (Pp.str "Found a type constraint which is not a type")
            in
 	     { utj_val = v;
@@ -1036,16 +1091,17 @@ and pretype_type k0 resolve_tc valcon env evdref lvar = function
   | c ->
       let j = pretype k0 resolve_tc empty_tycon env evdref lvar c in
       let loc = loc_of_glob_constr c in
-      let tj = evd_comb1 (Coercion.inh_coerce_to_sort loc env) evdref j in
+      let tj = evd_comb1 (Coercion.inh_coerce_to_sort loc env.ExtraEnv.env) evdref j in
 	match valcon with
 	| None -> tj
 	| Some v ->
-	    if e_cumul env evdref v tj.utj_val then tj
+	    if e_cumul env.ExtraEnv.env evdref v tj.utj_val then tj
 	    else
 	      error_unexpected_type_loc
-                (loc_of_glob_constr c) env !evdref tj.utj_val v
+                (loc_of_glob_constr c) env.ExtraEnv.env !evdref tj.utj_val v
 
 let ise_pretype_gen flags env sigma lvar kind c =
+  let env = make_env env in
   let evdref = ref sigma in
   let k0 = Context.Rel.length (rel_context env) in
   let c' = match kind with
@@ -1056,7 +1112,7 @@ let ise_pretype_gen flags env sigma lvar kind c =
     | IsType ->
 	(pretype_type k0 flags.use_typeclasses empty_valcon env evdref lvar c).utj_val 
   in
-  process_inference_flags flags env sigma (!evdref,c')
+  process_inference_flags flags env.ExtraEnv.env sigma (!evdref,c')
 
 let default_inference_flags fail = {
   use_typeclasses = true;
@@ -1088,19 +1144,21 @@ let on_judgment f j =
   {uj_val = c; uj_type = t}
 
 let understand_judgment env sigma c =
+  let env = make_env env in
   let evdref = ref sigma in
   let k0 = Context.Rel.length (rel_context env) in
   let j = pretype k0 true empty_tycon env evdref empty_lvar c in
   let j = on_judgment (fun c ->
-    let evd, c = process_inference_flags all_and_fail_flags env sigma (!evdref,c) in 
+    let evd, c = process_inference_flags all_and_fail_flags env.ExtraEnv.env sigma (!evdref,c) in 
       evdref := evd; c) j
   in j, Evd.evar_universe_context !evdref
 
 let understand_judgment_tcc env evdref c =
+  let env = make_env env in
   let k0 = Context.Rel.length (rel_context env) in
   let j = pretype k0 true empty_tycon env evdref empty_lvar c in
   on_judgment (fun c ->
-    let (evd,c) = process_inference_flags all_no_fail_flags env Evd.empty (!evdref,c) in
+    let (evd,c) = process_inference_flags all_no_fail_flags env.ExtraEnv.env Evd.empty (!evdref,c) in
     evdref := evd; c) j
 
 let ise_pretype_gen_ctx flags env sigma lvar kind c =
@@ -1149,3 +1207,9 @@ let type_uconstr ?(flags = constr_flags)
   let (sigma, c) = understand_ltac flags env sigma vars expected_type term in
   Sigma.Unsafe.of_pair (c, sigma)
   end }
+
+let pretype k0 resolve_tc typcon env evdref lvar t =
+  pretype k0 resolve_tc typcon (make_env env) evdref lvar t
+
+let pretype_type k0 resolve_tc valcon env evdref lvar t =
+  pretype_type k0 resolve_tc valcon (make_env env) evdref lvar t