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.

5 files changed, 18 insertions, 17 deletions

diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
index ae057b4581..828d634d0c 100644
--- a/plugins/decl_mode/decl_interp.ml
+++ b/plugins/decl_mode/decl_interp.ml
@@ -316,7 +316,7 @@ let rec match_aliases names constr = function
       let args,bnames,body = match_aliases qnames body q in
 	st::args,bnames,body
 
-let detype_ground env c = Detyping.detype false [] env Evd.empty c
+let detype_ground env c = Detyping.detype false [] env Evd.empty (EConstr.of_constr c)
 
 let interp_cases info env sigma params (pat:cases_pattern_expr) hyps =
   let et,pinfo =
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index adc4ad8a33..4fe59d755e 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -440,7 +440,7 @@ let concl_refiner metas body gls =
       [] -> anomaly ~label:"concl_refiner" (Pp.str "cannot happen")
     | (n,typ)::rest ->
 	let _A = subst_meta subst typ in
-	let x = id_of_name_using_hdchar env _A Anonymous in
+	let x = id_of_name_using_hdchar env evd (EConstr.of_constr _A) Anonymous in
 	let _x = fresh_id avoid x gls in
 	let nenv = Environ.push_named (LocalAssum (_x,_A)) env in
 	let asort = family_of_sort (Typing.e_sort_of nenv (ref evd) (EConstr.of_constr _A)) in
@@ -895,7 +895,6 @@ let build_per_info etype casee gls =
   let ctyp=pf_unsafe_type_of gls (EConstr.of_constr casee) in
   let is_dep = dependent (project gls) (EConstr.of_constr casee) concl in
   let hd,args = decompose_app (special_whd gls ctyp) in
-  let ctyp = EConstr.Unsafe.to_constr ctyp in
   let (ind,u) =
     try
       destInd hd
@@ -909,10 +908,11 @@ let build_per_info etype casee gls =
   let params,real_args = List.chop nparams args in
   let abstract_obj c body =
     let typ=pf_unsafe_type_of gls (EConstr.of_constr c) in
-    let typ = EConstr.Unsafe.to_constr typ in
-      lambda_create env (typ,subst_term (project gls) (EConstr.of_constr c) (EConstr.of_constr body)) in
+      lambda_create env (project gls) (typ,Termops.subst_term (project gls) (EConstr.of_constr c) body) in
   let pred= List.fold_right abstract_obj
-    real_args (lambda_create env (ctyp,subst_term (project gls) (EConstr.of_constr casee) concl)) in
+    real_args (lambda_create env (project gls) (ctyp,Termops.subst_term (project gls) (EConstr.of_constr casee) concl)) in
+  let ctyp = EConstr.Unsafe.to_constr ctyp in
+  let pred = EConstr.Unsafe.to_constr pred in
     is_dep,
   {per_casee=casee;
    per_ctype=ctyp;
@@ -1275,16 +1275,15 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
 	let env=pf_env gls in
 	let ctyp=pf_unsafe_type_of gls (EConstr.of_constr casee) in
 	let hd,all_args = decompose_app (special_whd gls ctyp) in
-	let ctyp = EConstr.Unsafe.to_constr ctyp in
 	let ind', u = destInd hd in
 	let _ = assert (eq_ind ind' ind) in (* just in case *)
 	let params,real_args = List.chop nparams all_args in
 	let abstract_obj c body =
 	  let typ=pf_unsafe_type_of gls (EConstr.of_constr c) in
-	  let typ = EConstr.Unsafe.to_constr typ in
-	    lambda_create env (typ,subst_term (project gls) (EConstr.of_constr c) (EConstr.of_constr body)) in
+	    lambda_create env (project gls) (typ,Termops.subst_term (project gls) (EConstr.of_constr c) body) in
 	let elim_pred = List.fold_right abstract_obj
-	  real_args (lambda_create env (ctyp,subst_term (project gls) (EConstr.of_constr casee) concl)) in
+	  real_args (lambda_create env (project gls) (ctyp,Termops.subst_term (project gls) (EConstr.of_constr casee) concl)) in
+        let elim_pred = EConstr.Unsafe.to_constr elim_pred in
 	let case_info = Inductiveops.make_case_info env ind RegularStyle in
 	let gen_arities = Inductive.arities_of_constructors (ind,u) spec in
 	let f_ids typ =
@@ -1345,6 +1344,7 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
 
 let understand_my_constr env sigma c concl =
   let env = env in
+  let c = EConstr.of_constr c in
   let rawc = Detyping.detype false [] env Evd.empty c in
   let rec frob = function
     | GEvar _ -> GHole (Loc.ghost,Evar_kinds.QuestionMark Evar_kinds.Expand,Misctypes.IntroAnonymous,None)
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index fd2f4bbd37..63bd3848f6 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -421,7 +421,7 @@ let rec pattern_to_term_and_type env typ  = function
 	Array.to_list
 	  (Array.init
 	     (cst_narg - List.length patternl)
-	     (fun i -> Detyping.detype false [] env (Evd.from_env env) csta.(i))
+	     (fun i -> Detyping.detype false [] env (Evd.from_env env) (EConstr.of_constr csta.(i)))
 	  )
       in
       let patl_as_term =
@@ -504,7 +504,6 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 		*)
 		let rt_as_constr,ctx = Pretyping.understand env (Evd.from_env env) rt in
 		let rt_typ = Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr rt_as_constr) in
-                let rt_typ = EConstr.Unsafe.to_constr rt_typ in
 		let res_raw_type = Detyping.detype false [] env (Evd.from_env env) rt_typ in
 		let res = fresh_id args_res.to_avoid "_res" in
 		let new_avoid = res::args_res.to_avoid in
@@ -757,7 +756,6 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
 			let typ_of_id =
 			  Typing.unsafe_type_of env_with_pat_ids (Evd.from_env env) (EConstr.mkVar id)
 			in
-			let typ_of_id = EConstr.Unsafe.to_constr typ_of_id in
 			let raw_typ_of_id =
 			  Detyping.detype false []
 			    env_with_pat_ids (Evd.from_env env) typ_of_id
@@ -804,6 +802,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
 	      List.map3
 	      (fun pat e typ_as_constr ->
 		 let this_pat_ids = ids_of_pat pat in
+		 let typ_as_constr = EConstr.of_constr typ_as_constr in
 		 let typ = Detyping.detype false [] new_env (Evd.from_env env) typ_as_constr in
 		 let pat_as_term = pattern_to_term pat in
 		 List.fold_right
@@ -811,7 +810,6 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
 		      if Id.Set.mem id this_pat_ids
 		      then (Prod (Name id),
 		      let typ_of_id = Typing.unsafe_type_of new_env (Evd.from_env env) (EConstr.mkVar id) in
-		      let typ_of_id = EConstr.Unsafe.to_constr typ_of_id in
 		      let raw_typ_of_id =
 			Detyping.detype false [] new_env (Evd.from_env env) typ_of_id
 		      in
@@ -970,7 +968,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 			    (List.map
 			      (fun p -> Detyping.detype false []
 				 env (Evd.from_env env)
-				 p) params)@(Array.to_list
+				 (EConstr.of_constr p)) params)@(Array.to_list
 				      (Array.make
 					 (List.length args' - nparam)
 					 (mkGHole ()))))
@@ -988,6 +986,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 			    let ty' = snd (Util.List.chop nparam ty) in
 			    List.fold_left2
 			      (fun acc var_as_constr arg ->
+                                let arg = EConstr.of_constr arg in
 				 if isRel var_as_constr
 				 then
 				   let na = RelDecl.get_name (Environ.lookup_rel (destRel var_as_constr) env) in
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 691385fad0..44aacaf45e 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -777,6 +777,7 @@ let merge_inductive_body (shift:merge_infos) avoid (oib1:one_inductive_body)
   let mkrawcor nme avoid typ =
     (* first replace rel 1 by a varname *)
     let substindtyp = substitterm 0 (mkRel 1) (mkVar nme) typ in
+    let substindtyp = EConstr.of_constr substindtyp in
     Detyping.detype false (Id.Set.elements avoid) (Global.env()) Evd.empty substindtyp in
   let lcstr1: glob_constr list =
     Array.to_list (Array.map (mkrawcor ind1name avoid) oib1.mind_user_lc) in
@@ -860,6 +861,7 @@ let glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift
 let mkProd_reldecl (rdecl:Context.Rel.Declaration.t) (t2:glob_constr) =
   match rdecl with
     | LocalAssum (nme,t) ->
+        let t = EConstr.of_constr t in
         let traw = Detyping.detype false [] (Global.env()) Evd.empty t in
         GProd (Loc.ghost,nme,Explicit,traw,t2)
     | LocalDef _ -> assert false
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index f5ea32878c..2a66ba8523 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -122,8 +122,8 @@ let pf_get_new_ids idl g =
     []
 
 let compute_renamed_type gls c =
-  EConstr.of_constr (rename_bound_vars_as_displayed (*no avoid*) [] (*no rels*) []
-    (EConstr.Unsafe.to_constr (pf_unsafe_type_of gls c)))
+  rename_bound_vars_as_displayed (project gls) (*no avoid*) [] (*no rels*) []
+    (pf_unsafe_type_of gls c)
 let h'_id = Id.of_string "h'"
 let teq_id = Id.of_string "teq"
 let ano_id = Id.of_string "anonymous"