Merge PR#513: A fix to #5414 (ident bound by ltac names now known for "match").

6 files changed, 123 insertions, 92 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index c3f392980..b88532e1b 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -245,6 +245,7 @@ let push_history_pattern n pci cont =
 
 type 'a pattern_matching_problem =
     { env       : env;
+      lvar      : Glob_term.ltac_var_map;
       evdref    : evar_map ref;
       pred      : constr;
       tomatch   : tomatch_stack;
@@ -346,25 +347,45 @@ let find_tomatch_tycon evdref env loc = function
   | None ->
       empty_tycon,None
 
-let coerce_row typing_fun evdref env pats (tomatch,(_,indopt)) =
+let make_return_predicate_ltac_lvar sigma na tm c lvar =
+  match na, tm.CAst.v 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 coerce_row typing_fun evdref env lvar 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 tomatch in
+  let j = typing_fun tycon env evdref !lvar tomatch in
   let evd, j = Coercion.inh_coerce_to_base ?loc:(loc_of_glob_constr tomatch) env !evdref j in
   evdref := evd;
   let typ = nf_evar !evdref j.uj_type in
+  lvar := make_return_predicate_ltac_lvar !evdref na tomatch j.uj_val !lvar;
   let t =
     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)
 
-let coerce_to_indtype typing_fun evdref env matx tomatchl = 
+let coerce_to_indtype typing_fun evdref env lvar 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
-  List.map2 (coerce_row typing_fun evdref env) matx' tomatchl
+  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
 
 (************************************************************************)
 (* Utils *)
@@ -1392,6 +1413,7 @@ 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
@@ -1824,6 +1846,7 @@ let build_inversion_problem loc env sigma tms t =
   let evdref = ref sigma in
   let pb =
     { env       = pb_env;
+      lvar      = empty_lvar;
       evdref    = evdref;
       pred      = (*ty *) mkSort s;
       tomatch   = sub_tms;
@@ -1847,15 +1870,15 @@ let build_initial_predicate arsign pred =
     | _ -> assert false
   in buildrec 0 pred [] (List.rev arsign)
 
-let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign =
+let extract_arity_signature ?(dolift=true) env0 lvar 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
       | NotInd (bo,typ) ->
 	  (match t with
-	    | None -> (match bo with
+	    | None -> let sign = match bo with
 		       | None -> [LocalAssum (na, lift n typ)]
-		       | Some b -> [LocalDef (na, lift n b, lift n typ)])
+		       | Some b -> [LocalDef (na, lift n b, lift n typ)] in sign,sign
 	    | Some (loc,_) ->
  	    user_err ?loc 
                 (str"Unexpected type annotation for a term of non inductive type."))
@@ -1865,22 +1888,31 @@ let extract_arity_signature ?(dolift=true) env0 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 =
+	  let realnal, realnal' =
 	    match t with
 	      | Some (loc,(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.");
-		  List.rev realnal
-	      | None -> List.make nrealargs_ctxt Anonymous in
-	  LocalAssum (na, EConstr.of_constr (build_dependent_inductive env0 indf'))
-	  ::(List.map2 RelDecl.set_name realnal arsign) in
+		  let realnal = List.rev realnal in
+                  let realnal' = List.map (ltac_interp_name lvar) realnal in
+                  realnal,realnal'
+	      | None ->
+                  let realnal = List.make nrealargs_ctxt Anonymous in
+                  realnal, realnal in
+          let na' = ltac_interp_name lvar na 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
   let rec buildrec n = function
     | [],[] -> []
     | (_,tm)::ltm, (_,x)::tmsign ->
 	let l = get_one_sign n tm x in
-	l :: buildrec (n + List.length l) (ltm,tmsign)
+	l :: buildrec (n + List.length (fst l)) (ltm,tmsign)
     | _ -> assert false
   in List.rev (buildrec 0 (tomatchl,tmsign))
 
@@ -1970,7 +2002,7 @@ 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 tomatchs arsign tycon pred =
+let prepare_predicate ?loc typing_fun env sigma lvar 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
@@ -1978,6 +2010,7 @@ let prepare_predicate ?loc typing_fun env sigma tomatchs arsign tycon pred =
     refresh_universes ~status:Evd.univ_flexible ~onlyalg:true (Some true)
 		      env sigma t
   in
+  let typing_arsign,building_arsign = List.split arsign in
   let preds =
     match pred, tycon with
     (* No return clause *)
@@ -1987,7 +2020,7 @@ let prepare_predicate ?loc typing_fun env sigma 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 arsign t in
+          prepare_predicate_from_arsign_tycon env sigma loc tomatchs typing_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
@@ -2006,22 +2039,22 @@ let prepare_predicate ?loc typing_fun env sigma tomatchs arsign tycon pred =
         (* 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 arsign)) t in
+        let pred2 = lift (List.length (List.flatten typing_arsign)) t in
 	[sigma1, pred1; sigma, pred2]
     (* Some type annotation *)
     | Some rtntyp, _ ->
       (* We extract the signature of the arity *)
-      let envar = List.fold_right push_rel_context arsign env in
+      let envar = List.fold_right push_rel_context typing_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 rtntyp in
+      let predcclj = typing_fun (mk_tycon (mkSort newt)) envar evdref lvar rtntyp in
       let sigma = !evdref in
       let predccl = nf_evar sigma predcclj.uj_val in
       [sigma, predccl]
   in
   List.map
     (fun (sigma,pred) ->
-      let (nal,pred) = build_initial_predicate arsign pred in
+      let (nal,pred) = build_initial_predicate building_arsign pred in
       sigma,nal,pred)
     preds
 
@@ -2441,10 +2474,10 @@ let context_of_arsign l =
     l ([], 0)
   in x
 
-let compile_program_cases ?loc style (typing_function, evdref) tycon env
+let compile_program_cases ?loc style (typing_function, evdref) tycon env lvar
     (predopt, tomatchl, eqns) =
   let typing_fun tycon env = function
-    | Some t ->	typing_function tycon env evdref t
+    | Some t ->	typing_function tycon env evdref lvar t
     | None -> Evarutil.evd_comb0 use_unit_judge evdref in
 
   (* We build the matrix of patterns and right-hand side *)
@@ -2452,14 +2485,15 @@ let compile_program_cases ?loc style (typing_function, evdref) tycon env
 
   (* We build the vector of terms to match consistently with the *)
   (* constructors found in patterns *)
-  let tomatchs = coerce_to_indtype typing_function evdref env matx tomatchl in
+  let predlvar,tomatchs = coerce_to_indtype typing_function evdref env lvar 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 len = List.length eqns in
   let sign, allnames, signlen, eqs, neqs, args =
     (* The arity signature *)
-    let arsign = extract_arity_signature ~dolift:false env tomatchs tomatchl in
+    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 *)
       (* Build the dependent arity signature, the equalities which makes
 	 the first part of the predicate and their instantiations. *)
     let avoid = [] in
@@ -2522,11 +2556,12 @@ let compile_program_cases ?loc style (typing_function, evdref) tycon env
   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 t
+    | Some t ->	typing_function tycon env evdref lvar t
     | None -> evd_comb0 use_unit_judge evdref in
 
   let pb =
     { env      = env;
+      lvar     = lvar;
       evdref   = evdref;
       pred     = pred;
       tomatch  = initial_pushed;
@@ -2548,10 +2583,10 @@ let compile_program_cases ?loc style (typing_function, evdref) tycon env
 (**************************************************************************)
 (* Main entry of the matching compilation                                 *)
 
-let compile_cases ?loc style (typing_fun, evdref) tycon env (predopt, tomatchl, eqns) =
+let compile_cases ?loc style (typing_fun, evdref) tycon env lvar (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 (predopt, tomatchl, eqns)
+      tycon env lvar (predopt, tomatchl, eqns)
   else
 
   (* We build the matrix of patterns and right-hand side *)
@@ -2559,15 +2594,15 @@ let compile_cases ?loc style (typing_fun, evdref) tycon env (predopt, tomatchl,
 
   (* We build the vector of terms to match consistently with the *)
   (* constructors found in patterns *)
-  let tomatchs = coerce_to_indtype typing_fun evdref env matx tomatchl in
+  let predlvar,tomatchs = coerce_to_indtype typing_fun evdref env lvar 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 tomatchs tomatchl in
-  let preds = prepare_predicate ?loc typing_fun env !evdref tomatchs arsign tycon predopt in
+  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 compile_for_one_predicate (sigma,nal,pred) =
     (* We push the initial terms to match and push their alias to rhs' envs *)
@@ -2598,13 +2633,14 @@ let compile_cases ?loc style (typing_fun, evdref) tycon env (predopt, tomatchl,
 
     (* 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 t
+    | Some t ->	typing_fun tycon env evdref lvar 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;
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index b16342db4..4b1fde25a 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -39,9 +39,9 @@ val irrefutable : env -> cases_pattern -> bool
 
 val compile_cases :
   ?loc:Loc.t -> case_style ->
-  (type_constraint -> env -> evar_map ref -> glob_constr -> unsafe_judgment) * evar_map ref ->
+  (type_constraint -> env -> evar_map ref -> ltac_var_map -> glob_constr -> unsafe_judgment) * evar_map ref ->
   type_constraint ->
-  env -> glob_constr option * tomatch_tuples * cases_clauses ->
+  env -> ltac_var_map -> glob_constr option * tomatch_tuples * cases_clauses ->
   unsafe_judgment
 
 val constr_of_pat : 
@@ -101,6 +101,7 @@ and pattern_continuation =
 
 type 'a pattern_matching_problem =
     { env       : env;
+      lvar      : Glob_term.ltac_var_map;
       evdref    : evar_map ref;
       pred      : constr;
       tomatch   : tomatch_stack;
@@ -115,10 +116,14 @@ val compile : 'a pattern_matching_problem -> unsafe_judgment
 
 val prepare_predicate : ?loc:Loc.t ->
            (Evarutil.type_constraint ->
-            Environ.env -> Evd.evar_map ref -> glob_constr -> unsafe_judgment) ->
+            Environ.env -> Evd.evar_map ref -> ltac_var_map -> glob_constr -> unsafe_judgment) ->
            Environ.env ->
            Evd.evar_map ->
+           Glob_term.ltac_var_map ->
            (types * tomatch_type) list ->
-           rel_context list ->
+           (rel_context * rel_context) list ->
            constr option ->
            glob_constr option -> (Evd.evar_map * Names.name list * constr) list
+
+val make_return_predicate_ltac_lvar : Evd.evar_map -> Names.name ->
+  Glob_term.glob_constr -> constr -> Glob_term.ltac_var_map -> Glob_term.ltac_var_map
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 62ff9ac70..9c09396cc 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -504,3 +504,27 @@ let glob_constr_of_closed_cases_pattern = function
       na,glob_constr_of_closed_cases_pattern_aux (CAst.make ?loc @@ PatCstr (cstr,l,Anonymous))
   | _ ->
       raise Not_found
+
+(**********************************************************************)
+(* 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()++ pr_id id ++
+                           spc()++str"is not bound to an identifier."++spc()++
+                           str"It cannot be used in a binder.")
+        else n
+
+let empty_lvar : ltac_var_map = {
+  ltac_constrs = Id.Map.empty;
+  ltac_uconstrs = Id.Map.empty;
+  ltac_idents = Id.Map.empty;
+  ltac_genargs = Id.Map.empty;
+}
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index 75db04f77..6bb421e73 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -83,3 +83,6 @@ val cases_pattern_of_glob_constr : Name.t -> glob_constr -> cases_pattern
 val glob_constr_of_closed_cases_pattern : cases_pattern -> Name.t * glob_constr
 
 val add_patterns_for_params_remove_local_defs : constructor -> cases_pattern list -> cases_pattern list
+
+val ltac_interp_name : Glob_term.ltac_var_map -> Names.name -> Names.name
+val empty_lvar : Glob_term.ltac_var_map
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 92e728683..7488f35bf 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -42,21 +42,11 @@ open Pretype_errors
 open Glob_term
 open Glob_ops
 open Evarconv
-open Pattern
 open Misctypes
 
 module NamedDecl = Context.Named.Declaration
 
 type typing_constraint = OfType of types | IsType | WithoutTypeConstraint
-type var_map = constr_under_binders Id.Map.t
-type uconstr_var_map = Glob_term.closed_glob_constr Id.Map.t
-type unbound_ltac_var_map = Geninterp.Val.t Id.Map.t
-type ltac_var_map = {
-  ltac_constrs : var_map;
-  ltac_uconstrs : uconstr_var_map;
-  ltac_idents: Id.t Id.Map.t;
-  ltac_genargs : unbound_ltac_var_map;
-}
 type glob_constr_ltac_closure = ltac_var_map * glob_constr
 type pure_open_constr = evar_map * EConstr.constr
 
@@ -419,17 +409,6 @@ let orelse_name name name' = match name with
   | Anonymous -> name'
   | _ -> name
 
-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()++ pr_id id ++
-                           spc()++str"is not bound to an identifier."++spc()++
-                           str"It cannot be used in a binder.")
-        else n
-
 let ltac_interp_name_env k0 lvar env sigma =
   (* envhd is the initial part of the env when pretype was called first *)
   (* (in practice is is probably 0, but we have to grant the
@@ -943,16 +922,20 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	  List.map (set_name Anonymous) arsgn
 	else arsgn
     in
-      let psign = LocalAssum (na, build_dependent_inductive env.ExtraEnv.env indf) :: arsgn in
+      let indt = build_dependent_inductive env.ExtraEnv.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 nar = List.length arsgn 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 lvar p in
+	    let pj = pretype_type empty_valcon env_p evdref predlvar p in
 	    let ccl = nf_evar !evdref pj.utj_val in
-	    let psign = make_arity_signature env.ExtraEnv.env !evdref true indf in (* with names *)
-	    let p = it_mkLambda_or_LetIn ccl psign 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
@@ -968,7 +951,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 
 	  | None ->
 	    let tycon = lift_tycon cs.cs_nargs tycon in
-	    let fj = pretype tycon env_f evdref lvar d in
+	    let fj = pretype tycon env_f evdref predlvar d in
 	    let ccl = nf_evar !evdref fj.uj_type in
 	    let ccl =
 	      if noccur_between !evdref 1 cs.cs_nargs ccl then
@@ -977,7 +960,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 		error_cant_find_case_type ?loc env.ExtraEnv.env !evdref
 		  cj.uj_val in
 		 (* let ccl = refresh_universes ccl in *)
-	    let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in
+	    let 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;
@@ -1004,14 +987,19 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	  else arsgn
       in
       let nar = List.length arsgn in
-      let psign = LocalAssum (na, build_dependent_inductive env.ExtraEnv.env indf) :: arsgn in
+      let indt = build_dependent_inductive env.ExtraEnv.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 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 lvar p in
+	  let pj = pretype_type empty_valcon env_p evdref predlvar 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 ->
@@ -1021,7 +1009,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
               let env = ltac_interp_name_env k0 lvar env !evdref in
               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 =
@@ -1054,8 +1042,8 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 
   | GCases (sty,po,tml,eqns) ->
     Cases.compile_cases ?loc sty
-      ((fun vtyc env evdref -> pretype vtyc (make_env env !evdref) evdref lvar),evdref)
-      tycon env.ExtraEnv.env (* loc *) (po,tml,eqns)
+      ((fun vtyc env evdref -> pretype vtyc (make_env env !evdref) evdref),evdref)
+      tycon env.ExtraEnv.env (* loc *) lvar (po,tml,eqns)
 
   | GCast (c,k) ->
     let cj =
@@ -1198,13 +1186,6 @@ let no_classes_no_fail_inference_flags = {
 let all_and_fail_flags = default_inference_flags true
 let all_no_fail_flags = default_inference_flags false
 
-let empty_lvar : ltac_var_map = {
-  ltac_constrs = Id.Map.empty;
-  ltac_uconstrs = Id.Map.empty;
-  ltac_idents = Id.Map.empty;
-  ltac_genargs = Id.Map.empty;
-}
-
 let on_judgment sigma f j =
   let c = mkCast(j.uj_val,DEFAULTcast, j.uj_type) in
   let (c,_,t) = destCast sigma (f c) in
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index dcacd0720..e17468ef8 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -12,7 +12,6 @@
    into elementary ones, insertion of coercions and resolution of
    implicit arguments. *)
 
-open Names
 open Term
 open Environ
 open Evd
@@ -28,23 +27,6 @@ val search_guard :
 
 type typing_constraint = OfType of types | IsType | WithoutTypeConstraint
 
-type var_map = Pattern.constr_under_binders Id.Map.t
-type uconstr_var_map = Glob_term.closed_glob_constr Id.Map.t
-type unbound_ltac_var_map = Geninterp.Val.t Id.Map.t
-
-type ltac_var_map = {
-  ltac_constrs : var_map;
-  (** Ltac variables bound to constrs *)
-  ltac_uconstrs : uconstr_var_map;
-  (** Ltac variables bound to untyped constrs *)
-  ltac_idents: Id.t Id.Map.t;
-  (** Ltac variables bound to identifiers *)
-  ltac_genargs : unbound_ltac_var_map;
-  (** Ltac variables bound to other kinds of arguments *)
-}
-
-val empty_lvar : ltac_var_map
-
 type glob_constr_ltac_closure = ltac_var_map * glob_constr
 type pure_open_constr = evar_map * constr