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.

11 files changed, 624 insertions, 534 deletions

diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index a0446bd6a0..f4313a8fa3 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -2029,7 +2029,7 @@ let _ =
     let (c, sigma) = Pfedit.refine_by_tactic env sigma ty tac in
     (EConstr.of_constr c, sigma)
   in
-  Pretyping.register_constr_interp0 wit_tactic eval
+  GlobEnv.register_constr_interp0 wit_tactic eval
 
 let vernac_debug b =
   set_debug (if b then Tactic_debug.DebugOn 0 else Tactic_debug.DebugOff)
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index ad33297f0a..120dc61436 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -35,7 +35,7 @@ open Evarsolve
 open Evarconv
 open Evd
 open Context.Rel.Declaration
-open Ltac_pretype
+open GlobEnv
 
 module RelDecl = Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
@@ -114,8 +114,10 @@ let rec relocate_index sigma n1 n2 k t =
 (**********************************************************************)
 (* Structures used in compiling pattern-matching *)
 
+let (!!) env = GlobEnv.env env
+
 type 'a rhs =
-    { rhs_env    : env;
+    { rhs_env    : GlobEnv.t;
       rhs_vars   : Id.Set.t;
       avoid_ids  : Id.Set.t;
       it         : 'a option}
@@ -247,8 +249,7 @@ let push_history_pattern n pci cont =
 *)
 
 type 'a pattern_matching_problem =
-    { env       : env;
-      lvar      : Ltac_pretype.ltac_var_map;
+    { env       : GlobEnv.t;
       evdref    : evar_map ref;
       pred      : constr;
       tomatch   : tomatch_stack;
@@ -256,7 +257,7 @@ type 'a pattern_matching_problem =
       mat       : 'a matrix;
       caseloc   : Loc.t option;
       casestyle : case_style;
-      typing_function: type_constraint -> env -> evar_map ref -> 'a option -> unsafe_judgment }
+      typing_function: type_constraint -> GlobEnv.t -> evar_map ref -> 'a option -> unsafe_judgment }
 
 (*--------------------------------------------------------------------------*
  * A few functions to infer the inductive type from the patterns instead of *
@@ -331,6 +332,10 @@ let binding_vars_of_inductive sigma = function
   | NotInd _ -> []
   | IsInd (_,IndType(_,realargs),_) -> List.filter (isRel sigma) realargs
 
+let set_tomatch_realnames names = function
+  | NotInd _ as t -> t
+  | IsInd (typ,ind,_) -> IsInd (typ,ind,names)
+
 let extract_inductive_data env sigma decl =
   match decl with
   | LocalAssum (_,t) ->
@@ -357,50 +362,45 @@ let find_tomatch_tycon evdref env loc = function
   | None ->
       empty_tycon,None
 
-let make_return_predicate_ltac_lvar sigma na tm c lvar =
+let make_return_predicate_ltac_lvar env sigma na tm c =
+  (* If we have an [x as x return ...] clause and [x] expands to [c],
+     we have to update the status of [x] in the substitution:
+     - if [c] is a variable [id'], then [x] should now become [id']
+     - otherwise, [x] should be hidden *)
   match na, DAst.get tm with
   | Name id, (GVar id' | GRef (Globnames.VarRef id', _)) when Id.equal id id' ->
-     if Id.Map.mem id lvar.ltac_genargs then
-       let ltac_genargs = Id.Map.remove id lvar.ltac_genargs in
-       let ltac_idents = match kind sigma c with
-       | Var id' -> Id.Map.add id id' lvar.ltac_idents
-       | _ -> lvar.ltac_idents in
-       { lvar with ltac_genargs; ltac_idents }
-     else lvar
-  | _ -> lvar
-
-let ltac_interp_realnames lvar = function
-  | t, IsInd (ty,ind,realnal) -> t, IsInd (ty,ind,List.map (ltac_interp_name lvar) realnal)
-  | _ as x -> x
+     let expansion = match kind sigma c with
+       | Var id' -> Name id'
+       | _ -> Anonymous in
+       GlobEnv.hide_variable env expansion id
+  | _ -> env
 
 let is_patvar pat =
   match DAst.get pat with
   | PatVar _ -> true
   | _ -> false
 
-let coerce_row typing_fun evdref env lvar pats (tomatch,(na,indopt)) =
+let coerce_row typing_fun evdref env pats (tomatch,(na,indopt)) =
   let loc = loc_of_glob_constr tomatch in
-  let tycon,realnames = find_tomatch_tycon evdref env loc indopt in
-  let j = typing_fun tycon env evdref !lvar tomatch in
-  let j = evd_comb1 (Coercion.inh_coerce_to_base ?loc:(loc_of_glob_constr tomatch) env) evdref j in
+  let tycon,realnames = find_tomatch_tycon evdref !!env loc indopt in
+  let j = typing_fun tycon env evdref tomatch in
+  let j = evd_comb1 (Coercion.inh_coerce_to_base ?loc:(loc_of_glob_constr tomatch) !!env) evdref j in
   let typ = nf_evar !evdref j.uj_type in
-  lvar := make_return_predicate_ltac_lvar !evdref na tomatch j.uj_val !lvar;
+  let env = make_return_predicate_ltac_lvar env !evdref na tomatch j.uj_val in
   let t =
     if realnames = None && pats <> [] && List.for_all is_patvar pats then NotInd (None,typ) else
-    try try_find_ind env !evdref typ realnames
+    try try_find_ind !!env !evdref typ realnames
     with Not_found ->
-      unify_tomatch_with_patterns evdref env loc typ pats realnames in
-  (j.uj_val,t)
+      unify_tomatch_with_patterns evdref !!env loc typ pats realnames in
+  (env,(j.uj_val,t))
 
-let coerce_to_indtype typing_fun evdref env lvar matx tomatchl =
+let coerce_to_indtype typing_fun evdref env matx tomatchl =
   let pats = List.map (fun r ->  r.patterns) matx in
   let matx' = match matrix_transpose pats with
     | [] -> List.map (fun _ -> []) tomatchl (* no patterns at all *)
     | m -> m in
-  let lvar = ref lvar in
-  let tms = List.map2 (coerce_row typing_fun evdref env lvar) matx' tomatchl in
-  let tms = List.map (ltac_interp_realnames !lvar) tms in
-  !lvar,tms
+  let env,tms = List.fold_left2_map (fun env -> coerce_row typing_fun evdref env) env matx' tomatchl in
+  env,tms
 
 (************************************************************************)
 (* Utils *)
@@ -418,7 +418,7 @@ let adjust_tomatch_to_pattern pb ((current,typ),deps,dep) =
   let typ,names =
     match typ with IsInd(t,_,names) -> t,Some names | NotInd(_,t) -> t,None in
   let tmtyp =
-    try try_find_ind pb.env !(pb.evdref) typ names
+    try try_find_ind !!(pb.env) !(pb.evdref) typ names
     with Not_found -> NotInd (None,typ) in
   match tmtyp with
   | NotInd (None,typ) ->
@@ -426,17 +426,17 @@ let adjust_tomatch_to_pattern pb ((current,typ),deps,dep) =
       (match find_row_ind tm1 with
 	| None -> (current,tmtyp)
 	| Some (_,(ind,_)) ->
-	    let indt = inductive_template pb.evdref pb.env None ind in
+            let indt = inductive_template pb.evdref !!(pb.env) None ind in
 	    let current =
 	      if List.is_empty deps && isEvar !(pb.evdref) typ then
 	      (* Don't insert coercions if dependent; only solve evars *)
-                let () = Option.iter ((:=) pb.evdref) (cumul pb.env !(pb.evdref) indt typ) in
+                let () = Option.iter ((:=) pb.evdref) (cumul !!(pb.env) !(pb.evdref) indt typ) in
 		current
 	      else
-		(evd_comb2 (Coercion.inh_conv_coerce_to true pb.env)
+                (evd_comb2 (Coercion.inh_conv_coerce_to true !!(pb.env))
 		  pb.evdref (make_judge current typ) indt).uj_val in
 	    let sigma =  !(pb.evdref) in
-	    (current,try_find_ind pb.env sigma indt names))
+            (current,try_find_ind !!(pb.env) sigma indt names))
   | _ -> (current,tmtyp)
 
 let type_of_tomatch = function
@@ -466,10 +466,10 @@ let remove_current_pattern eqn =
 	    alias_stack = alias_of_pat pat :: eqn.alias_stack }
     | [] -> anomaly (Pp.str "Empty list of patterns.")
 
-let push_current_pattern (cur,ty) eqn =
+let push_current_pattern sigma (cur,ty) eqn =
   match eqn.patterns with
     | pat::pats ->
-        let rhs_env = push_rel (LocalDef (alias_of_pat pat,cur,ty)) eqn.rhs.rhs_env in
+        let _,rhs_env = push_rel sigma (LocalDef (alias_of_pat pat,cur,ty)) eqn.rhs.rhs_env in
 	{ eqn with
             rhs = { eqn.rhs with rhs_env = rhs_env };
 	    patterns = pats }
@@ -786,31 +786,31 @@ let recover_and_adjust_alias_names names sign =
   in
   List.split (aux (names,sign))
 
-let push_rels_eqn sign eqn =
+let push_rels_eqn sigma sign eqn =
   {eqn with
-     rhs = {eqn.rhs with rhs_env = push_rel_context sign eqn.rhs.rhs_env} }
+     rhs = {eqn.rhs with rhs_env = snd (push_rel_context sigma sign eqn.rhs.rhs_env) } }
 
-let push_rels_eqn_with_names sign eqn =
+let push_rels_eqn_with_names sigma sign eqn =
   let subpats = List.rev (List.firstn (List.length sign) eqn.patterns) in
   let subpatnames = List.map alias_of_pat subpats in
   let sign = recover_initial_subpattern_names subpatnames sign in
-  push_rels_eqn sign eqn
+  push_rels_eqn sigma sign eqn
 
-let push_generalized_decl_eqn env n decl eqn =
+let push_generalized_decl_eqn env sigma n decl eqn =
   match RelDecl.get_name decl with
   | Anonymous ->
-      push_rels_eqn [decl] eqn
+      push_rels_eqn sigma [decl] eqn
   | Name _ ->
-      push_rels_eqn [RelDecl.set_name (RelDecl.get_name (Environ.lookup_rel n eqn.rhs.rhs_env)) decl] eqn
+      push_rels_eqn sigma [RelDecl.set_name (RelDecl.get_name (Environ.lookup_rel n !!(eqn.rhs.rhs_env))) decl] eqn
 
 let drop_alias_eqn eqn =
   { eqn with alias_stack = List.tl eqn.alias_stack }
 
-let push_alias_eqn alias eqn =
+let push_alias_eqn sigma alias eqn =
   let aliasname = List.hd eqn.alias_stack in
   let eqn = drop_alias_eqn eqn in
   let alias = RelDecl.set_name aliasname alias in
-  push_rels_eqn [alias] eqn
+  push_rels_eqn sigma [alias] eqn
 
 (**********************************************************************)
 (* Functions to deal with elimination predicate *)
@@ -958,7 +958,7 @@ let rec extract_predicate ccl = function
       ccl
 
 let abstract_predicate env sigma indf cur realargs (names,na) tms ccl =
-  let sign = make_arity_signature env sigma true indf in
+  let sign = make_arity_signature !!env sigma true indf in
   (* n is the number of real args + 1 (+ possible let-ins in sign) *)
   let n = List.length sign in
   (* Before abstracting we generalize over cur and on those realargs *)
@@ -979,7 +979,7 @@ let abstract_predicate env sigma indf cur realargs (names,na) tms ccl =
   let pred = extract_predicate ccl tms in
   (* Build the predicate properly speaking *)
   let sign = List.map2 set_name (na::names) sign in
-  it_mkLambda_or_LetIn_name env sigma pred sign
+  it_mkLambda_or_LetIn_name !!env sigma pred sign
 
 (* [expand_arg] is used by [specialize_predicate]
    if Yk denotes [Xk;xk] or [Xk],
@@ -1208,7 +1208,7 @@ let first_clause_irrefutable env = function
 
 let group_equations pb ind current cstrs mat =
   let mat =
-    if first_clause_irrefutable pb.env mat then [List.hd mat] else mat in
+    if first_clause_irrefutable !!(pb.env) mat then [List.hd mat] else mat in
   let brs = Array.make (Array.length cstrs) [] in
   let only_default = ref None in
   let _ =
@@ -1216,7 +1216,7 @@ let group_equations pb ind current cstrs mat =
       (fun eqn () ->
 	 let rest = remove_current_pattern eqn in
 	 let pat = current_pattern eqn in
-	 match DAst.get (check_and_adjust_constructor pb.env ind cstrs pat) with
+         match DAst.get (check_and_adjust_constructor !!(pb.env) ind cstrs pat) with
 	   | PatVar name ->
 	       (* This is a default clause that we expand *)
 	       for i=1 to Array.length cstrs do
@@ -1238,7 +1238,7 @@ let rec generalize_problem names pb = function
   | [] -> pb, []
   | i::l ->
       let pb',deps = generalize_problem names pb l in
-      let d = map_constr (lift i) (lookup_rel i pb.env) in
+      let d = map_constr (lift i) (lookup_rel i !!(pb.env)) in
       begin match d with
       | LocalDef (Anonymous,_,_) -> pb', deps
       | _ ->
@@ -1271,7 +1271,7 @@ let build_branch initial current realargs deps (realnames,curname) pb arsign eqn
   (* that had matched constructor C *)
   let cs_args = const_info.cs_args in
   let cs_args = List.map (fun d -> map_rel_decl EConstr.of_constr d) cs_args in
-  let names,aliasname = get_names pb.env !(pb.evdref) cs_args eqns in
+  let names,aliasname = get_names !!(pb.env) !(pb.evdref) cs_args eqns in
   let typs = List.map2 RelDecl.set_name names cs_args
   in
 
@@ -1279,7 +1279,7 @@ let build_branch initial current realargs deps (realnames,curname) pb arsign eqn
   (* This is a bit too strong I think, in the sense that what we would *)
   (* really like is to have beta-iota reduction only at the positions where *)
   (* parameters are substituted *)
-  let typs = List.map (map_type (nf_betaiota pb.env !(pb.evdref))) typs in
+  let typs = List.map (map_type (nf_betaiota !!(pb.env) !(pb.evdref))) typs in
 
   (* We build the matrix obtained by expanding the matching on *)
   (* "C x1..xn as x" followed by a residual matching on eqn into *)
@@ -1291,11 +1291,11 @@ let build_branch initial current realargs deps (realnames,curname) pb arsign eqn
   let typs' =
     List.map_i (fun i d -> (mkRel i, map_constr (lift i) d)) 1 typs in
 
-  let extenv = push_rel_context typs pb.env in
+  let typs,extenv = push_rel_context !(pb.evdref) typs pb.env in
 
   let typs' =
     List.map (fun (c,d) ->
-      (c,extract_inductive_data extenv !(pb.evdref) d,d)) typs' in
+      (c,extract_inductive_data !!extenv !(pb.evdref) d,d)) typs' in
 
   (* We compute over which of x(i+1)..xn and x matching on xi will need a *)
   (* generalization *)
@@ -1360,7 +1360,7 @@ let build_branch initial current realargs deps (realnames,curname) pb arsign eqn
   let submat = adjust_impossible_cases pb pred tomatch submat in
   let () = match submat with
   | [] ->
-    raise_pattern_matching_error (pb.env, Evd.empty, NonExhaustive (complete_history history))
+    raise_pattern_matching_error (!!(pb.env), Evd.empty, NonExhaustive (complete_history history))
   | _ -> ()
   in
 
@@ -1370,7 +1370,7 @@ let build_branch initial current realargs deps (realnames,curname) pb arsign eqn
       tomatch = tomatch;
       pred = pred;
       history = history;
-      mat = List.map (push_rels_eqn_with_names typs) submat }
+      mat = List.map (push_rels_eqn_with_names !(pb.evdref) typs) submat }
 
 (**********************************************************************
  INVARIANT:
@@ -1400,13 +1400,13 @@ and match_current pb (initial,tomatch) =
   let ((current,typ),deps,dep) = tomatch in
   match typ with
     | NotInd (_,typ) ->
-	check_all_variables pb.env !(pb.evdref) typ pb.mat;
+        check_all_variables !!(pb.env) !(pb.evdref) typ pb.mat;
 	compile_all_variables initial tomatch pb
     | IsInd (_,(IndType(indf,realargs) as indt),names) ->
 	let mind,_ = dest_ind_family indf in
-        let mind = Tacred.check_privacy pb.env mind in
-	let cstrs = get_constructors pb.env indf in
-	let arsign, _ = get_arity pb.env indf in
+        let mind = Tacred.check_privacy !!(pb.env) mind in
+        let cstrs = get_constructors !!(pb.env) indf in
+        let arsign, _ = get_arity !!(pb.env) indf in
 	let eqns,onlydflt = group_equations pb (fst mind) current cstrs pb.mat in
         let no_cstr = Int.equal (Array.length cstrs) 0 in
 	if (not no_cstr || not (List.is_empty pb.mat)) && onlydflt then
@@ -1423,18 +1423,17 @@ and match_current pb (initial,tomatch) =
             postprocess_dependencies !(pb.evdref) depstocheck
               brvals pb.tomatch pb.pred deps cstrs in
           let brvals = Array.map (fun (sign,body) ->
-            let sign = List.map (map_name (ltac_interp_name pb.lvar)) sign in
             it_mkLambda_or_LetIn body sign) brvals in
 	  let (pred,typ) =
-	    find_predicate pb.caseloc pb.env pb.evdref
+            find_predicate pb.caseloc pb.env pb.evdref
 	      pred current indt (names,dep) tomatch in
-	  let ci = make_case_info pb.env (fst mind) pb.casestyle in
-          let pred = nf_betaiota pb.env !(pb.evdref) pred in
+          let ci = make_case_info !!(pb.env) (fst mind) pb.casestyle in
+          let pred = nf_betaiota !!(pb.env) !(pb.evdref) pred in
 	  let case =
-            make_case_or_project pb.env !(pb.evdref) indf ci pred current brvals
+            make_case_or_project !!(pb.env) !(pb.evdref) indf ci pred current brvals
 	  in
-          let _ = Evarutil.evd_comb1 (Typing.type_of pb.env) pb.evdref pred in
-	  Typing.check_allowed_sort pb.env !(pb.evdref) mind current pred;
+          let _ = Evarutil.evd_comb1 (Typing.type_of !!(pb.env)) pb.evdref pred in
+          Typing.check_allowed_sort !!(pb.env) !(pb.evdref) mind current pred;
 	  { uj_val = applist (case, inst);
 	    uj_type = prod_applist !(pb.evdref) typ inst }
 
@@ -1444,14 +1443,15 @@ and match_current pb (initial,tomatch) =
 and shift_problem ((current,t),_,na) pb =
   let ty = type_of_tomatch t in
   let tomatch = lift_tomatch_stack 1 pb.tomatch in
-  let pred = specialize_predicate_var (current,t,na) pb.env pb.tomatch pb.pred in
+  let pred = specialize_predicate_var (current,t,na) !!(pb.env) pb.tomatch pb.pred in
+  let env = Name.fold_left (fun env id -> hide_variable env Anonymous id) pb.env na in
   let pb =
     { pb with
-       env = push_rel (LocalDef (na,current,ty)) pb.env;
+       env = snd (push_rel !(pb.evdref) (LocalDef (na,current,ty)) env);
        tomatch = tomatch;
        pred = lift_predicate 1 pred tomatch;
        history = pop_history pb.history;
-       mat = List.map (push_current_pattern (current,ty)) pb.mat } in
+       mat = List.map (push_current_pattern !(pb.evdref) (current,ty)) pb.mat } in
   let j = compile pb in
   { uj_val = subst1 current j.uj_val;
     uj_type = subst1 current j.uj_type }
@@ -1461,7 +1461,7 @@ and shift_problem ((current,t),_,na) pb =
    are already introduced in the context, we avoid creating aliases to
    themselves by treating this case specially. *)
 and pop_problem ((current,t),_,na) pb =
-  let pred = specialize_predicate_var (current,t,na) pb.env pb.tomatch pb.pred in
+  let pred = specialize_predicate_var (current,t,na) !!(pb.env) pb.tomatch pb.pred in
   let pb =
     { pb with
        pred = pred;
@@ -1483,9 +1483,9 @@ and compile_branch initial current realargs names deps pb arsign eqns cstr =
 and compile_generalization pb i d rest =
   let pb =
     { pb with
-       env = push_rel d pb.env;
+       env = snd (push_rel !(pb.evdref) d pb.env);
        tomatch = rest;
-       mat = List.map (push_generalized_decl_eqn pb.env i d) pb.mat } in
+       mat = List.map (push_generalized_decl_eqn pb.env !(pb.evdref) i d) pb.mat } in
   let j = compile pb in
   { uj_val = mkLambda_or_LetIn d j.uj_val;
     uj_type = mkProd_wo_LetIn d j.uj_type }
@@ -1498,11 +1498,11 @@ and compile_alias initial pb (na,orig,(expanded,expanded_typ)) rest =
     let alias = LocalDef (na,c,t) in
     let pb =
       { pb with
-         env = push_rel alias pb.env;
+         env = snd (push_rel !(pb.evdref) alias pb.env);
          tomatch = lift_tomatch_stack 1 rest;
          pred = lift_predicate 1 pb.pred pb.tomatch;
          history = pop_history_pattern pb.history;
-         mat = List.map (push_alias_eqn alias) pb.mat } in
+         mat = List.map (push_alias_eqn !(pb.evdref) alias) pb.mat } in
     let j = compile pb in
     let sigma = !(pb.evdref) in
     { uj_val =
@@ -1534,7 +1534,7 @@ and compile_alias initial pb (na,orig,(expanded,expanded_typ)) rest =
   if not (Flags.is_program_mode ()) && (isRel sigma orig || isVar sigma orig) then
     (* Try to compile first using non expanded alias *)
     try
-      if initial then f orig (Retyping.get_type_of pb.env sigma orig)
+      if initial then f orig (Retyping.get_type_of !!(pb.env) sigma orig)
       else just_pop ()
     with e when precatchable_exception e ->
     (* Try then to compile using expanded alias *)
@@ -1549,7 +1549,7 @@ and compile_alias initial pb (na,orig,(expanded,expanded_typ)) rest =
     (* Could be needed in case of a recursive call which requires to
        be on a variable for size reasons *)
     pb.evdref := sigma;
-    if initial then f orig (Retyping.get_type_of pb.env !(pb.evdref) orig)
+    if initial then f orig (Retyping.get_type_of !!(pb.env) !(pb.evdref) orig)
     else just_pop ()
 
 
@@ -1573,7 +1573,7 @@ substituer après par les initiaux *)
  * Syntactic correctness has already been done in constrintern *)
 let matx_of_eqns env eqns =
   let build_eqn {CAst.loc;v=(ids,initial_lpat,initial_rhs)} =
-    let avoid = ids_of_named_context_val (named_context_val env) in
+    let avoid = ids_of_named_context_val (named_context_val !!env) in
     let avoid = List.fold_left (fun accu id -> Id.Set.add id accu) avoid ids in
     let rhs =
       { rhs_env = env;
@@ -1616,8 +1616,8 @@ let matx_of_eqns env eqns =
 *)
 
 let adjust_to_extended_env_and_remove_deps env extenv sigma subst t =
-  let n = Context.Rel.length (rel_context env) in
-  let n' = Context.Rel.length (rel_context extenv) in
+  let n = Context.Rel.length (rel_context !!env) in
+  let n' = Context.Rel.length (rel_context !!extenv) in
   (* We first remove the bindings that are dependently typed (they are
      difficult to manage and it is not sure these are so useful in practice);
      Notes:
@@ -1630,22 +1630,22 @@ let adjust_to_extended_env_and_remove_deps env extenv sigma subst t =
     (* d1 ... dn dn+1 ... dn'-p+1 ... dn' *)
     (* \--env-/          (= x:ty)         *)
     (* \--------------extenv------------/ *)
-    let (p, _, _) = lookup_rel_id x (rel_context extenv) in
+    let (p, _, _) = lookup_rel_id x (rel_context !!extenv) in
     let rec traverse_local_defs p =
-      match lookup_rel p extenv with
+      match lookup_rel p !!extenv with
       | LocalDef (_,c,_) -> assert (isRel sigma c); traverse_local_defs (p + destRel sigma c)
       | LocalAssum _ -> p in
     let p = traverse_local_defs p in
     let u = lift (n' - n) u in
-    try Some (p, u, expand_vars_in_term extenv sigma u)
+    try Some (p, u, expand_vars_in_term !!extenv sigma u)
       (* pedrot: does this really happen to raise [Failure _]? *)
     with Failure _ -> None in
   let subst0 = List.map_filter map subst in
   let t0 = lift (n' - n) t in
   (subst0, t0)
 
-let push_binder d (k,env,subst) =
-  (k+1,push_rel d env,List.map (fun (na,u,d) -> (na,lift 1 u,d)) subst)
+let push_binder sigma d (k,env,subst) =
+  (k+1,snd (push_rel sigma d env),List.map (fun (na,u,d) -> (na,lift 1 u,d)) subst)
 
 let rec list_assoc_in_triple x = function
     [] -> raise Not_found
@@ -1667,7 +1667,7 @@ let rec list_assoc_in_triple x = function
 *)
 
 let abstract_tycon ?loc env evdref subst tycon extenv t =
-  let t = nf_betaiota env !evdref t in (* it helps in some cases to remove K-redex*)
+  let t = nf_betaiota !!env !evdref t in (* it helps in some cases to remove K-redex*)
   let src = match EConstr.kind !evdref t with
     | Evar (evk,_) -> (Loc.tag ?loc @@ Evar_kinds.SubEvar (None,evk))
     | _ -> (Loc.tag ?loc @@ Evar_kinds.CasesType true) in
@@ -1679,31 +1679,31 @@ let abstract_tycon ?loc env evdref subst tycon extenv t =
      convertible subterms of the substitution *)
   let rec aux (k,env,subst as x) t =
     match EConstr.kind !evdref t with
-    | Rel n when is_local_def (lookup_rel n env) -> t
+    | Rel n when is_local_def (lookup_rel n !!env) -> t
     | Evar ev ->
-        let ty = get_type_of env !evdref t in
-	let ty = Evarutil.evd_comb1 (refresh_universes (Some false) env) evdref ty in
+        let ty = get_type_of !!env !evdref t in
+        let ty = Evarutil.evd_comb1 (refresh_universes (Some false) !!env) evdref ty in
         let inst =
 	  List.map_i
 	    (fun i _ ->
               try list_assoc_in_triple i subst0 with Not_found -> mkRel i)
-              1 (rel_context env) in
-        let ev' = evd_comb1 (Evarutil.new_evar env ~src) evdref ty in
-        begin match solve_simple_eqn (evar_conv_x full_transparent_state) env !evdref (None,ev,substl inst ev') with
+              1 (rel_context !!env) in
+        let ev' = evd_comb1 (Evarutil.new_evar !!env ~src) evdref ty in
+        begin match solve_simple_eqn (evar_conv_x full_transparent_state) !!env !evdref (None,ev,substl inst ev') with
         | Success evd -> evdref := evd
         | UnifFailure _ -> assert false
         end;
         ev'
     | _ ->
-    let good = List.filter (fun (_,u,_) -> is_conv_leq env !evdref t u) subst in
+    let good = List.filter (fun (_,u,_) -> is_conv_leq !!env !evdref t u) subst in
     match good with
     | [] ->
-      map_constr_with_full_binders !evdref push_binder aux x t
+      map_constr_with_full_binders !evdref (push_binder !evdref) aux x t
     | (_, _, u) :: _ -> (* u is in extenv *)
       let vl = List.map pi1 good in
       let ty = 
-	let ty = get_type_of env !evdref t in
-	  Evarutil.evd_comb1 (refresh_universes (Some false) env) evdref ty
+        let ty = get_type_of !!env !evdref t in
+          Evarutil.evd_comb1 (refresh_universes (Some false) !!env) evdref ty
       in
       let dummy_subst = List.init k (fun _ -> mkProp) in
       let ty = substl dummy_subst (aux x ty) in
@@ -1711,7 +1711,7 @@ let abstract_tycon ?loc env evdref subst tycon extenv t =
       let inst =
 	List.map_i
 	  (fun i _ -> if Int.List.mem i vl then u else mkRel i) 1
-	  (rel_context extenv) in
+          (rel_context !!extenv) in
       let map a = match EConstr.kind !evdref a with
       | Rel n -> not (noccurn !evdref n u) || Int.Set.mem n depvl
       | _ -> true
@@ -1719,10 +1719,10 @@ let abstract_tycon ?loc env evdref subst tycon extenv t =
       let rel_filter = List.map map inst in
       let named_filter =
 	List.map (fun d -> local_occur_var !evdref (NamedDecl.get_id d) u)
-	  (named_context extenv) in
+          (named_context !!extenv) in
       let filter = Filter.make (rel_filter @ named_filter) in
       let candidates = u :: List.map mkRel vl in
-      let ev = evd_comb1 (Evarutil.new_evar extenv ~src ~filter ~candidates) evdref ty in
+      let ev = evd_comb1 (Evarutil.new_evar !!extenv ~src ~filter ~candidates) evdref ty in
       lift k ev
   in
   aux (0,extenv,subst0) t0
@@ -1732,19 +1732,19 @@ let build_tycon ?loc env tycon_env s subst tycon extenv evdref t =
     | None ->
 	(* This is the situation we are building a return predicate and
            we are in an impossible branch *)
-	let n = Context.Rel.length (rel_context env) in
-	let n' = Context.Rel.length (rel_context tycon_env) in
+        let n = Context.Rel.length (rel_context !!env) in
+        let n' = Context.Rel.length (rel_context !!tycon_env) in
         let impossible_case_type, u =
           evd_comb1
-            (new_type_evar (reset_context env) ~src:(Loc.tag ?loc Evar_kinds.ImpossibleCase))
+            (new_type_evar (reset_context !!env) ~src:(Loc.tag ?loc Evar_kinds.ImpossibleCase))
             evdref univ_flexible_alg
         in
         (lift (n'-n) impossible_case_type, mkSort u)
     | Some t ->
         let t = abstract_tycon ?loc tycon_env evdref subst tycon extenv t in
-        let tt = evd_comb1 (Typing.type_of extenv) evdref t in
+        let tt = evd_comb1 (Typing.type_of !!extenv) evdref t in
         (t,tt) in
-  match cumul env !evdref tt (mkSort s) with
+  match cumul !!env !evdref tt (mkSort s) with
   | None -> anomaly (Pp.str "Build_tycon: should be a type.");
   | Some sigma -> evdref := sigma;
     { uj_val = t; uj_type = tt }
@@ -1761,14 +1761,14 @@ let build_tycon ?loc env tycon_env s subst tycon extenv evdref t =
 
 let build_inversion_problem loc env sigma tms t =
   let make_patvar t (subst,avoid) =
-    let id = next_name_away (named_hd env sigma t Anonymous) avoid in
+    let id = next_name_away (named_hd !!env sigma t Anonymous) avoid in
     DAst.make @@ PatVar (Name id), ((id,t)::subst, Id.Set.add id avoid) in
   let rec reveal_pattern t (subst,avoid as acc) =
-    match EConstr.kind sigma (whd_all env sigma t) with
+    match EConstr.kind sigma (whd_all !!env sigma t) with
     | Construct (cstr,u) -> DAst.make (PatCstr (cstr,[],Anonymous)), acc
     | App (f,v) when isConstruct sigma f ->
 	let cstr,u = destConstruct sigma f in
-	let n = constructor_nrealargs_env env cstr in
+        let n = constructor_nrealargs_env !!env cstr in
 	let l = List.lastn n (Array.to_list v) in
 	let l,acc = List.fold_right_map reveal_pattern l acc in
 	DAst.make (PatCstr (cstr,l,Anonymous)), acc
@@ -1780,19 +1780,19 @@ let build_inversion_problem loc env sigma tms t =
 	let patl,acc = List.fold_right_map reveal_pattern realargs acc in
 	let pat,acc = make_patvar t acc in
 	let indf' = lift_inductive_family n indf in
-	let sign = make_arity_signature env sigma true indf' in
+        let sign = make_arity_signature !!env sigma true indf' in
         let patl = pat :: List.rev patl in
 	let patl,sign = recover_and_adjust_alias_names patl sign in
 	let p = List.length patl in
-	let env' = push_rel_context sign env in
+        let _,env' = push_rel_context sigma sign env in
 	let patl',acc_sign,acc = aux (n+p) env' (sign@acc_sign) tms acc in
 	List.rev_append patl patl',acc_sign,acc
     | (t, NotInd (bo,typ)) :: tms ->
       let pat,acc = make_patvar t acc in
       let d = LocalAssum (alias_of_pat pat,typ) in
-      let patl,acc_sign,acc = aux (n+1) (push_rel d env) (d::acc_sign) tms acc in
+      let patl,acc_sign,acc = aux (n+1) (snd (push_rel sigma d env)) (d::acc_sign) tms acc in
       pat::patl,acc_sign,acc in
-  let avoid0 = vars_of_env env in
+  let avoid0 = vars_of_env !!env in
   (* [patl] is a list of patterns revealing the substructure of
      constructors present in the constraints on the type of the
      multiple terms t1..tn that are matched in the original problem;
@@ -1808,9 +1808,9 @@ let build_inversion_problem loc env sigma tms t =
   let decls =
     List.map_i (fun i d -> (mkRel i, map_constr (lift i) d)) 1 sign in
 
-  let pb_env = push_rel_context sign env in
+  let _,pb_env = push_rel_context sigma sign env in
   let decls =
-    List.map (fun (c,d) -> (c,extract_inductive_data pb_env sigma d,d)) decls in
+    List.map (fun (c,d) -> (c,extract_inductive_data !!(pb_env) sigma d,d)) decls in
 
   let decls = List.rev decls in
   let dep_sign = find_dependencies_signature sigma (List.make n true) decls in
@@ -1843,7 +1843,7 @@ let build_inversion_problem loc env sigma tms t =
      constraints are incompatible with the constraints on the
      inductive types of the multiple terms matched in Xi *)
   let catch_all_eqn =
-    if List.for_all (irrefutable env) patl then
+    if List.for_all (irrefutable !!env) patl then
       (* No need for a catch all clause *)
       []
     else
@@ -1857,13 +1857,12 @@ let build_inversion_problem loc env sigma tms t =
 	          it = None } } ] in
   (* [pb] is the auxiliary pattern-matching serving as skeleton for the
       return type of the original problem Xi *)
-  let s' = Retyping.get_sort_of env sigma t in
+  let s' = Retyping.get_sort_of !!env sigma t in
   let sigma, s = Evd.new_sort_variable univ_flexible sigma in
-  let sigma = Evd.set_leq_sort env sigma s' s in
+  let sigma = Evd.set_leq_sort !!env sigma s' s in
   let evdref = ref sigma in
   let pb =
     { env       = pb_env;
-      lvar      = empty_lvar;
       evdref    = evdref;
       pred      = (*ty *) mkSort s;
       tomatch   = sub_tms;
@@ -1878,16 +1877,16 @@ let build_inversion_problem loc env sigma tms t =
 (* Here, [pred] is assumed to be in the context built from all *)
 (* realargs and terms to match *)
 let build_initial_predicate arsign pred =
-  let rec buildrec n pred tmnames = function
+  let rec buildrec pred tmnames = function
     | [] -> List.rev tmnames,pred
     | (decl::realdecls)::lnames ->
         let na = RelDecl.get_name decl in
-        let n' = n + List.length realdecls in
-        buildrec (n'+1) pred (force_name na::tmnames) lnames
+        let realnames = List.map RelDecl.get_name realdecls in
+        buildrec pred ((force_name na,realnames)::tmnames) lnames
     | _ -> assert false
-  in buildrec 0 pred [] (List.rev arsign)
+  in buildrec pred [] (List.rev arsign)
 
-let extract_arity_signature ?(dolift=true) env0 lvar tomatchl tmsign =
+let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign =
   let lift = if dolift then lift else fun n t -> t in
   let get_one_sign n tm (na,t) =
     match tm with
@@ -1895,7 +1894,7 @@ let extract_arity_signature ?(dolift=true) env0 lvar tomatchl tmsign =
 	  (match t with
 	    | None -> let sign = match bo with
 		       | None -> [LocalAssum (na, lift n typ)]
-		       | Some b -> [LocalDef (na, lift n b, lift n typ)] in sign,sign
+                       | Some b -> [LocalDef (na, lift n b, lift n typ)] in sign
             | Some {CAst.loc} ->
             user_err ?loc
                 (str"Unexpected type annotation for a term of non inductive type."))
@@ -1905,31 +1904,23 @@ let extract_arity_signature ?(dolift=true) env0 lvar tomatchl tmsign =
 	  let nrealargs_ctxt = inductive_nrealdecls_env env0 ind in
 	  let arsign = fst (get_arity env0 indf') in
 	  let arsign = List.map (fun d -> map_rel_decl EConstr.of_constr d) arsign in
-	  let realnal, realnal' =
+          let realnal =
 	    match t with
               | Some {CAst.loc;v=(ind',realnal)} ->
 		  if not (eq_ind ind ind') then
 		    user_err ?loc  (str "Wrong inductive type.");
 		  if not (Int.equal nrealargs_ctxt (List.length realnal)) then
 		      anomaly (Pp.str "Ill-formed 'in' clause in cases.");
-		  let realnal = List.rev realnal in
-                  let realnal' = List.map (ltac_interp_name lvar) realnal in
-                  realnal,realnal'
+                  List.rev realnal
 	      | None ->
-                  let realnal = List.make nrealargs_ctxt Anonymous in
-                  realnal, realnal in
-          let na' = ltac_interp_name lvar na in
+                  List.make nrealargs_ctxt Anonymous in
           let t = EConstr.of_constr (build_dependent_inductive env0 indf') in
-          (* Context with names for typing *)
-          let arsign1 = LocalAssum (na, t) :: List.map2 RelDecl.set_name realnal arsign in
-          (* Context with names for building the term *)
-          let arsign2 = LocalAssum (na', t) :: List.map2 RelDecl.set_name realnal' arsign in
-          arsign1,arsign2 in
+          LocalAssum (na, t) :: List.map2 RelDecl.set_name realnal arsign in
   let rec buildrec n = function
     | [],[] -> []
     | (_,tm)::ltm, (_,x)::tmsign ->
 	let l = get_one_sign n tm x in
-	l :: buildrec (n + List.length (fst l)) (ltm,tmsign)
+        l :: buildrec (n + List.length l) (ltm,tmsign)
     | _ -> assert false
   in List.rev (buildrec 0 (tomatchl,tmsign))
 
@@ -1986,9 +1977,9 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c =
   in
   assert (len == 0);
   let p = predicate 0 c in
-  let env' = List.fold_right push_rel_context arsign env in
-  try let sigma' = fst (Typing.type_of env' sigma p) in
-        Some (sigma', p)
+  let arsign,env' = List.fold_right_map (push_rel_context sigma) arsign env in
+  try let sigma' = fst (Typing.type_of !!env' sigma p) in
+        Some (sigma', p, arsign)
   with e when precatchable_exception e -> None
 
 (* Builds the predicate. If the predicate is dependent, its context is
@@ -2017,15 +2008,14 @@ let noccur_with_meta sigma n m term =
   in
   try (occur_rec n term; true) with LocalOccur -> false
 
-let prepare_predicate ?loc typing_fun env sigma lvar tomatchs arsign tycon pred =
+let prepare_predicate ?loc typing_fun env sigma tomatchs arsign tycon pred =
   let refresh_tycon sigma t =
     (** If we put the typing constraint in the term, it has to be
        refreshed to preserve the invariant that no algebraic universe
        can appear in the term.  *)
     refresh_universes ~status:Evd.univ_flexible ~onlyalg:true (Some true)
-		      env sigma t
+                      !!env sigma t
   in
-  let typing_arsign,building_arsign = List.split arsign in
   let preds =
     match pred, tycon with
     (* No return clause *)
@@ -2035,12 +2025,12 @@ let prepare_predicate ?loc typing_fun env sigma lvar tomatchs arsign tycon pred
        (* First strategy: we abstract the tycon wrt to the dependencies *)
          let sigma, t = refresh_tycon sigma t in
          let p1 =
-          prepare_predicate_from_arsign_tycon env sigma loc tomatchs typing_arsign t in
+          prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign t in
 	(* Second strategy: we build an "inversion" predicate *)
 	let sigma2,pred2 = build_inversion_problem loc env sigma tomatchs t in
 	(match p1 with
-	 | Some (sigma1,pred1) -> [sigma1, pred1; sigma2, pred2]
-	 | None -> [sigma2, pred2])
+         | Some (sigma1,pred1,arsign) -> [sigma1, pred1, arsign; sigma2, pred2, arsign]
+         | None -> [sigma2, pred2, arsign])
     | None, _ ->
 	(* No dependent type constraint, or no constraints at all: *)
 	(* we use two strategies *)
@@ -2048,28 +2038,28 @@ let prepare_predicate ?loc typing_fun env sigma lvar tomatchs arsign tycon pred
 	| Some t -> refresh_tycon sigma t
 	| None -> 
           let (sigma, (t, _)) =
-	    new_type_evar env sigma univ_flexible_alg ~src:(Loc.tag ?loc @@ Evar_kinds.CasesType false) in
+            new_type_evar !!env sigma univ_flexible_alg ~src:(Loc.tag ?loc @@ Evar_kinds.CasesType false) in
 	    sigma, t
 	in
         (* First strategy: we build an "inversion" predicate *)
 	let sigma1,pred1 = build_inversion_problem loc env sigma tomatchs t in
 	(* Second strategy: we directly use the evar as a non dependent pred *)
-        let pred2 = lift (List.length (List.flatten typing_arsign)) t in
-	[sigma1, pred1; sigma, pred2]
+        let pred2 = lift (List.length (List.flatten arsign)) t in
+        [sigma1, pred1, arsign; sigma, pred2, arsign]
     (* Some type annotation *)
     | Some rtntyp, _ ->
       (* We extract the signature of the arity *)
-      let envar = List.fold_right push_rel_context typing_arsign env in
+      let building_arsign,envar = List.fold_right_map (push_rel_context sigma) arsign env in
       let sigma, newt = new_sort_variable univ_flexible_alg sigma in
       let evdref = ref sigma in
-      let predcclj = typing_fun (mk_tycon (mkSort newt)) envar evdref lvar rtntyp in
+      let predcclj = typing_fun (mk_tycon (mkSort newt)) envar evdref rtntyp in
       let sigma = !evdref in
       let predccl = nf_evar sigma predcclj.uj_val in
-      [sigma, predccl]
+      [sigma, predccl, building_arsign]
   in
   List.map
-    (fun (sigma,pred) ->
-      let (nal,pred) = build_initial_predicate building_arsign pred in
+    (fun (sigma,pred,arsign) ->
+      let (nal,pred) = build_initial_predicate arsign pred in
       sigma,nal,pred)
     preds
 
@@ -2152,7 +2142,7 @@ let constr_of_pat env evdref arsign pat avoid =
 		   typ env (substl args liftt, []) ua avoid
 	       in
 	       let args' = arg' :: List.map (lift n') args in
-	       let env' = push_rel_context sign' env in
+               let env' = EConstr.push_rel_context sign' env in
 		 (pat' :: patargs, args', sign' @ sign, env', n' + n, succ m, avoid))
 	    ci.cs_args (List.rev args) ([], [], [], env, 0, 0, avoid)
 	in
@@ -2172,8 +2162,8 @@ let constr_of_pat env evdref arsign pat avoid =
 		let avoid = Id.Set.add id avoid in
 		let sign, i, avoid =
 		  try
-		    let env = push_rel_context sign env in
-		    evdref := the_conv_x_leq (push_rel_context sign env)
+                    let env = EConstr.push_rel_context sign env in
+                    evdref := the_conv_x_leq (EConstr.push_rel_context sign env)
 		      (lift (succ m) ty) (lift 1 apptype) !evdref;
 		    let eq_t = mk_eq evdref (lift (succ m) ty)
 		      (mkRel 1) (* alias *)
@@ -2240,7 +2230,6 @@ let lift_rel_context n l =
    full signature. However prevpatterns are in the original one signature per pattern form.
  *)
 let build_ineqs evdref prevpatterns pats liftsign =
-  let _tomatchs = List.length pats in
   let diffs =
     List.fold_left
       (fun c eqnpats ->
@@ -2288,7 +2277,7 @@ let constrs_of_pats typing_fun env evdref eqns tomatchs sign neqs arity =
 	 let _, newpatterns, pats =
 	   List.fold_left2
 	     (fun (idents, newpatterns, pats) pat arsign ->
-		let pat', cpat, idents = constr_of_pat env evdref arsign pat idents in
+                let pat', cpat, idents = constr_of_pat !!env evdref arsign pat idents in
 		  (idents, pat' :: newpatterns, cpat :: pats))
 	      (Id.Set.empty, [], []) eqn.patterns sign
 	 in
@@ -2315,7 +2304,7 @@ let constrs_of_pats typing_fun env evdref eqns tomatchs sign neqs arity =
 	 in
 	 let ineqs = build_ineqs evdref prevpatterns pats signlen in
 	 let rhs_rels' = rels_of_patsign !evdref rhs_rels in
-	 let _signenv = push_rel_context rhs_rels' env in
+         let _signenv,_ = push_rel_context !evdref rhs_rels' env in
 	 let arity =
 	   let args, nargs =
 	     List.fold_right (fun (sign, c, (_, args), _) (allargs,n) ->
@@ -2335,11 +2324,11 @@ let constrs_of_pats typing_fun env evdref eqns tomatchs sign neqs arity =
 	   let eqs_rels, arity = decompose_prod_n_assum !evdref neqs arity in
 	     eqs_rels @ neqs_rels @ rhs_rels', arity
 	 in
-	 let rhs_env = push_rel_context rhs_rels' env in
+         let _,rhs_env = push_rel_context !evdref rhs_rels' env in
 	 let j = typing_fun (mk_tycon tycon) rhs_env eqn.rhs.it in
 	 let bbody = it_mkLambda_or_LetIn j.uj_val rhs_rels'
 	 and btype = it_mkProd_or_LetIn j.uj_type rhs_rels' in
-	 let _btype = evd_comb1 (Typing.type_of env) evdref bbody in
+         let _btype = evd_comb1 (Typing.type_of !!env) evdref bbody in
 	 let branch_name = Id.of_string ("program_branch_" ^ (string_of_int !i)) in
 	 let branch_decl = LocalDef (Name branch_name, lift !i bbody, lift !i btype) in
 	 let branch =
@@ -2492,10 +2481,10 @@ let context_of_arsign l =
     l ([], 0)
   in x
 
-let compile_program_cases ?loc style (typing_function, evdref) tycon env lvar
+let compile_program_cases ?loc style (typing_function, evdref) tycon env
     (predopt, tomatchl, eqns) =
   let typing_fun tycon env = function
-    | Some t ->	typing_function tycon env evdref lvar t
+    | Some t ->	typing_function tycon env evdref t
     | None -> Evarutil.evd_comb0 use_unit_judge evdref in
 
   (* We build the matrix of patterns and right-hand side *)
@@ -2503,29 +2492,28 @@ let compile_program_cases ?loc style (typing_function, evdref) tycon env lvar
 
   (* We build the vector of terms to match consistently with the *)
   (* constructors found in patterns *)
-  let predlvar,tomatchs = coerce_to_indtype typing_function evdref env lvar matx tomatchl in
+  let env,tomatchs = coerce_to_indtype typing_function evdref env matx tomatchl in
   let tycon = valcon_of_tycon tycon in
   let tomatchs, tomatchs_lets, tycon' = abstract_tomatch env !evdref tomatchs tycon in
-  let env = push_rel_context tomatchs_lets env in
+  let _,env = push_rel_context !evdref tomatchs_lets env in
   let len = List.length eqns in
   let sign, allnames, signlen, eqs, neqs, args =
     (* The arity signature *)
-    let arsign = extract_arity_signature ~dolift:false env predlvar tomatchs tomatchl in
-    let arsign = List.map fst arsign in (* Because no difference between the arity for typing and the arity for building *)
+    let arsign = extract_arity_signature ~dolift:false !!env tomatchs tomatchl in
       (* Build the dependent arity signature, the equalities which makes
 	 the first part of the predicate and their instantiations. *)
     let avoid = Id.Set.empty in
-      build_dependent_signature env evdref avoid tomatchs arsign
+      build_dependent_signature !!env evdref avoid tomatchs arsign
 
   in
   let tycon, arity =
     let nar = List.fold_left (fun n sign -> List.length sign + n) 0 sign in
     match tycon' with
-    | None -> let ev = mkExistential env evdref in ev, lift nar ev
+    | None -> let ev = mkExistential !!env evdref in ev, lift nar ev
     | Some t ->
 	let pred =
 	  match prepare_predicate_from_arsign_tycon env !evdref loc tomatchs sign t with
-	  | Some (evd, pred) -> evdref := evd; pred
+          | Some (evd, pred, arsign) -> evdref := evd; pred
 	  | None ->
 	       lift nar t
 	in Option.get tycon, pred
@@ -2541,7 +2529,7 @@ let compile_program_cases ?loc style (typing_function, evdref) tycon env lvar
   in
   let matx = List.rev matx in
   let _ = assert (Int.equal len (List.length lets)) in
-  let env = push_rel_context lets env in
+  let _,env = push_rel_context !evdref lets env in
   let matx = List.map (fun eqn -> { eqn with rhs = { eqn.rhs with rhs_env = env } }) matx in
   let tomatchs = List.map (fun (x, y) -> lift len x, lift_tomatch_type len y) tomatchs in
   let args = List.rev_map (lift len) args in
@@ -2554,10 +2542,10 @@ let compile_program_cases ?loc style (typing_function, evdref) tycon env lvar
   let out_tmt na = function NotInd (None,t) -> LocalAssum (na,t)
 			  | NotInd (Some b, t) -> LocalDef (na,b,t)
 			  | IsInd (typ,_,_) -> LocalAssum (na,typ) in
-  let typs = List.map2 (fun na (tm,tmt) -> (tm,out_tmt na tmt)) nal tomatchs in
+  let typs = List.map2 (fun (na,_) (tm,tmt) -> (tm,out_tmt na tmt)) nal tomatchs in
     
   let typs =
-    List.map (fun (c,d) -> (c,extract_inductive_data env !evdref d,d)) typs in
+    List.map (fun (c,d) -> (c,extract_inductive_data !!env !evdref d,d)) typs in
     
   let dep_sign =
     find_dependencies_signature !evdref
@@ -2566,20 +2554,20 @@ let compile_program_cases ?loc style (typing_function, evdref) tycon env lvar
     
   let typs' =
     List.map3
-      (fun (tm,tmt) deps na ->
+      (fun (tm,tmt) deps (na,realnames) ->
          let deps = if not (isRel !evdref tm) then [] else deps in
+          let tmt = set_tomatch_realnames realnames tmt in
            ((tm,tmt),deps,na))
       tomatchs dep_sign nal in
     
   let initial_pushed = List.map (fun x -> Pushed (true,x)) typs' in
     
   let typing_function tycon env evdref = function
-    | Some t ->	typing_function tycon env evdref lvar t
+    | Some t ->	typing_function tycon env evdref t
     | None -> evd_comb0 use_unit_judge evdref in
 
   let pb =
     { env      = env;
-      lvar     = lvar;
       evdref   = evdref;
       pred     = pred;
       tomatch  = initial_pushed;
@@ -2591,7 +2579,7 @@ let compile_program_cases ?loc style (typing_function, evdref) tycon env lvar
 
   let j = compile pb in
     (* We check for unused patterns *)
-    List.iter (check_unused_pattern env) matx;
+    List.iter (check_unused_pattern !!env) matx;
     let body = it_mkLambda_or_LetIn (applist (j.uj_val, args)) lets in
     let j =
       { uj_val = it_mkLambda_or_LetIn body tomatchs_lets;
@@ -2602,10 +2590,10 @@ let compile_program_cases ?loc style (typing_function, evdref) tycon env lvar
 (**************************************************************************)
 (* Main entry of the matching compilation                                 *)
 
-let compile_cases ?loc style (typing_fun, evdref) tycon env lvar (predopt, tomatchl, eqns) =
+let compile_cases ?loc style (typing_fun, evdref) tycon env (predopt, tomatchl, eqns) =
   if predopt == None && Flags.is_program_mode () && Program.is_program_cases () then
     compile_program_cases ?loc style (typing_fun, evdref)
-      tycon env lvar (predopt, tomatchl, eqns)
+      tycon env (predopt, tomatchl, eqns)
   else
 
   (* We build the matrix of patterns and right-hand side *)
@@ -2613,15 +2601,13 @@ let compile_cases ?loc style (typing_fun, evdref) tycon env lvar (predopt, tomat
 
   (* We build the vector of terms to match consistently with the *)
   (* constructors found in patterns *)
-  let predlvar,tomatchs = coerce_to_indtype typing_fun evdref env lvar matx tomatchl in
-
-
+  let predenv,tomatchs = coerce_to_indtype typing_fun evdref env matx tomatchl in
 
   (* If an elimination predicate is provided, we check it is compatible
      with the type of arguments to match; if none is provided, we
      build alternative possible predicates *)
-  let arsign = extract_arity_signature env predlvar tomatchs tomatchl in
-  let preds = prepare_predicate ?loc typing_fun env !evdref predlvar tomatchs arsign tycon predopt in
+  let arsign = extract_arity_signature !!env tomatchs tomatchl in
+  let preds = prepare_predicate ?loc typing_fun predenv !evdref tomatchs arsign tycon predopt in
 
   let compile_for_one_predicate (sigma,nal,pred) =
     (* We push the initial terms to match and push their alias to rhs' envs *)
@@ -2631,10 +2617,10 @@ let compile_cases ?loc style (typing_fun, evdref) tycon env lvar (predopt, tomat
     let out_tmt na = function NotInd (None,t) -> LocalAssum (na,t)
 			    | NotInd (Some b,t) -> LocalDef (na,b,t)
 			    | IsInd (typ,_,_) -> LocalAssum (na,typ) in
-    let typs = List.map2 (fun na (tm,tmt) -> (tm,out_tmt na tmt)) nal tomatchs in
+    let typs = List.map2 (fun (na,_) (tm,tmt) -> (tm,out_tmt na tmt)) nal tomatchs in
 
     let typs =
-      List.map (fun (c,d) -> (c,extract_inductive_data env sigma d,d)) typs in
+      List.map (fun (c,d) -> (c,extract_inductive_data !!env sigma d,d)) typs in
 
     let dep_sign =
       find_dependencies_signature !evdref
@@ -2643,8 +2629,9 @@ let compile_cases ?loc style (typing_fun, evdref) tycon env lvar (predopt, tomat
 
     let typs' =
       List.map3
-        (fun (tm,tmt) deps na ->
+        (fun (tm,tmt) deps (na,realnames) ->
           let deps = if not (isRel !evdref tm) then [] else deps in
+          let tmt = set_tomatch_realnames realnames tmt in
           ((tm,tmt),deps,na))
         tomatchs dep_sign nal in
 
@@ -2652,14 +2639,13 @@ let compile_cases ?loc style (typing_fun, evdref) tycon env lvar (predopt, tomat
 
     (* A typing function that provides with a canonical term for absurd cases*)
     let typing_fun tycon env evdref = function
-    | Some t ->	typing_fun tycon env evdref lvar t
+    | Some t ->	typing_fun tycon env evdref t
     | None -> evd_comb0 use_unit_judge evdref in
 
     let myevdref = ref sigma in
 
     let pb =
       { env       = env;
-        lvar      = lvar;
         evdref    = myevdref;
 	pred      = pred;
 	tomatch   = initial_pushed;
@@ -2672,7 +2658,7 @@ let compile_cases ?loc style (typing_fun, evdref) tycon env lvar (predopt, tomat
     let j = compile pb in
 
     (* We coerce to the tycon (if an elim predicate was provided) *)
-    let j = inh_conv_coerce_to_tycon ?loc env myevdref j tycon in
+    let j = inh_conv_coerce_to_tycon ?loc !!env myevdref j tycon in
     evdref := !myevdref;
     j in
 
@@ -2681,6 +2667,6 @@ let compile_cases ?loc style (typing_fun, evdref) tycon env lvar (predopt, tomat
   let j = list_try_compile compile_for_one_predicate preds in
 
   (* We check for unused patterns *)
-  List.iter (check_unused_pattern env) matx;
+  List.iter (check_unused_pattern !!env) matx;
 
   j
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index 04a3464679..76b81a58c1 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -15,7 +15,6 @@ open Environ
 open EConstr
 open Inductiveops
 open Glob_term
-open Ltac_pretype
 open Evardefine
 
 (** {5 Compilation of pattern-matching } *)
@@ -42,9 +41,9 @@ val irrefutable : env -> cases_pattern -> bool
 
 val compile_cases :
   ?loc:Loc.t -> case_style ->
-  (type_constraint -> env -> evar_map ref -> ltac_var_map -> glob_constr -> unsafe_judgment) * evar_map ref ->
+  (type_constraint -> GlobEnv.t -> evar_map ref -> glob_constr -> unsafe_judgment) * evar_map ref ->
   type_constraint ->
-  env -> ltac_var_map -> glob_constr option * tomatch_tuples * cases_clauses ->
+  GlobEnv.t -> glob_constr option * tomatch_tuples * cases_clauses ->
   unsafe_judgment
 
 val constr_of_pat : 
@@ -59,7 +58,7 @@ val constr_of_pat :
            Names.Id.Set.t
 
 type 'a rhs =
-    { rhs_env    : env;
+    { rhs_env    : GlobEnv.t;
       rhs_vars   : Id.Set.t;
       avoid_ids  : Id.Set.t;
       it         : 'a option}
@@ -103,8 +102,7 @@ and pattern_continuation =
   | Result of cases_pattern list
 
 type 'a pattern_matching_problem =
-    { env       : env;
-      lvar      : Ltac_pretype.ltac_var_map;
+    { env       : GlobEnv.t;
       evdref    : evar_map ref;
       pred      : constr;
       tomatch   : tomatch_stack;
@@ -112,21 +110,19 @@ type 'a pattern_matching_problem =
       mat       : 'a matrix;
       caseloc   : Loc.t option;
       casestyle : case_style;
-      typing_function: type_constraint -> env -> evar_map ref -> 'a option -> unsafe_judgment }
-
+      typing_function: type_constraint -> GlobEnv.t -> evar_map ref -> 'a option -> unsafe_judgment }
 
 val compile : 'a pattern_matching_problem -> unsafe_judgment
 
 val prepare_predicate : ?loc:Loc.t ->
            (type_constraint ->
-            Environ.env -> Evd.evar_map ref -> ltac_var_map -> glob_constr -> unsafe_judgment) ->
-           Environ.env ->
+            GlobEnv.t -> Evd.evar_map ref -> glob_constr -> unsafe_judgment) ->
+           GlobEnv.t ->
            Evd.evar_map ->
-           Ltac_pretype.ltac_var_map ->
            (types * tomatch_type) list ->
-           (rel_context * rel_context) list ->
+           rel_context list ->
            constr option ->
-           glob_constr option -> (Evd.evar_map * Name.t list * constr) list
+           glob_constr option -> (Evd.evar_map * (Name.t * Name.t list) list * constr) list
 
-val make_return_predicate_ltac_lvar : Evd.evar_map -> Name.t ->
-  Glob_term.glob_constr -> constr -> Ltac_pretype.ltac_var_map -> ltac_var_map
+val make_return_predicate_ltac_lvar : GlobEnv.t -> Evd.evar_map -> Name.t ->
+  Glob_term.glob_constr -> constr -> GlobEnv.t
diff --git a/pretyping/globEnv.ml b/pretyping/globEnv.ml
new file mode 100644
index 0000000000..1bb4551f7c
--- /dev/null
+++ b/pretyping/globEnv.ml
@@ -0,0 +1,193 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Util
+open Pp
+open CErrors
+open Names
+open Environ
+open EConstr
+open Evarutil
+open Termops
+open Vars
+open Ltac_pretype
+
+(** This files provides a level of abstraction for the kind of
+    environment used for type inference (so-called pretyping); in
+    particular:
+    - it supports that term variables can be interpreted as Ltac
+      variables pointing to the effective expected name
+    - it incrementally and lazily computes the renaming of rel
+      variables used to build purely-named evar contexts
+*)
+
+type t = {
+  static_env : env;
+  (** For locating indices *)
+  renamed_env : env;
+  (** For name management *)
+  extra : ext_named_context Lazy.t;
+  (** Delay the computation of the evar extended environment *)
+  lvar : ltac_var_map;
+}
+
+let make env sigma lvar =
+  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) in
+  {
+    static_env = env;
+    renamed_env = env;
+    extra = lazy (get_extra env sigma);
+    lvar = lvar;
+  }
+
+let env env = env.static_env
+
+let ltac_interp_name { ltac_idents ; ltac_genargs } = function
+  | Anonymous -> Anonymous
+  | Name id as na ->
+      try Name (Id.Map.find id ltac_idents)
+      with Not_found ->
+        if Id.Map.mem id ltac_genargs then
+          user_err (str "Ltac variable" ++ spc () ++ Id.print id ++
+                    spc () ++ str "is not bound to an identifier." ++
+                    spc () ++str "It cannot be used in a binder.")
+        else na
+
+let push_rel sigma d env =
+  let d' = Context.Rel.Declaration.map_name (ltac_interp_name env.lvar) d in
+  let env = {
+    static_env = push_rel d env.static_env;
+    renamed_env = push_rel d' env.renamed_env;
+    extra = lazy (push_rel_decl_to_named_context sigma d' (Lazy.force env.extra));
+    lvar = env.lvar;
+    } in
+  d', env
+
+let push_rel_context ?(force_names=false) sigma ctx env =
+  let open Context.Rel.Declaration in
+  let ctx' = List.Smart.map (map_name (ltac_interp_name env.lvar)) ctx in
+  let ctx' = if force_names then Namegen.name_context env.renamed_env sigma ctx' else ctx' in
+  let env = {
+    static_env = push_rel_context ctx env.static_env;
+    renamed_env = push_rel_context ctx' env.renamed_env;
+    extra = lazy (List.fold_right (fun d acc -> push_rel_decl_to_named_context sigma d acc) ctx' (Lazy.force env.extra));
+    lvar = env.lvar;
+    } in
+  ctx', env
+
+let push_rec_types sigma (lna,typarray) env =
+  let open Context.Rel.Declaration in
+  let ctxt = Array.map2_i (fun i na t -> Context.Rel.Declaration.LocalAssum (na, lift i t)) lna typarray in
+  let env,ctx = Array.fold_left_map (fun e assum -> let (d,e) = push_rel sigma assum e in (e,d)) env ctxt in
+  Array.map get_name ctx, 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.renamed_env) in
+  let inst_rels = List.rev (rel_list 0 (nb_rel env.renamed_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 hide_variable env expansion id =
+  let lvar = env.lvar in
+  if Id.Map.mem id lvar.ltac_genargs then
+    let lvar = match expansion with
+    | Name id' ->
+       (* We are typically in a situation [match id return P with ... end]
+          which we interpret as [match id' as id' return P with ... end],
+          with [P] interpreted in an environment where [id] is bound to [id'].
+          The variable is already bound to [id'], so nothing to do *)
+       lvar
+    | _ ->
+       (* We are typically in a situation [match id return P with ... end]
+          with [id] bound to a non-variable term [c]. We interpret as
+         [match c as id return P with ... end], and hides [id] while
+         interpreting [P], since it has become a binder and cannot be anymore be
+         substituted by a variable coming from the Ltac substitution. *)
+       { lvar with
+         ltac_uconstrs = Id.Map.remove id lvar.ltac_uconstrs;
+         ltac_constrs = Id.Map.remove id lvar.ltac_constrs;
+         ltac_genargs = Id.Map.remove id lvar.ltac_genargs } in
+    { env with lvar }
+  else
+    env
+
+let protected_get_type_of env sigma c =
+  try Retyping.get_type_of ~lax:true env sigma c
+  with Retyping.RetypeError _ ->
+    user_err
+      (str "Cannot reinterpret " ++ quote (print_constr c) ++
+       str " in the current environment.")
+
+let invert_ltac_bound_name env id0 id =
+  try mkRel (pi1 (lookup_rel_id id (rel_context env.static_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 interp_ltac_variable ?loc typing_fun env sigma id =
+  (* Check if [id] is an ltac variable *)
+  try
+    let (ids,c) = Id.Map.find id env.lvar.ltac_constrs in
+    let subst = List.map (invert_ltac_bound_name env id) ids in
+    let c = substl subst c in
+      { uj_val = c; uj_type = protected_get_type_of env.renamed_env sigma c }
+  with Not_found ->
+  try
+    let {closure;term} = Id.Map.find id env.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. *)
+    typing_fun {env with 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 env.lvar.ltac_genargs then begin
+    let Geninterp.Val.Dyn (typ, _) = Id.Map.find id env.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;
+  raise Not_found
+
+module ConstrInterpObj =
+struct
+  type ('r, 'g, 't) obj =
+    unbound_ltac_var_map -> env -> Evd.evar_map -> types -> 'g -> constr * Evd.evar_map
+  let name = "constr_interp"
+  let default _ = None
+end
+
+module ConstrInterp = Genarg.Register(ConstrInterpObj)
+
+let register_constr_interp0 = ConstrInterp.register0
+
+let interp_glob_genarg env sigma ty arg =
+  let open Genarg in
+  let GenArg (Glbwit tag, arg) = arg in
+  let interp = ConstrInterp.obj tag in
+  interp env.lvar.ltac_genargs env.renamed_env sigma ty arg
diff --git a/pretyping/globEnv.mli b/pretyping/globEnv.mli
new file mode 100644
index 0000000000..2445618749
--- /dev/null
+++ b/pretyping/globEnv.mli
@@ -0,0 +1,79 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Names
+open Environ
+open Evd
+open EConstr
+open Ltac_pretype
+
+(** To embed constr in glob_constr *)
+
+val register_constr_interp0 :
+  ('r, 'g, 't) Genarg.genarg_type ->
+    (unbound_ltac_var_map -> env -> evar_map -> types -> 'g -> constr * evar_map) -> unit
+
+(** {6 Pretyping name management} *)
+
+(** The following provides a level of abstraction for the kind of
+    environment used for type inference (so-called pretyping); in
+    particular:
+    - it supports that term variables can be interpreted as Ltac
+      variables pointing to the effective expected name
+    - it incrementally and lazily computes the renaming of rel
+      variables used to build purely-named evar contexts
+*)
+
+(** Type of environment extended with naming and ltac interpretation data *)
+
+type t
+
+(** Build a pretyping environment from an ltac environment *)
+
+val make : env -> evar_map -> ltac_var_map -> t
+
+(** Export the underlying environement *)
+
+val env : t -> env
+
+(** Push to the environment, returning the declaration(s) with interpreted names *)
+
+val push_rel : evar_map -> rel_declaration -> t -> rel_declaration * t
+val push_rel_context : ?force_names:bool -> evar_map -> rel_context -> t -> rel_context * t
+val push_rec_types : evar_map -> Name.t array * constr array -> t -> Name.t array * t
+
+(** Declare an evar using renaming information *)
+
+val e_new_evar : t -> evar_map ref -> ?src:Evar_kinds.t Loc.located ->
+  ?naming:Namegen.intro_pattern_naming_expr -> constr -> constr
+
+(** [hide_variable env na id] tells to hide the binding of [id] in
+    the ltac environment part of [env] and to additionally rebind
+    it to [id'] in case [na] is some [Name id']. It is useful e.g.
+    for the dual status of [y] as term and binder. This is the case
+    of [match y return p with ... end] which implicitly denotes
+    [match z as z return p with ... end] when [y] is bound to a
+    variable [z] and [match t as y return p with ... end] when [y]
+    is bound to a non-variable term [t]. In the latter case, the
+    binding of [y] to [t] should be hidden in [p]. *)
+
+val hide_variable : t -> Name.t -> Id.t -> t
+
+(** In case a variable is not bound by a term binder, look if it has
+    an interpretation as a term in the ltac_var_map *)
+
+val interp_ltac_variable : ?loc:Loc.t -> (t -> Glob_term.glob_constr -> unsafe_judgment) ->
+  t -> evar_map -> Id.t -> unsafe_judgment
+
+(** Interpreting a generic argument, typically a "ltac:(...)", taking
+    into account the possible renaming *)
+
+val interp_glob_genarg : t -> evar_map -> constr ->
+  Genarg.glob_generic_argument -> constr * evar_map
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 24eb666828..bd13f1d00a 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -15,7 +15,6 @@ open Nameops
 open Globnames
 open Glob_term
 open Evar_kinds
-open Ltac_pretype
 
 (* Untyped intermediate terms, after ASTs and before constr. *)
 
@@ -577,22 +576,9 @@ let glob_constr_of_closed_cases_pattern p = match DAst.get p with
 
 let glob_constr_of_cases_pattern p = glob_constr_of_cases_pattern_aux false p
 
-(**********************************************************************)
-(* Interpreting ltac variables *)
-
-open Pp
-open CErrors
-
-let ltac_interp_name { ltac_idents ; ltac_genargs } = function
-  | Anonymous -> Anonymous
-  | Name id as n ->
-      try Name (Id.Map.find id ltac_idents)
-      with Not_found ->
-        if Id.Map.mem id ltac_genargs then
-          user_err (str"Ltac variable"++spc()++ Id.print id ++
-                           spc()++str"is not bound to an identifier."++spc()++
-                           str"It cannot be used in a binder.")
-        else n
+(* This has to be in some file... *)
+
+open Ltac_pretype
 
 let empty_lvar : ltac_var_map = {
   ltac_constrs = Id.Map.empty;
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index 7bc0140931..91a2ef9c1e 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -101,9 +101,4 @@ val glob_constr_of_cases_pattern : 'a cases_pattern_g -> 'a glob_constr_g
 
 val add_patterns_for_params_remove_local_defs : constructor -> 'a cases_pattern_g list -> 'a cases_pattern_g list
 
-(* [ltac_interp_name subst na] interprets a name according to a name
-   substitution (subst.ltac_idents) and a list of names
-   (subst.ltac_genargs) on which to fail; returns [na] otherwise *)
-val ltac_interp_name : Ltac_pretype.ltac_var_map -> Name.t -> Name.t
-
 val empty_lvar : Ltac_pretype.ltac_var_map
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
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 73f5b77e0e..fcc361b16b 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -122,11 +122,3 @@ val pretype_type :
 val ise_pretype_gen :
   inference_flags -> env -> evar_map ->
   ltac_var_map -> typing_constraint -> glob_constr -> evar_map * constr * types
-
-(**/**)
-
-(** To embed constr in glob_constr *)
-
-val register_constr_interp0 :
-  ('r, 'g, 't) Genarg.genarg_type ->
-    (unbound_ltac_var_map -> env -> evar_map -> types -> 'g -> constr * evar_map) -> unit
diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib
index 5da5aff449..d0359b43f4 100644
--- a/pretyping/pretyping.mllib
+++ b/pretyping/pretyping.mllib
@@ -32,6 +32,7 @@ Program
 Coercion
 Detyping
 Indrec
+GlobEnv
 Cases
 Pretyping
 Unification
diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v
index 0f22a1f0a0..3e19cfc8a6 100644
--- a/test-suite/success/ltac.v
+++ b/test-suite/success/ltac.v
@@ -348,3 +348,13 @@ symmetry in H.
 match goal with h:_ |- _ => assert (h=h) end. (* h should be H0 *)
 exact (eq_refl H0).
 Abort.
+
+(* Check that internal names used in "match" compilation to push "term
+   to match" on the environment are not interpreted as ltac variables *)
+
+Module ToMatchNames.
+Ltac g c := let r := constr:(match c return _ with a => 1 end) in idtac.
+Goal True.
+g 1.
+Abort.
+End ToMatchNames.