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

Also taking into account a name in the return clause and in the
indices.

Note the double meaning ``bound as a term to match'' and ``binding in
the "as" clause'' when the term to match is a variable for all of
"match", "if" and "let".

19 files changed, 309 insertions, 122 deletions

diff --git a/API/API.mli b/API/API.mli
index d844e8bf5..2045fadae 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -2510,6 +2510,20 @@ sig
    and closed_glob_constr = Glob_term.closed_glob_constr = {
        closure: closure;
        term: glob_constr }
+
+  type var_map = Pattern.constr_under_binders Names.Id.Map.t
+  type uconstr_var_map = Glob_term.closed_glob_constr Names.Id.Map.t
+  type unbound_ltac_var_map = Geninterp.Val.t Names.Id.Map.t
+  type ltac_var_map = Glob_term.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: Names.Id.t Names.Id.Map.t;
+        (** Ltac variables bound to identifiers *)
+        ltac_genargs : unbound_ltac_var_map;
+        (** Ltac variables bound to other kinds of arguments *)
+      }
 end
 
 module Libnames :
@@ -2875,10 +2889,6 @@ sig
                          | IsType
                          | WithoutTypeConstraint
 
-  type var_map = Pattern.constr_under_binders Names.Id.Map.t
-  type uconstr_var_map = Glob_term.closed_glob_constr Names.Id.Map.t
-  type unbound_ltac_var_map = Geninterp.Val.t Names.Id.Map.t
-
   type inference_hook = Environ.env -> Evd.evar_map -> Evar.t -> Evd.evar_map * EConstr.constr
   type inference_flags = Pretyping.inference_flags = {
       use_typeclasses : bool;
@@ -2888,22 +2898,11 @@ sig
       expand_evars : bool
     }
 
-  type ltac_var_map = Pretyping.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: Names.Id.t Names.Id.Map.t;
-        (** Ltac variables bound to identifiers *)
-        ltac_genargs : unbound_ltac_var_map;
-        (** Ltac variables bound to other kinds of arguments *)
-      }                                                 
   type pure_open_constr = Evd.evar_map * EConstr.constr
-  type glob_constr_ltac_closure = ltac_var_map * Glob_term.glob_constr
+  type glob_constr_ltac_closure = Glob_term.ltac_var_map * Glob_term.glob_constr
 
-  val empty_lvar : ltac_var_map
   val understand_ltac : inference_flags ->
-                        Environ.env -> Evd.evar_map -> ltac_var_map ->
+                        Environ.env -> Evd.evar_map -> Glob_term.ltac_var_map ->
                         typing_constraint -> Glob_term.glob_constr -> pure_open_constr
   val understand_tcc : ?flags:inference_flags -> Environ.env -> Evd.evar_map ->
                        ?expected_type:typing_constraint -> Glob_term.glob_constr -> Evd.evar_map * EConstr.constr
@@ -2917,11 +2916,11 @@ sig
   val interp_elimination_sort : Misctypes.glob_sort -> Sorts.family
   val register_constr_interp0 :
     ('r, 'g, 't) Genarg.genarg_type ->
-    (unbound_ltac_var_map -> Environ.env -> Evd.evar_map -> EConstr.types -> 'g -> EConstr.constr * Evd.evar_map) -> unit
+    (Glob_term.unbound_ltac_var_map -> Environ.env -> Evd.evar_map -> EConstr.types -> 'g -> EConstr.constr * Evd.evar_map) -> unit
   val all_and_fail_flags : inference_flags
   val ise_pretype_gen :
     inference_flags -> Environ.env -> Evd.evar_map ->
-    ltac_var_map -> typing_constraint -> Glob_term.glob_constr -> Evd.evar_map * EConstr.constr
+    Glob_term.ltac_var_map -> typing_constraint -> Glob_term.glob_constr -> Evd.evar_map * EConstr.constr
 end
 
 module Evarconv :
@@ -3746,6 +3745,7 @@ sig
   val cases_pattern_of_glob_constr : Names.Name.t -> Glob_term.glob_constr -> Glob_term.cases_pattern
   val map_glob_constr :
     (Glob_term.glob_constr -> Glob_term.glob_constr) -> Glob_term.glob_constr -> Glob_term.glob_constr
+  val empty_lvar : Glob_term.ltac_var_map
 end
 
 module Indrec :
diff --git a/intf/glob_term.ml b/intf/glob_term.ml
index 5da20c9d1..a35dae4aa 100644
--- a/intf/glob_term.ml
+++ b/intf/glob_term.ml
@@ -95,3 +95,19 @@ type closure = {
 and closed_glob_constr = {
   closure: closure;
   term: glob_constr }
+
+(** Ltac variable maps *)
+type var_map = Pattern.constr_under_binders Id.Map.t
+type uconstr_var_map = 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 *)
+}
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index eae72d9e8..1f2a0a1b4 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -722,7 +722,7 @@ let resolve_and_replace_implicits ?(flags=Pretyping.all_and_fail_flags) ?(expect
   (* we first (pseudo) understand [rt] and get back the computed evar_map *)
   (* FIXME : JF (30/03/2017) I'm not completely sure to have split understand as needed. 
 If someone knows how to prevent solved existantial removal in  understand, please do not hesitate to change the computation of [ctx] here *) 
-  let ctx,_ = Pretyping.ise_pretype_gen flags env sigma Pretyping.empty_lvar expected_type rt in
+  let ctx,_ = Pretyping.ise_pretype_gen flags env sigma Glob_ops.empty_lvar expected_type rt in
   let ctx, f = Evarutil.nf_evars_and_universes ctx in
 
   (* then we map [rt] to replace the implicit holes by their values *)
diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml
index 958f43bd7..4f6f244f8 100644
--- a/plugins/ltac/evar_tactics.ml
+++ b/plugins/ltac/evar_tactics.ml
@@ -28,7 +28,7 @@ let instantiate_evar evk (ist,rawc) sigma =
   let filtered = Evd.evar_filtered_env evi in
   let constrvars = Tacinterp.extract_ltac_constr_values ist filtered in
   let lvar = {
-    Pretyping.ltac_constrs = constrvars;
+    Glob_term.ltac_constrs = constrvars;
     ltac_uconstrs = Names.Id.Map.empty;
     ltac_idents = Names.Id.Map.empty;
     ltac_genargs = ist.Geninterp.lfun;
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index 9b6ac8a9a..67893bd11 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -386,7 +386,7 @@ type ltac_call_kind =
   | LtacNameCall of ltac_constant
   | LtacAtomCall of glob_atomic_tactic_expr
   | LtacVarCall of Id.t * glob_tactic_expr
-  | LtacConstrInterp of Glob_term.glob_constr * Pretyping.ltac_var_map
+  | LtacConstrInterp of Glob_term.glob_constr * Glob_term.ltac_var_map
 
 type ltac_trace = ltac_call_kind Loc.located list
 
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 85d3944b1..18c9e839a 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -605,10 +605,10 @@ let interp_gen kind ist pattern_mode flags env sigma c =
   let { closure = constrvars ; term } =
     interp_glob_closure ist env sigma ~kind:kind_for_intern ~pattern_mode c in
   let vars = {
-    Pretyping.ltac_constrs = constrvars.typed;
-    Pretyping.ltac_uconstrs = constrvars.untyped;
-    Pretyping.ltac_idents = constrvars.idents;
-    Pretyping.ltac_genargs = ist.lfun;
+    Glob_term.ltac_constrs = constrvars.typed;
+    Glob_term.ltac_uconstrs = constrvars.untyped;
+    Glob_term.ltac_idents = constrvars.idents;
+    Glob_term.ltac_genargs = ist.lfun;
   } in
   (* Jason Gross: To avoid unnecessary modifications to tacinterp, as
       suggested by Arnaud Spiwack, we run push_trace immediately.  We do
diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml
index 8126421c7..d495eb821 100644
--- a/plugins/ltac/tactic_debug.ml
+++ b/plugins/ltac/tactic_debug.ml
@@ -366,7 +366,7 @@ let explain_ltac_call_trace last trace loc =
   | Tacexpr.LtacAtomCall te ->
       quote (Pptactic.pr_glob_tactic (Global.env())
               (Tacexpr.TacAtom (Loc.tag te)))
-  | Tacexpr.LtacConstrInterp (c, { Pretyping.ltac_constrs = vars }) ->
+  | Tacexpr.LtacConstrInterp (c, { Glob_term.ltac_constrs = vars }) ->
       quote (Printer.pr_glob_constr_env (Global.env()) c) ++
         (if not (Id.Map.is_empty vars) then
           strbrk " (with " ++
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 38ee4be45..d1b4eb850 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -226,8 +226,8 @@ let isAppInd gl c =
 
 let interp_refine ist gl rc =
   let constrvars = Tacinterp.extract_ltac_constr_values ist (pf_env gl) in
-  let vars = { Pretyping.empty_lvar with
-    Pretyping.ltac_constrs = constrvars; ltac_genargs = ist.Tacinterp.lfun
+  let vars = { Glob_ops.empty_lvar with
+    Glob_term.ltac_constrs = constrvars; ltac_genargs = ist.Tacinterp.lfun
   } in
   let kind = Pretyping.OfType (pf_concl gl) in
   let flags = {
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
 
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 2aa620c1d..ef454299e 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -428,7 +428,7 @@ module V82 = struct
       in
       let env = Evd.evar_filtered_env evi in
       let rawc = Constrintern.intern_constr env com in
-      let ltac_vars = Pretyping.empty_lvar in
+      let ltac_vars = Glob_ops.empty_lvar in
       let sigma = Evar_refiner.w_refine (evk, evi) (ltac_vars, rawc) sigma in
       Proofview.Unsafe.tclEVARS sigma
     end in
diff --git a/test-suite/bugs/closed/5414.v b/test-suite/bugs/closed/5414.v
new file mode 100644
index 000000000..2522a274f
--- /dev/null
+++ b/test-suite/bugs/closed/5414.v
@@ -0,0 +1,12 @@
+(* Use of idents bound to ltac names in a "match" *)
+
+Definition foo : Type.
+Proof.
+  let x := fresh "a" in
+  refine (forall k : nat * nat, let '(x, _) := k in (_ : Type)).
+  exact (a = a).
+Defined.
+Goal foo.
+intros k. elim k. (* elim because elim keeps names *)
+intros.
+Check a. (* We check that the name is "a" *)
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index f064dfe76..97fa8e254 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -80,3 +80,49 @@ fun '(D n m p q) => n + m + p + q
      : J -> nat
 The command has indeed failed with message:
 The constructor D (in type J) expects 3 arguments.
+lem1 = 
+fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl
+     : forall k : nat * nat, k = k
+lem2 = 
+fun dd : bool => if dd as aa return (aa = aa) then eq_refl else eq_refl
+     : forall k : bool, k = k
+
+Argument scope is [bool_scope]
+lem3 = 
+fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl
+     : forall k : nat * nat, k = k
+1 subgoal
+  
+  x : nat
+  n, n0 := match x + 0 with
+           | 0 => 0
+           | S _ => 0
+           end : nat
+  e,
+  e0 := match x + 0 as y return (y = y) with
+        | 0 => eq_refl
+        | S n => eq_refl
+        end : x + 0 = x + 0
+  n1, n2 := match x with
+            | 0 => 0
+            | S _ => 0
+            end : nat
+  e1, e2 := match x return (x = x) with
+            | 0 => eq_refl
+            | S n => eq_refl
+            end : x = x
+  ============================
+  x + 0 = 0
+1 subgoal
+  
+  p : nat
+  a,
+  a0 := match eq_refl as y in (_ = e) return (y = y /\ e = e) with
+        | eq_refl => conj eq_refl eq_refl
+        end : eq_refl = eq_refl /\ p = p
+  a1,
+  a2 := match eq_refl in (_ = e) return (p = p /\ e = e) with
+        | eq_refl => conj eq_refl eq_refl
+        end : p = p /\ p = p
+  ============================
+  eq_refl = eq_refl
diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v
index 6a4fd007d..17fee3303 100644
--- a/test-suite/output/Cases.v
+++ b/test-suite/output/Cases.v
@@ -121,3 +121,66 @@ Check fun x => let '(D n m p q) := x in n+m+p+q.
 (* This used to succeed, being interpreted as "let '{{n, m, p}} := ..." *)
 
 Fail Check fun x : J => let '{{n, m, _}} p := x in n + m + p.
+
+(* Test use of idents bound to ltac names in a "match" *)
+
+Lemma lem1 : forall k, k=k :>nat * nat.
+let x := fresh "aa" in
+let y := fresh "bb" in
+let z := fresh "cc" in
+let k := fresh "dd" in
+refine (fun k : nat * nat => match k as x return x = x with (y,z) => eq_refl end).
+Qed.
+Print lem1.
+
+Lemma lem2 : forall k, k=k :> bool.
+let x := fresh "aa" in
+let y := fresh "bb" in
+let z := fresh "cc" in
+let k := fresh "dd" in
+refine (fun k => if k as x return x = x then eq_refl else eq_refl).
+Qed.
+Print lem2.
+
+Lemma lem3 : forall k, k=k :>nat * nat.
+let x := fresh "aa" in
+let y := fresh "bb" in
+let z := fresh "cc" in
+let k := fresh "dd" in
+refine (fun k : nat * nat => let (y,z) as x return x = x := k in eq_refl).
+Qed.
+Print lem3.
+
+Lemma lem4 x : x+0=0.
+match goal with |- ?y = _ => pose (match y with 0 => 0 | S n => 0 end) end.
+match goal with |- ?y = _ => pose (match y as y with 0 => 0 | S n => 0 end) end.
+match goal with |- ?y = _ => pose (match y as y return y=y with 0 => eq_refl | S n => eq_refl end) end.
+match goal with |- ?y = _ => pose (match y return y=y with 0 => eq_refl | S n => eq_refl end) end.
+match goal with |- ?y + _ = _ => pose (match y with 0 => 0 | S n => 0 end) end.
+match goal with |- ?y + _ = _ => pose (match y as y with 0 => 0 | S n => 0 end) end.
+match goal with |- ?y + _ = _ => pose (match y as y return y=y with 0 => eq_refl | S n => eq_refl end) end.
+match goal with |- ?y + _ = _ => pose (match y return y=y with 0 => eq_refl | S n => eq_refl end) end.
+Show.
+
+Lemma lem5 (p:nat) : eq_refl p = eq_refl p.
+let y := fresh "n" in (* Checking that y is hidden *)
+  let z := fresh "e" in (* Checking that z is hidden *)
+  match goal with
+  |- ?y = _ => pose (match y as y in _ = z return y=y /\ z=z with eq_refl => conj eq_refl eq_refl end)
+  end.
+let y := fresh "n" in
+  let z := fresh "e" in
+  match goal with
+  |- ?y = _ => pose (match y in _ = z return y=y /\ z=z with eq_refl => conj eq_refl eq_refl end)
+  end.
+let y := fresh "n" in
+  let z := fresh "e" in
+  match goal with
+  |- eq_refl ?y = _ => pose (match eq_refl y in _ = z return y=y /\ z=z with eq_refl => conj eq_refl eq_refl end)
+  end.
+let p := fresh "p" in
+  let z := fresh "e" in
+  match goal with
+  |- eq_refl ?p = _ => pose (match eq_refl p in _ = z return p=p /\ z=z with eq_refl => conj eq_refl eq_refl end)
+  end.
+Show.
diff --git a/test-suite/success/Case19.v b/test-suite/success/Case19.v
index e59828def..ce98879a5 100644
--- a/test-suite/success/Case19.v
+++ b/test-suite/success/Case19.v
@@ -17,3 +17,22 @@ Fail exists (fun x =>
         with
         | eq_refl => eq_refl
         end).
+Abort.
+
+(* Some tests with ltac matching on building "if" and "let" *)
+
+Goal forall b c d, (if negb b then c else d) = 0.
+intros.
+match goal with
+|- (if ?b then ?c else ?d) = 0 => transitivity (if b then d else c)
+end.
+Abort.
+
+Definition swap {A} {B} '((x,y):A*B) := (y,x).
+
+Goal forall p, (let '(x,y) := swap p in x + y) = 0.
+intros.
+match goal with
+|- (let '(x,y) := ?p in x + y) = 0 => transitivity (let (x,y) := p in x+y)
+end.
+Abort.