Namegen primitives now apply on evar constrs.

Incidentally, this fixes a printing bug in output/inference.v where the
displayed name of an evar was the wrong one because its type was not
evar-expanded enough.

6 files changed, 39 insertions, 39 deletions

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 55fda1c7db..669d808140 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -1458,7 +1458,7 @@ let _ =
   Hook.set Typeclasses.solve_all_instances_hook solve_inst
 
 let resolve_one_typeclass env ?(sigma=Evd.empty) gl unique =
-  let nc, gl, subst, _, _ = Evarutil.push_rel_context_to_named_context env gl in
+  let nc, gl, subst, _, _ = Evarutil.push_rel_context_to_named_context env sigma gl in
   let (gl,t,sigma) =
     Goal.V82.mk_goal sigma nc gl Store.empty in
   let (ev, _) = destEvar sigma t in
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index 188e215a5d..b08456f2f1 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -76,10 +76,24 @@ let build_dependent_inductive ind (mib,mip) =
        Context.Rel.to_extended_list mkRel mip.mind_nrealdecls mib.mind_params_ctxt
        @ Context.Rel.to_extended_list mkRel 0 realargs)
 
+let named_hd env t na = named_hd env Evd.empty (EConstr.of_constr t) na
+let name_assumption env = function
+| LocalAssum (na,t) -> LocalAssum (named_hd env t na, t)
+| LocalDef (na,c,t) -> LocalDef (named_hd env c na, c, t)
+
+let name_context env hyps =
+  snd
+    (List.fold_left
+       (fun (env,hyps) d ->
+	  let d' = name_assumption env d in (push_rel d' env, d' :: hyps))
+       (env,[]) (List.rev hyps))
+
 let my_it_mkLambda_or_LetIn s c = it_mkLambda_or_LetIn c s
 let my_it_mkProd_or_LetIn s c = Term.it_mkProd_or_LetIn c s
 let my_it_mkLambda_or_LetIn_name s c =
-  it_mkLambda_or_LetIn_name (Global.env()) c s
+  let env = Global.env () in
+  let mkLambda_or_LetIn_name d b = mkLambda_or_LetIn (name_assumption env d) b in
+  List.fold_left (fun c d -> mkLambda_or_LetIn_name d c) c s
 
 let get_coq_eq ctx =
   try
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 7f7a07b8fe..d9b6685179 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -857,14 +857,13 @@ let descend_then env sigma head dirn =
   (dirn_nlams,
    dirn_env,
    (fun dirnval (dfltval,resty) ->
-      let deparsign = make_arity_signature env true indf in
-      let deparsign = List.map (fun d -> map_rel_decl EConstr.of_constr d) deparsign in
+      let deparsign = make_arity_signature env sigma true indf in
       let p =
 	it_mkLambda_or_LetIn (lift (mip.mind_nrealargs+1) resty) deparsign in
       let build_branch i =
 	let result = if Int.equal i dirn then dirnval else dfltval in
-	let args = name_context env cstr.(i-1).cs_args in
-	let args = List.map (fun d -> map_rel_decl EConstr.of_constr d) args in
+	let cs_args = List.map (fun d -> map_rel_decl EConstr.of_constr d) cstr.(i-1).cs_args in
+	let args = name_context env sigma cs_args in
 	it_mkLambda_or_LetIn result args in
       let brl =
         List.map build_branch
@@ -905,8 +904,7 @@ let build_selector env sigma dirn c ind special default =
   let ind, _ = check_privacy env indp in
   let typ = Retyping.get_type_of env sigma default in
   let (mib,mip) = lookup_mind_specif env ind in
-  let deparsign = make_arity_signature env true indf in
-  let deparsign = List.map (fun d -> map_rel_decl EConstr.of_constr d) deparsign in
+  let deparsign = make_arity_signature env sigma true indf in
   let p = it_mkLambda_or_LetIn typ deparsign in
   let cstrs = get_constructors env indf in
   let build_branch i =
@@ -1535,9 +1533,6 @@ let decomp_tuple_term env sigma c t =
     in [((ex,exty),inner_code)]::iterated_decomp
   in decomprec (mkRel 1) c t
 
-let lambda_create env (a,b) =
-  mkLambda (named_hd env (EConstr.Unsafe.to_constr a) Anonymous, a, b)
-
 let subst_tuple_term env sigma dep_pair1 dep_pair2 b =
   let sigma = Sigma.to_evar_map sigma in
   let typ = get_type_of env sigma dep_pair1 in
@@ -1555,9 +1550,9 @@ let subst_tuple_term env sigma dep_pair1 dep_pair2 b =
   (* We build the expected goal *)
   let abst_B =
     List.fold_right
-      (fun (e,t) body -> lambda_create env (t,subst_term sigma e body)) e1_list b in
+      (fun (e,t) body -> lambda_create env sigma (t,subst_term sigma e body)) e1_list b in
   let pred_body = beta_applist sigma (abst_B,proj_list) in
-  let body = mkApp (lambda_create env (typ,pred_body),[|dep_pair1|]) in
+  let body = mkApp (lambda_create env sigma (typ,pred_body),[|dep_pair1|]) in
   let expected_goal = beta_applist sigma (abst_B,List.map fst e2_list) in
   (* Simulate now the normalisation treatment made by Logic.mk_refgoals *)
   let expected_goal = nf_betaiota sigma expected_goal in
diff --git a/tactics/inv.ml b/tactics/inv.ml
index ecb8eedaca..632a297211 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -90,8 +90,7 @@ let make_inv_predicate env evd indf realargs id status concl =
               | None ->
 		let sort = get_sort_family_of env !evd concl in
 		let sort = Evarutil.evd_comb1 (Evd.fresh_sort_in_family env) evd sort in
-		let p = make_arity env true indf sort in
-		let p = EConstr.of_constr p in
+		let p = make_arity env !evd true indf sort in
 		let evd',(p,ptyp) = Unification.abstract_list_all env
                   !evd p concl (realargs@[mkVar id])
 		in evd := evd'; p in
@@ -133,11 +132,7 @@ let make_inv_predicate env evd indf realargs id status concl =
         build_concl eqns args (succ n) restlist
   in
   let (newconcl, args) = build_concl [] [] 0 realargs in
-  let name_context env ctx =
-    let map f c = List.map (fun d -> Termops.map_rel_decl f d) c in
-    map EConstr.of_constr (name_context env (map EConstr.Unsafe.to_constr ctx))
-  in
-  let predicate = it_mkLambda_or_LetIn newconcl (name_context env hyps) in
+  let predicate = it_mkLambda_or_LetIn newconcl (name_context env !evd hyps) in
   let _ = Evarutil.evd_comb1 (Typing.type_of env) evd predicate in
   (* OK - this predicate should now be usable by res_elimination_then to
      do elimination on the conclusion. *)
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index d7c396179f..d864e547c5 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -119,11 +119,11 @@ let max_prefix_sign lid sign =
 let rec add_prods_sign env sigma t =
   match EConstr.kind sigma (whd_all env sigma t) with
     | Prod (na,c1,b) ->
-	let id = id_of_name_using_hdchar env (EConstr.Unsafe.to_constr t) na in
+	let id = id_of_name_using_hdchar env sigma t na in
 	let b'= subst1 (mkVar id) b in
         add_prods_sign (push_named (LocalAssum (id,c1)) env) sigma b'
     | LetIn (na,c1,t1,b) ->
-	let id = id_of_name_using_hdchar env (EConstr.Unsafe.to_constr t) na in
+	let id = id_of_name_using_hdchar env sigma t na in
 	let b'= subst1 (mkVar id) b in
         add_prods_sign (push_named (LocalDef (id,c1,t1)) env) sigma b'
     | _ -> (env,t)
@@ -147,8 +147,7 @@ let compute_first_inversion_scheme env sigma ind sort dep_option =
   let p = next_ident_away (Id.of_string "P") allvars in
   let pty,goal =
     if dep_option  then
-      let pty = make_arity env true indf sort in
-      let pty = EConstr.of_constr pty in
+      let pty = make_arity env sigma true indf sort in
       let goal =
 	mkProd
 	  (Anonymous, mkAppliedInd ind, applist(mkVar p,realargs@[mkRel 1]))
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index a29803251e..13ffbc52fe 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -412,16 +412,13 @@ let id_of_name_with_default id = function
 let default_id_of_sort s =
   if Sorts.is_small s then default_small_ident else default_type_ident
 
-let id_of_name_using_hdchar env c name =
-  id_of_name_using_hdchar env (EConstr.Unsafe.to_constr c) name
-
 let default_id env sigma decl =
   let open Context.Rel.Declaration in
   match decl with
   | LocalAssum (name,t) ->
       let dft = default_id_of_sort (Retyping.get_sort_of env sigma t) in
       id_of_name_with_default dft name
-  | LocalDef (name,b,_) -> id_of_name_using_hdchar env b name
+  | LocalDef (name,b,_) -> id_of_name_using_hdchar env sigma b name
 
 (* Non primitive introduction tactics are treated by intro_then_gen
    There is possibly renaming, with possibly names to avoid and
@@ -1075,14 +1072,14 @@ let intros_replacing ids =
 
 (* User-level introduction tactics *)
 
-let lookup_hypothesis_as_renamed env ccl = function
-  | AnonHyp n -> Detyping.lookup_index_as_renamed env (EConstr.Unsafe.to_constr ccl) n
-  | NamedHyp id -> Detyping.lookup_name_as_displayed env (EConstr.Unsafe.to_constr ccl) id
+let lookup_hypothesis_as_renamed env sigma ccl = function
+  | AnonHyp n -> Detyping.lookup_index_as_renamed env sigma ccl n
+  | NamedHyp id -> Detyping.lookup_name_as_displayed env sigma ccl id
 
 let lookup_hypothesis_as_renamed_gen red h gl =
   let env = Proofview.Goal.env gl in
   let rec aux ccl =
-    match lookup_hypothesis_as_renamed env ccl h with
+    match lookup_hypothesis_as_renamed env (Tacmach.New.project gl) ccl h with
       | None when red ->
         let (redfun, _) = Redexpr.reduction_of_red_expr env (Red true) in
         let Sigma (c, _, _) = redfun.e_redfun env (Proofview.Goal.sigma gl) ccl in
@@ -1350,7 +1347,7 @@ let enforce_prop_bound_names rename tac =
               if Retyping.get_sort_family_of env sigma t = InProp then
                 (* "very_standard" says that we should have "H" names only, but
                    this would break compatibility even more... *)
-                let s = match Namegen.head_name (EConstr.Unsafe.to_constr t) with
+                let s = match Namegen.head_name sigma t with
                   | Some id when not very_standard -> string_of_id id
                   | _ -> "" in
                 Name (add_suffix Namegen.default_prop_ident s)
@@ -2768,7 +2765,7 @@ let enough_by na t tac = forward false (Some (Some tac)) (ipat_of_name na) t
 
 (* Compute a name for a generalization *)
 
-let generalized_name sigma c t ids cl = function
+let generalized_name env sigma c t ids cl = function
   | Name id as na ->
       if Id.List.mem id ids then
 	user_err  (pr_id id ++ str " is already used.");
@@ -2783,7 +2780,7 @@ let generalized_name sigma c t ids cl = function
 	    (* On ne s'etait pas casse la tete : on avait pris pour nom de
                variable la premiere lettre du type, meme si "c" avait ete une
                constante dont on aurait pu prendre directement le nom *)
-	    named_hd (Global.env()) (EConstr.Unsafe.to_constr t) Anonymous
+	    named_hd env sigma t Anonymous
 
 (* Abstract over [c] in [forall x1:A1(c)..xi:Ai(c).T(c)] producing
    [forall x, x1:A1(x1), .., xi:Ai(x). T(x)] with all [c] abtracted in [Ai]
@@ -2795,7 +2792,7 @@ let generalize_goal_gen env sigma ids i ((occs,c,b),na) t cl =
   let dummy_prod = it_mkProd_or_LetIn mkProp decls in
   let newdecls,_ = decompose_prod_n_assum sigma i (subst_term_gen sigma EConstr.eq_constr_nounivs c dummy_prod) in
   let cl',sigma' = subst_closed_term_occ env sigma (AtOccs occs) c (it_mkProd_or_LetIn cl newdecls) in
-  let na = generalized_name sigma c t ids cl' na in
+  let na = generalized_name env sigma c t ids cl' na in
   let decl = match b with
     | None -> LocalAssum (na,t)
     | Some b -> LocalDef (na,b,t)
@@ -3230,7 +3227,7 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac =
             | Var id -> id
             | _ ->
             let type_of = Tacmach.New.pf_unsafe_type_of gl in
-            id_of_name_using_hdchar (Global.env()) (type_of c) Anonymous in
+            id_of_name_using_hdchar (Global.env()) sigma (type_of c) Anonymous in
             let x = fresh_id_in_env avoid id env in
 	    Tacticals.New.tclTHEN
 	      (letin_tac None (Name x) c None allHypsAndConcl)
@@ -4434,7 +4431,7 @@ let induction_gen clear_flag isrec with_evars elim
      declaring the induction argument as a new local variable *)
     let id =
     (* Type not the right one if partially applied but anyway for internal use*)
-      let x = id_of_name_using_hdchar (Global.env()) t Anonymous in
+      let x = id_of_name_using_hdchar (Global.env()) evd t Anonymous in
       new_fresh_id [] x gl in
     let info_arg = (is_arg_pure_hyp, not enough_applied) in
     pose_induction_arg_then
@@ -4471,7 +4468,7 @@ let induction_gen_l isrec with_evars elim names lc =
                 let type_of = Tacmach.New.pf_unsafe_type_of gl in
                 let sigma = Tacmach.New.project gl in
                 let x =
-		  id_of_name_using_hdchar (Global.env()) (type_of c) Anonymous in
+		  id_of_name_using_hdchar (Global.env()) sigma (type_of c) Anonymous in
 
                 let id = new_fresh_id [] x gl in
 		let newl' = List.map (fun r -> replace_term sigma c (mkVar id) r) l' in