Moving part of pretyping dealing with ltac and renaming in new module GlobEnv.

This module contains:
- the former ExtraEnv in pretyping
- a few functions to traverse binders in pretyping.ml and cases.ml
- the part of pretyping dealing with genarg interpretation

The dependency of pretyping in an interpretation of names as names of
variables of identifier is now hidden in GlobEnv (no more explicit
"lvar" management in pretyping.ml). Similarly for the interpretation
of names as terms and for the interpretation of tactics-in-terms.

We keep empty_lvar in Glob_ops for compatibility, even though it is a
bit isolated there.

1 files changed, 147 insertions, 295 deletions

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 4c3a001186..2d200ad27e 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -38,19 +38,20 @@ open Reductionops
 open Type_errors
 open Typing
 open Globnames
-open Nameops
 open Evarutil
 open Evardefine
 open Pretype_errors
 open Glob_term
 open Glob_ops
+open GlobEnv
 open Evarconv
-open Ltac_pretype
 
 module NamedDecl = Context.Named.Declaration
 
 type typing_constraint = OfType of types | IsType | WithoutTypeConstraint
 
+let (!!) env = GlobEnv.env env
+
 (************************************************************************)
 (* This concerns Cases *)
 open Inductive
@@ -58,58 +59,6 @@ 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 sigma =
-  let avoid = Environ.ids_of_named_context_val (Environ.named_context_val env) in
-  Context.Rel.fold_outside (fun d acc -> push_rel_decl_to_named_context sigma d acc)
-    (rel_context env) ~init:(empty_csubst, avoid, named_context env)
-
-let make_env env sigma = { env = env; extra = lazy (get_extra env sigma) }
-let rel_context env = rel_context env.env
-
-let push_rel sigma d env = {
-  env = push_rel d env.env;
-  extra = lazy (push_rel_decl_to_named_context sigma d (Lazy.force env.extra));
-}
-
-let pop_rel_context n env sigma = make_env (pop_rel_context n env.env) sigma
-
-let push_rel_context sigma ctx env = {
-  env = push_rel_context ctx env.env;
-  extra = lazy (List.fold_right (fun d acc -> push_rel_decl_to_named_context sigma d acc) 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 open Context.Named.Declaration in
-  let inst_vars = List.map (get_id %> mkVar) (named_context env.env) in
-  let inst_rels = List.rev (rel_list 0 (nb_rel env.env)) in
-  let (subst, _, nc) = Lazy.force env.extra in
-  let typ' = csubst_subst subst typ in
-  let instance = inst_rels @ inst_vars in
-  let sign = val_of_named_context nc in
-  let sigma = !evdref in
-  let (sigma, e) = new_evar_instance sign sigma typ' ?src ?naming instance in
-  evdref := sigma;
-  e
-
-let push_rec_types sigma (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 sigma assum e) env ctxt
-
-end
-
-open ExtraEnv
-
 (* An auxiliary function for searching for fixpoint guard indexes *)
 
 exception Found of int array
@@ -400,7 +349,7 @@ let adjust_evar_source evdref na c =
 let inh_conv_coerce_to_tycon ?loc resolve_tc env evdref j = function
   | None -> j
   | Some t ->
-      evd_comb2 (Coercion.inh_conv_coerce_to ?loc resolve_tc env.ExtraEnv.env) evdref j t
+      evd_comb2 (Coercion.inh_conv_coerce_to ?loc resolve_tc !!env) evdref j t
 
 let check_instance loc subst = function
   | [] -> ()
@@ -417,77 +366,21 @@ let orelse_name name name' = match name with
   | Anonymous -> name'
   | _ -> name
 
-(* Rename identifiers of the (initial part of) typing "rel" env *)
-(* according to a name substitution *)
-let ltac_interp_name_env k0 lvar env sigma =
-  (* ctxt is the initial part of the env when pretype was called first *)
-  (* (in practice k0 is probably 0, but we have to grant the
-     specification of pretype which accepts to start with a non empty
-     rel_context) *)
-  let n = Context.Rel.length (rel_context env) - k0 in
-  let ctxt,_ = List.chop n (rel_context env) in
-  let open Context.Rel.Declaration in
-  let ctxt' = List.Smart.map (map_name (ltac_interp_name lvar)) ctxt in
-  if List.equal (fun d1 d2 -> Name.equal (get_name d1) (get_name d2)) ctxt ctxt' then env
-  else push_rel_context sigma ctxt' (pop_rel_context n env sigma)
-
-let invert_ltac_bound_name lvar env id0 id =
-  let id' = Id.Map.find id lvar.ltac_idents in
-  try mkRel (pi1 (lookup_rel_id id' (rel_context env)))
-  with Not_found ->
-    user_err  (str "Ltac variable " ++ Id.print id0 ++
-		       str " depends on pattern variable name " ++ Id.print 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.ExtraEnv.env sigma c
-  with Retyping.RetypeError _ ->
-    user_err 
-      (str "Cannot reinterpret " ++ quote (print_constr c) ++
-       str " in the current environment.")
-
-let pretype_id pretype k0 loc env evdref lvar id =
-  let sigma = !evdref in
+let pretype_id pretype k0 loc env evdref id =
   (* Look for the binder of [id] *)
   try
-    let (n,_,typ) = lookup_rel_id id (rel_context env) in
+    let (n,_,typ) = lookup_rel_id id (rel_context !!env) in
       { uj_val  = mkRel n; uj_type = lift n typ }
   with Not_found ->
-    let env = ltac_interp_name_env k0 lvar env !evdref in
-    (* Check if [id] is an ltac variable *)
-    try
-      let (ids,c) = Id.Map.find id lvar.ltac_constrs in
-      let subst = List.map (invert_ltac_bound_name lvar env id) ids in
-      let c = substl subst c in
-	{ uj_val = c; uj_type = protected_get_type_of env sigma c }
-    with Not_found -> try
-       let {closure;term} = Id.Map.find id lvar.ltac_uconstrs in
-       let lvar = {
-         ltac_constrs = closure.typed;
-         ltac_uconstrs = closure.untyped;
-         ltac_idents = closure.idents;
-         ltac_genargs = Id.Map.empty; }
-       in
-       (* spiwack: I'm catching [Not_found] potentially too eagerly
-          here, as the call to the main pretyping function is caught
-          inside the try but I want to avoid refactoring this function
-          too much for now. *)
-       pretype env evdref lvar term
-    with Not_found ->
-        (* Check if [id] is a ltac variable not bound to a term *)
-	(* and build a nice error message *)
-      if Id.Map.mem id lvar.ltac_genargs then begin
-        let Geninterp.Val.Dyn (typ, _) = Id.Map.find id lvar.ltac_genargs in
-	user_err ?loc 
-         (str "Variable " ++ Id.print id ++ str " should be bound to a term but is \
-          bound to a " ++ Geninterp.Val.pr typ ++ str ".")
-      end;
-      (* Check if [id] is a section or goal variable *)
-      try
-	  { uj_val  = mkVar id; uj_type = NamedDecl.get_type (lookup_named id env) }
-      with Not_found ->
-	  (* [id] not found, standard error message *)
-	  error_var_not_found ?loc id
+  try
+    GlobEnv.interp_ltac_variable ?loc (fun env -> pretype env evdref) env !evdref id
+  with Not_found ->
+  (* Check if [id] is a section or goal variable *)
+  try
+    { uj_val  = mkVar id; uj_type = NamedDecl.get_type (lookup_named id !!env) }
+  with Not_found ->
+    (* [id] not found, standard error message *)
+    error_var_not_found ?loc id
 
 (*************************************************************************)
 (* Main pretyping function                                               *)
@@ -525,18 +418,18 @@ let pretype_global ?loc rigid env evd gr us =
     match us with
     | None -> evd, None
     | Some l -> 
-       let _, ctx = Global.constr_of_global_in_context env.ExtraEnv.env gr in
+       let _, ctx = Global.constr_of_global_in_context !!env gr in
        let len = Univ.AUContext.size ctx in
        interp_instance ?loc evd ~len l
   in
-  let (sigma, c) = Evd.fresh_global ?loc ~rigid ?names:instance env.ExtraEnv.env evd gr in
+  let (sigma, c) = Evd.fresh_global ?loc ~rigid ?names:instance !!env evd gr in
   (sigma, c)
 
 let pretype_ref ?loc evdref env ref us =
   match ref with
   | VarRef id ->
       (* Section variable *)
-      (try make_judge (mkVar id) (NamedDecl.get_type (lookup_named id env))
+      (try make_judge (mkVar id) (NamedDecl.get_type (lookup_named id !!env))
        with Not_found ->
          (* This may happen if env is a goal env and section variables have
             been cleared - section variables should be different from goal
@@ -545,7 +438,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 = unsafe_type_of env.ExtraEnv.env evd c in
+    let ty = unsafe_type_of !!env evd c in
       make_judge c ty
 
 let judge_of_Type ?loc evd s =
@@ -563,29 +456,17 @@ let pretype_sort ?loc evdref = function
 let new_type_evar env evdref loc =
   let sigma = !evdref in
   let (sigma, (e, _)) =
-    Evarutil.new_type_evar env.ExtraEnv.env sigma
+    Evarutil.new_type_evar !!env sigma
       univ_flexible_alg ~src:(loc,Evar_kinds.InternalHole)
   in
   evdref := sigma;
   e
 
-module ConstrInterpObj =
-struct
-  type ('r, 'g, 't) obj =
-    unbound_ltac_var_map -> env -> evar_map -> types -> 'g -> constr * evar_map
-  let name = "constr_interp"
-  let default _ = None
-end
-
-module ConstrInterp = Genarg.Register(ConstrInterpObj)
-
-let register_constr_interp0 = ConstrInterp.register0
-
 (* [pretype tycon env evdref lvar lmeta cstr] attempts to type [cstr] *)
 (* in environment [env], with existential variables [evdref] and *)
 (* the type constraint tycon *)
 
-let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdref (lvar : ltac_var_map) t =
+let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) evdref t =
   let inh_conv_coerce_to_tycon ?loc = inh_conv_coerce_to_tycon ?loc resolve_tc in
   let pretype_type = pretype_type k0 resolve_tc in
   let pretype = pretype k0 resolve_tc in
@@ -599,7 +480,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 
   | GVar id ->
     inh_conv_coerce_to_tycon ?loc env evdref
-      (pretype_id (fun e r l t -> pretype tycon e r l t) k0 loc env evdref lvar id)
+      (pretype_id (fun e r t -> pretype tycon e r t) k0 loc env evdref id)
       tycon
 
   | GEvar (id, inst) ->
@@ -610,13 +491,12 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
         with Not_found ->
           user_err ?loc  (str "Unknown existential variable.") in
       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 args = pretype_instance k0 resolve_tc env evdref loc hyps evk inst in
       let c = mkEvar (evk, args) in
-      let j = (Retyping.get_judgment_of env.ExtraEnv.env !evdref c) in
+      let j = (Retyping.get_judgment_of !!env !evdref c) in
 	inh_conv_coerce_to_tycon ?loc env evdref j tycon
 
   | GPatVar kind ->
-    let env = ltac_interp_name_env k0 lvar env !evdref in
     let ty =
       match tycon with
       | Some ty -> ty
@@ -625,7 +505,6 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
       { uj_val = e_new_evar env evdref ~src:(loc,k) ty; uj_type = ty }
 
   | GHole (k, naming, None) ->
-      let env = ltac_interp_name_env k0 lvar env !evdref in
       let ty =
         match tycon with
         | Some ty -> ty
@@ -634,39 +513,34 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
         { uj_val = e_new_evar env evdref ~src:(loc,k) ~naming ty; uj_type = ty }
 
   | GHole (k, _naming, Some arg) ->
-      let env = ltac_interp_name_env k0 lvar env !evdref in
       let ty =
         match tycon with
         | Some ty -> ty
         | None ->
           new_type_evar env evdref loc in
-      let open Genarg in
-      let ist = lvar.ltac_genargs in
-      let GenArg (Glbwit tag, arg) = arg in
-      let interp = ConstrInterp.obj tag in
-      let (c, sigma) = interp ist env.ExtraEnv.env !evdref ty arg in
+      let (c, sigma) = GlobEnv.interp_glob_genarg env !evdref ty arg in
       let () = evdref := sigma in
       { uj_val = c; uj_type = ty }
 
   | GRec (fixkind,names,bl,lar,vdef) ->
     let rec type_bl env ctxt = function
-    [] -> ctxt
+      | [] -> ctxt
       | (na,bk,None,ty)::bl ->
-        let ty' = pretype_type empty_valcon env evdref lvar ty in
+        let ty' = pretype_type empty_valcon env evdref ty in
 	let dcl = LocalAssum (na, ty'.utj_val) in
-        let dcl' = LocalAssum (ltac_interp_name lvar na,ty'.utj_val) in
-	  type_bl (push_rel !evdref dcl env) (Context.Rel.add dcl' ctxt) bl
+        let dcl', env = push_rel !evdref dcl env in
+        type_bl env (Context.Rel.add dcl' ctxt) bl
       | (na,bk,Some bd,ty)::bl ->
-        let ty' = pretype_type empty_valcon env evdref lvar ty in
-        let bd' = pretype (mk_tycon ty'.utj_val) env evdref lvar bd in
+        let ty' = pretype_type empty_valcon env evdref ty in
+        let bd' = pretype (mk_tycon ty'.utj_val) env evdref bd in
         let dcl = LocalDef (na, bd'.uj_val, ty'.utj_val) in
-        let dcl' = LocalDef (ltac_interp_name lvar na, bd'.uj_val, ty'.utj_val) in
-	  type_bl (push_rel !evdref dcl env) (Context.Rel.add dcl' ctxt) bl in
+        let dcl', env = push_rel !evdref dcl env in
+        type_bl env (Context.Rel.add dcl' ctxt) bl in
     let ctxtv = Array.map (type_bl env Context.Rel.empty) bl in
     let larj =
       Array.map2
         (fun e ar ->
-          pretype_type empty_valcon (push_rel_context !evdref e env) evdref lvar ar)
+          pretype_type empty_valcon (snd (push_rel_context !evdref e env)) evdref ar)
         ctxtv lar in
     let lara = Array.map (fun a -> a.utj_val) larj in
     let ftys = Array.map2 (fun e a -> it_mkProd_or_LetIn a e) ctxtv lara in
@@ -679,14 +553,14 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	  | GFix (vn,i) -> i
 	  | GCoFix i -> i
         in
-        begin match conv env.ExtraEnv.env !evdref ftys.(fixi) t with
+        begin match conv !!env !evdref ftys.(fixi) t with
           | None -> ()
           | Some sigma -> evdref := sigma
         end
       | None -> ()
     in
       (* Note: bodies are not used by push_rec_types, so [||] is safe *)
-    let newenv = push_rec_types !evdref (names,ftys,[||]) env in
+    let _,newenv = push_rec_types !evdref (names,ftys) env in
     let vdefj =
       Array.map2_i
 	(fun i ctxt def ->
@@ -695,12 +569,12 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
           let (ctxt,ty) =
 	    decompose_prod_n_assum !evdref (Context.Rel.length ctxt)
               (lift nbfix ftys.(i)) in
-          let nenv = push_rel_context !evdref ctxt newenv in
-          let j = pretype (mk_tycon ty) nenv evdref lvar def in
+          let ctxt,nenv = push_rel_context !evdref ctxt newenv in
+          let j = pretype (mk_tycon ty) nenv evdref def in
 	    { uj_val = it_mkLambda_or_LetIn j.uj_val ctxt;
 	      uj_type = it_mkProd_or_LetIn j.uj_type ctxt })
         ctxtv vdef in
-      evdref := Typing.check_type_fixpoint ?loc env.ExtraEnv.env !evdref names ftys vdefj;
+      evdref := Typing.check_type_fixpoint ?loc !!env !evdref names ftys vdefj;
       let nf c = nf_evar !evdref c in
       let ftys = Array.map nf ftys in (** FIXME *)
       let fdefs = Array.map (fun x -> nf (j_val x)) vdefj in
@@ -722,13 +596,13 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	  let fixdecls = (names,ftys,fdefs) in
           let indexes =
             search_guard
-              ?loc env.ExtraEnv.env possible_indexes (nf_fix !evdref fixdecls)
+              ?loc !!env possible_indexes (nf_fix !evdref fixdecls)
           in
 	    make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i)
 	| GCoFix i ->
           let fixdecls = (names,ftys,fdefs) in
 	  let cofix = (i, fixdecls) in
-            (try check_cofix env.ExtraEnv.env (i, nf_fix !evdref fixdecls)
+            (try check_cofix !!env (i, nf_fix !evdref fixdecls)
              with reraise ->
                let (e, info) = CErrors.push reraise in
                let info = Option.cata (Loc.add_loc info) info loc in
@@ -743,11 +617,11 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 
   | GProj (p, c) ->
     (* TODO: once GProj is used as an input syntax, use bidirectional typing here *)
-    let cj = pretype empty_tycon env evdref lvar c in
-    judge_of_projection env.ExtraEnv.env !evdref p cj
+    let cj = pretype empty_tycon env evdref c in
+    judge_of_projection !!env !evdref p cj
 
   | GApp (f,args) ->
-    let fj = pretype empty_tycon env evdref lvar f in
+    let fj = pretype empty_tycon env evdref f in
     let floc = loc_of_glob_constr f in
     let length = List.length args in
     let candargs =
@@ -763,7 +637,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	    if Int.equal npars 0 then []
 	    else
 	      try
-	  	let IndType (indf, args) = find_rectype env.ExtraEnv.env !evdref ty in
+                let IndType (indf, args) = find_rectype !!env !evdref ty in
 	  	let ((ind',u'),pars) = dest_ind_family indf in
 	  	  if eq_ind ind ind' then List.map EConstr.of_constr pars
 	  	  else (* Let the usual code throw an error *) []
@@ -785,17 +659,17 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
       | [] -> resj
       | c::rest ->
 	let argloc = loc_of_glob_constr c 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
+        let resj = evd_comb1 (Coercion.inh_app_fun resolve_tc !!env) evdref resj in
+        let resty = whd_all !!env !evdref resj.uj_type in
       	  match EConstr.kind !evdref resty with
 	  | Prod (na,c1,c2) ->
 	    let tycon = Some c1 in
-	    let hj = pretype tycon env evdref lvar c in
+            let hj = pretype tycon env evdref c in
 	    let candargs, ujval =
 	      match candargs with
 	      | [] -> [], j_val hj
 	      | arg :: args -> 
-                begin match conv env.ExtraEnv.env !evdref (j_val hj) arg with
+                begin match conv !!env !evdref (j_val hj) arg with
                   | Some sigma -> evdref := sigma;
                     args, nf_evar !evdref (j_val hj)
                   | None ->
@@ -808,21 +682,21 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	      apply_rec env (n+1) j candargs rest
 		
 	  | _ ->
-	    let hj = pretype empty_tycon env evdref lvar c in
+            let hj = pretype empty_tycon env evdref c in
 	      error_cant_apply_not_functional
-                ?loc:(Loc.merge_opt floc argloc) env.ExtraEnv.env !evdref
+                ?loc:(Loc.merge_opt floc argloc) !!env !evdref
                 resj [|hj|]
     in
     let resj = apply_rec env 1 fj candargs args in
     let resj =
       match EConstr.kind !evdref resj.uj_val with
       | App (f,args) ->
-          if is_template_polymorphic env.ExtraEnv.env !evdref f then
+          if is_template_polymorphic !!env !evdref f then
 	    (* Special case for inductive type applications that must be 
 	       refreshed right away. *)
 	    let c = mkApp (f, args) 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
+            let c = evd_comb1 (Evarsolve.refresh_universes (Some true) !!env) evdref c in
+            let t = Retyping.get_type_of !!env !evdref c in
 	      make_judge c (* use this for keeping evars: resj.uj_val *) t
 	  else resj
       | _ -> resj 
@@ -835,40 +709,34 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	match tycon with
 	| None -> evd, tycon
 	| Some ty ->
-	  let evd, ty' = Coercion.inh_coerce_to_prod ?loc env.ExtraEnv.env evd ty in
+          let evd, ty' = Coercion.inh_coerce_to_prod ?loc !!env evd ty in
 	    evd, Some ty')
       evdref tycon
     in
-    let (name',dom,rng) = evd_comb1 (split_tycon ?loc env.ExtraEnv.env) evdref tycon' in
+    let (name',dom,rng) = evd_comb1 (split_tycon ?loc !!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
-       the substitution must also be applied on variables before they are
-       looked up in the rel context. *)
+    let j = pretype_type dom_valcon env evdref c1 in
     let var = LocalAssum (name, j.utj_val) in
-    let j' = pretype rng (push_rel !evdref var env) evdref lvar c2 in
-    let name = ltac_interp_name lvar name in
-    let resj = judge_of_abstraction env.ExtraEnv.env (orelse_name name name') j j' in
+    let var',env' = push_rel !evdref var env in
+    let j' = pretype rng env' evdref c2 in
+    let name = get_name var' in
+    let resj = judge_of_abstraction !!env (orelse_name name name') j j' in
       inh_conv_coerce_to_tycon ?loc env evdref resj tycon
 
   | GProd(name,bk,c1,c2) ->
-    let j = pretype_type empty_valcon env evdref lvar c1 in
-    (* The name specified by ltac is used also to create bindings. So
-       the substitution must also be applied on variables before they are
-       looked up in the rel context. *)
-    let j' = match name with
+    let j = pretype_type empty_valcon env evdref c1 in
+    let name, j' = match name with
       | Anonymous ->
-        let j = pretype_type empty_valcon env evdref lvar c2 in
-          { j with utj_val = lift 1 j.utj_val }
+        let j = pretype_type empty_valcon env evdref c2 in
+        name, { j with utj_val = lift 1 j.utj_val }
       | Name _ ->
         let var = LocalAssum (name, j.utj_val) in
-        let env' = push_rel !evdref var env in
-          pretype_type empty_valcon env' evdref lvar c2
+        let var, env' = push_rel !evdref var env in
+        get_name var, pretype_type empty_valcon env' evdref c2
     in
-    let name = ltac_interp_name lvar name in
     let resj =
       try
-        judge_of_product env.ExtraEnv.env name j j'
+        judge_of_product !!env name j j'
       with TypeError _ as e ->
         let (e, info) = CErrors.push e in
         let info = Option.cata (Loc.add_loc info) info loc in
@@ -879,33 +747,31 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
     let tycon1 =
       match t with
       | Some t ->
-	 mk_tycon (pretype_type empty_valcon env evdref lvar t).utj_val
+         mk_tycon (pretype_type empty_valcon env evdref t).utj_val
       | None ->
          empty_tycon in
-    let j = pretype tycon1 env evdref lvar c1 in
+    let j = pretype tycon1 env evdref c1 in
     let t = evd_comb1 (Evarsolve.refresh_universes
-      ~onlyalg:true ~status:Evd.univ_flexible (Some false) env.ExtraEnv.env)
+      ~onlyalg:true ~status:Evd.univ_flexible (Some false) !!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
-       looked up in the rel context. *)
     let var = LocalDef (name, j.uj_val, t) in
     let tycon = lift_tycon 1 tycon in
-    let j' = pretype tycon (push_rel !evdref var env) evdref lvar c2 in
-    let name = ltac_interp_name lvar name in
+    let var, env = push_rel !evdref var env in
+    let j' = pretype tycon env evdref c2 in
+    let name = get_name var in
       { uj_val = mkLetIn (name, j.uj_val, t, j'.uj_val) ;
 	uj_type = subst1 j.uj_val j'.uj_type }
 
   | GLetTuple (nal,(na,po),c,d) ->
-    let cj = pretype empty_tycon env evdref lvar c in
+    let cj = pretype empty_tycon env evdref c in
     let (IndType (indf,realargs)) =
-      try find_rectype env.ExtraEnv.env !evdref cj.uj_type
+      try find_rectype !!env !evdref cj.uj_type
       with Not_found ->
 	let cloc = loc_of_glob_constr c in
-	  error_case_not_inductive ?loc:cloc env.ExtraEnv.env !evdref cj
+          error_case_not_inductive ?loc:cloc !!env !evdref cj
     in
     let ind = fst (fst (dest_ind_family indf)) in
-    let cstrs = get_constructors env.ExtraEnv.env indf in
+    let cstrs = get_constructors !!env indf in
     if not (Int.equal (Array.length cstrs) 1) then
       user_err ?loc  (str "Destructing let is only for inductive types" ++
 	str " with one constructor.");
@@ -915,7 +781,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	int cs.cs_nargs ++ str " variables.");
     let fsign, record = 
       let set_name na d = set_name na (map_rel_decl EConstr.of_constr d) in
-      match Environ.get_projections env.ExtraEnv.env ind with
+      match Environ.get_projections !!env ind with
       | None ->
 	 List.map2 set_name (List.rev nal) cs.cs_args, false
       | Some ps ->
@@ -934,108 +800,97 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
     let fsign = if Flags.version_strictly_greater Flags.V8_6
                 then Context.Rel.map (whd_betaiota !evdref) fsign
                 else fsign (* beta-iota-normalization regression in 8.5 and 8.6 *) in
+    let fsign,env_f = push_rel_context !evdref fsign env in
     let obj ind p v f =
-      if not record then 
-        let nal = List.map (fun na -> ltac_interp_name lvar na) nal in
-        let nal = List.rev nal in
-        let fsign = List.map2 set_name nal fsign in
+      if not record then
 	let f = it_mkLambda_or_LetIn f fsign in
-	let ci = make_case_info env.ExtraEnv.env (fst ind) LetStyle in
+        let ci = make_case_info !!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 !evdref fsign env in
-      (* Make dependencies from arity signature impossible *)
+    (* Make dependencies from arity signature impossible *)
     let arsgn =
-      let arsgn,_ = get_arity env.ExtraEnv.env indf in
+      let arsgn,_ = get_arity !!env indf in
       List.map (set_name Anonymous) arsgn
     in
-      let indt = build_dependent_inductive env.ExtraEnv.env indf in
+      let indt = build_dependent_inductive !!env indf in
       let psign = LocalAssum (na, indt) :: arsgn in (* For locating names in [po] *)
-      let predlvar = Cases.make_return_predicate_ltac_lvar !evdref na c cj.uj_val lvar in
-      let psign' = LocalAssum (ltac_interp_name predlvar na, indt) :: arsgn in
-      let psign' = List.map (fun d -> map_rel_decl EConstr.of_constr d) psign' in
-      let psign' = Namegen.name_context env.ExtraEnv.env !evdref psign' in (* For naming abstractions in [po] *)
       let psign = List.map (fun d -> map_rel_decl EConstr.of_constr d) psign in
+      let predenv = Cases.make_return_predicate_ltac_lvar env !evdref na c cj.uj_val in
       let nar = List.length arsgn in
+      let psign',env_p = push_rel_context ~force_names:true !evdref psign predenv in
 	  (match po with
 	  | Some p ->
-	    let env_p = push_rel_context !evdref psign env in
-	    let pj = pretype_type empty_valcon env_p evdref predlvar p in
+            let pj = pretype_type empty_valcon env_p evdref p in
 	    let ccl = nf_evar !evdref pj.utj_val in
 	    let p = it_mkLambda_or_LetIn ccl psign' in
 	    let inst =
 	      (Array.map_to_list EConstr.of_constr cs.cs_concl_realargs)
 	      @[EConstr.of_constr (build_dependent_constructor cs)] in
 	    let lp = lift cs.cs_nargs p 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 fty = hnf_lam_applist !!env !evdref lp inst in
+            let fj = pretype (mk_tycon fty) env_f evdref d in
 	    let v =
 	      let ind,_ = dest_ind_family indf in
-		Typing.check_allowed_sort env.ExtraEnv.env !evdref ind cj.uj_val p;
+                Typing.check_allowed_sort !!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) }
 
 	  | None ->
 	    let tycon = lift_tycon cs.cs_nargs tycon in
-	    let fj = pretype tycon env_f evdref predlvar d in
+            let fj = pretype tycon env_f evdref d in
 	    let ccl = nf_evar !evdref fj.uj_type in
 	    let ccl =
 	      if noccur_between !evdref 1 cs.cs_nargs ccl then
 		lift (- cs.cs_nargs) ccl
 	      else
-		error_cant_find_case_type ?loc env.ExtraEnv.env !evdref
+                error_cant_find_case_type ?loc !!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.ExtraEnv.env !evdref ind cj.uj_val p;
+                Typing.check_allowed_sort !!env !evdref ind cj.uj_val p;
 		obj ind p cj.uj_val fj.uj_val
 	    in { uj_val = v; uj_type = ccl })
 
   | GIf (c,(na,po),b1,b2) ->
-    let cj = pretype empty_tycon env evdref lvar c in
+    let cj = pretype empty_tycon env evdref c in
     let (IndType (indf,realargs)) =
-      try find_rectype env.ExtraEnv.env !evdref cj.uj_type
+      try find_rectype !!env !evdref cj.uj_type
       with Not_found ->
 	let cloc = loc_of_glob_constr c in
-	  error_case_not_inductive ?loc:cloc env.ExtraEnv.env !evdref cj in
-    let cstrs = get_constructors env.ExtraEnv.env indf in
+          error_case_not_inductive ?loc:cloc !!env !evdref cj in
+    let cstrs = get_constructors !!env indf in
       if not (Int.equal (Array.length cstrs) 2) then
         user_err ?loc 
 		      (str "If is only for inductive types with two constructors.");
 
       let arsgn =
-	let arsgn,_ = get_arity env.ExtraEnv.env indf in
+        let arsgn,_ = get_arity !!env indf in
         (* Make dependencies from arity signature impossible *)
         List.map (set_name Anonymous) arsgn
       in
       let nar = List.length arsgn in
-      let indt = build_dependent_inductive env.ExtraEnv.env indf in
+      let indt = build_dependent_inductive !!env indf in
       let psign = LocalAssum (na, indt) :: arsgn in (* For locating names in [po] *)
-      let predlvar = Cases.make_return_predicate_ltac_lvar !evdref na c cj.uj_val lvar in
-      let psign' = LocalAssum (ltac_interp_name predlvar na, indt) :: arsgn in
-      let psign' = List.map (fun d -> map_rel_decl EConstr.of_constr d) psign' in
-      let psign' = Namegen.name_context env.ExtraEnv.env !evdref psign' in (* For naming abstractions in [po] *)
       let psign = List.map (fun d -> map_rel_decl EConstr.of_constr d) psign in
+      let predenv = Cases.make_return_predicate_ltac_lvar env !evdref na c cj.uj_val in
+      let psign,env_p = push_rel_context !evdref psign predenv in
       let pred,p = match po with
 	| Some p ->
-	  let env_p = push_rel_context !evdref psign env in
-	  let pj = pretype_type empty_valcon env_p evdref predlvar p in
+          let pj = pretype_type empty_valcon env_p evdref p in
 	  let ccl = nf_evar !evdref pj.utj_val in
-	  let pred = it_mkLambda_or_LetIn ccl psign' in
+          let pred = it_mkLambda_or_LetIn ccl psign in
 	  let typ = lift (- nar) (beta_applist !evdref (pred,[cj.uj_val])) in
 	    pred, typ
 	| None ->
 	  let p = match tycon with
 	    | Some ty -> ty
-	    | None ->
-              let env = ltac_interp_name_env k0 lvar env !evdref in
-              new_type_evar env evdref loc
+            | None -> new_type_evar env evdref loc
 	  in
-	    it_mkLambda_or_LetIn (lift (nar+1) p) psign', p in
+            it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in
       let pred = nf_evar !evdref pred in
       let p = nf_evar !evdref p in
       let f cs b =
@@ -1050,85 +905,83 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	let csgn =
           List.map (set_name Anonymous) cs_args
         in
-	let env_c = push_rel_context !evdref csgn env in
-	let bj = pretype (mk_tycon pi) env_c evdref lvar b in
+        let _,env_c = push_rel_context !evdref csgn env in
+        let bj = pretype (mk_tycon pi) env_c evdref b in
 	  it_mkLambda_or_LetIn bj.uj_val cs_args in
       let b1 = f cstrs.(0) b1 in
       let b2 = f cstrs.(1) b2 in
       let v =
 	let ind,_ = dest_ind_family indf in
-	let ci = make_case_info env.ExtraEnv.env (fst ind) IfStyle in
+        let ci = make_case_info !!env (fst ind) IfStyle in
 	let pred = nf_evar !evdref pred in
-	  Typing.check_allowed_sort env.ExtraEnv.env !evdref ind cj.uj_val pred;
+          Typing.check_allowed_sort !!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
       inh_conv_coerce_to_tycon ?loc env evdref cj tycon
 
   | GCases (sty,po,tml,eqns) ->
-    Cases.compile_cases ?loc sty
-      ((fun vtyc env evdref -> pretype vtyc (make_env env !evdref) evdref),evdref)
-      tycon env.ExtraEnv.env (* loc *) lvar (po,tml,eqns)
+    Cases.compile_cases ?loc sty (pretype,evdref) tycon env (po,tml,eqns)
 
   | GCast (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.ExtraEnv.env) evdref cj
+        let cj = pretype empty_tycon env evdref c in
+          evd_comb1 (Coercion.inh_coerce_to_base ?loc !!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 tj = pretype_type empty_valcon env evdref t in
         let tval = evd_comb1 (Evarsolve.refresh_universes
-                             ~onlyalg:true ~status:Evd.univ_flexible (Some false) env.ExtraEnv.env)
+                             ~onlyalg:true ~status:Evd.univ_flexible (Some false) !!env)
                           evdref tj.utj_val in
 	let tval = nf_evar !evdref tval in
 	let cj, tval = match k with
 	  | VMcast ->
- 	    let cj = pretype empty_tycon env evdref lvar c in
+            let cj = pretype empty_tycon env evdref c in
 	    let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tval in
 	      if not (occur_existential !evdref cty || occur_existential !evdref tval) then
-                match Reductionops.vm_infer_conv env.ExtraEnv.env !evdref cty tval with
+                match Reductionops.vm_infer_conv !!env !evdref cty tval with
                 | Some evd -> (evdref := evd; cj, tval)
                 | None ->
-		  error_actual_type ?loc env.ExtraEnv.env !evdref cj tval 
-                      (ConversionFailed (env.ExtraEnv.env,cty,tval))
+                  error_actual_type ?loc !!env !evdref cj tval
+                      (ConversionFailed (!!env,cty,tval))
 	      else user_err ?loc  (str "Cannot check cast with vm: " ++
 		str "unresolved arguments remain.")
 	  | NATIVEcast ->
- 	    let cj = pretype empty_tycon env evdref lvar c in
+            let cj = pretype empty_tycon env evdref c in
 	    let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tval in
             begin
-              match Nativenorm.native_infer_conv env.ExtraEnv.env !evdref cty tval with
+              match Nativenorm.native_infer_conv !!env !evdref cty tval with
               | Some evd -> (evdref := evd; cj, tval)
               | None ->
-                error_actual_type ?loc env.ExtraEnv.env !evdref cj tval
-                  (ConversionFailed (env.ExtraEnv.env,cty,tval))
+                error_actual_type ?loc !!env !evdref cj tval
+                  (ConversionFailed (!!env,cty,tval))
             end
 	  | _ -> 
- 	    pretype (mk_tycon tval) env evdref lvar c, tval
+            pretype (mk_tycon tval) env evdref c, tval
 	in
 	let v = mkCast (cj.uj_val, k, tval) in
 	  { uj_val = v; uj_type = tval }
     in inh_conv_coerce_to_tycon ?loc env evdref cj tycon
 
-and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update =
+and pretype_instance k0 resolve_tc env evdref loc hyps evk update =
   let f decl (subst,update) =
     let id = NamedDecl.get_id decl in
     let t = replace_vars subst (NamedDecl.get_type decl) in
     let c, update =
       try
         let c = List.assoc id update in
-        let c = pretype k0 resolve_tc (mk_tycon t) env evdref lvar c in
+        let c = pretype k0 resolve_tc (mk_tycon t) env evdref c in
         c.uj_val, List.remove_assoc id update
       with Not_found ->
       try
-        let (n,_,t') = lookup_rel_id id (rel_context env) in
-        if is_conv env.ExtraEnv.env !evdref t (lift n t') then mkRel n, update else raise Not_found
+        let (n,_,t') = lookup_rel_id id (rel_context !!env) in
+        if is_conv !!env !evdref t (lift n t') then mkRel n, update else raise Not_found
       with Not_found ->
       try
-        let t' = env |> lookup_named id |> NamedDecl.get_type in
-        if is_conv env.ExtraEnv.env !evdref t t' then mkVar id, update else raise Not_found
+        let t' = !!env |> lookup_named id |> NamedDecl.get_type in
+        if is_conv !!env !evdref t t' then mkVar id, update else raise Not_found
       with Not_found ->
         user_err ?loc  (str "Cannot interpret " ++
           pr_existential_key !evdref evk ++
@@ -1138,19 +991,19 @@ and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update =
   check_instance loc subst inst;
   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 : ExtraEnv.t) evdref lvar c = match DAst.get c with
+(* [pretype_type valcon env evdref c] coerces [c] into a type *)
+and pretype_type k0 resolve_tc valcon (env : GlobEnv.t) evdref c = match DAst.get c with
   | GHole (knd, naming, None) ->
       let loc = loc_of_glob_constr c in
       (match valcon with
        | Some v ->
            let s =
 	     let sigma =  !evdref in
-	     let t = Retyping.get_type_of env.ExtraEnv.env sigma v in
-	       match EConstr.kind sigma (whd_all env.ExtraEnv.env sigma t) with
+             let t = Retyping.get_type_of !!env sigma v in
+               match EConstr.kind sigma (whd_all !!env sigma t) with
                | Sort s -> ESorts.kind sigma s
                | Evar ev when is_Type sigma (existential_type sigma ev) ->
-		   evd_comb1 (define_evar_as_sort env.ExtraEnv.env) evdref ev
+                   evd_comb1 (define_evar_as_sort !!env) evdref ev
                | _ -> anomaly (Pp.str "Found a type constraint which is not a type.")
            in
            (* Correction of bug #5315 : we need to define an evar for *all* holes *)
@@ -1161,40 +1014,39 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar c = match D
            { utj_val = v;
 	     utj_type = s }
        | None ->
-           let env = ltac_interp_name_env k0 lvar env !evdref in
 	   let s = evd_comb0 (new_sort_variable univ_flexible_alg) evdref in
 	     { utj_val = e_new_evar env evdref ~src:(loc, knd) ~naming (mkSort s);
 	       utj_type = s})
   | _ ->
-      let j = pretype k0 resolve_tc empty_tycon env evdref lvar c in
+      let j = pretype k0 resolve_tc empty_tycon env evdref c in
       let loc = loc_of_glob_constr c in
-      let tj = evd_comb1 (Coercion.inh_coerce_to_sort ?loc env.ExtraEnv.env) evdref j in
+      let tj = evd_comb1 (Coercion.inh_coerce_to_sort ?loc !!env) evdref j in
 	match valcon with
 	| None -> tj
 	| Some v ->
-          begin match cumul env.ExtraEnv.env !evdref v tj.utj_val with
+          begin match cumul !!env !evdref v tj.utj_val with
             | Some sigma -> evdref := sigma; tj
             | None ->
 	      error_unexpected_type
-                ?loc:(loc_of_glob_constr c) env.ExtraEnv.env !evdref tj.utj_val v
+                ?loc:(loc_of_glob_constr c) !!env !evdref tj.utj_val v
           end
 
 let ise_pretype_gen flags env sigma lvar kind c =
-  let env = make_env env sigma in
+  let env = GlobEnv.make env sigma lvar in
   let evdref = ref sigma in
-  let k0 = Context.Rel.length (rel_context env) in
+  let k0 = Context.Rel.length (rel_context !!env) in
   let c', c'_ty = match kind with
     | WithoutTypeConstraint ->
-        let j = pretype k0 flags.use_typeclasses empty_tycon env evdref lvar c in
+        let j = pretype k0 flags.use_typeclasses empty_tycon env evdref c in
         j.uj_val, j.uj_type
     | OfType exptyp ->
-        let j = pretype k0 flags.use_typeclasses (mk_tycon exptyp) env evdref lvar c in
+        let j = pretype k0 flags.use_typeclasses (mk_tycon exptyp) env evdref c in
         j.uj_val, j.uj_type
     | IsType ->
-        let tj = pretype_type k0 flags.use_typeclasses empty_valcon env evdref lvar c in
+        let tj = pretype_type k0 flags.use_typeclasses empty_valcon env evdref c in
         tj.utj_val, mkSort tj.utj_type
   in
-  process_inference_flags flags env.ExtraEnv.env sigma (!evdref,c',c'_ty)
+  process_inference_flags flags !!env sigma (!evdref,c',c'_ty)
 
 let default_inference_flags fail = {
   use_typeclasses = true;
@@ -1237,7 +1089,7 @@ let understand_ltac flags env sigma lvar kind c =
   (sigma, c)
 
 let pretype k0 resolve_tc typcon env evdref lvar t =
-  pretype k0 resolve_tc typcon (make_env env !evdref) evdref lvar t
+  pretype k0 resolve_tc typcon (GlobEnv.make env !evdref lvar) evdref t
 
 let pretype_type k0 resolve_tc valcon env evdref lvar t =
-  pretype_type k0 resolve_tc valcon (make_env env !evdref) evdref lvar t
+  pretype_type k0 resolve_tc valcon (GlobEnv.make env !evdref lvar) evdref t