Renaming is_template_polymorphic -> is_template_polymorphic_ind.

This emphasizes that it works only on inductive types.

Also, the name is_template_polymorphic will be reused for a more
general version.

6 files changed, 10 insertions, 10 deletions

diff --git a/engine/termops.ml b/engine/termops.ml
index f720e5195d..c0dd9d07d1 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -1173,7 +1173,7 @@ let isGlobalRef sigma c =
   | Const _ | Ind _ | Construct _ | Var _ -> true
   | _ -> false
 
-let is_template_polymorphic env sigma f =
+let is_template_polymorphic_ind env sigma f =
   match EConstr.kind sigma f with
   | Ind (ind, u) ->
     if not (EConstr.EInstance.is_empty u) then false
diff --git a/engine/termops.mli b/engine/termops.mli
index 1054fbbc5e..07c9541f25 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -282,7 +282,7 @@ val is_global : Evd.evar_map -> GlobRef.t -> constr -> bool
 
 val isGlobalRef : Evd.evar_map -> constr -> bool
 
-val is_template_polymorphic : env -> Evd.evar_map -> constr -> bool
+val is_template_polymorphic_ind : env -> Evd.evar_map -> constr -> bool
 
 val is_Prop : Evd.evar_map -> constr -> bool
 val is_Set : Evd.evar_map -> constr -> bool
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index dd38ec6f64..96213af9c6 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -83,7 +83,7 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false)
   (** Refresh the types of evars under template polymorphic references *)
   let rec refresh_term_evars ~onevars ~top t =
     match EConstr.kind !evdref t with
-    | App (f, args) when is_template_polymorphic env !evdref f ->
+    | App (f, args) when Termops.is_template_polymorphic_ind env !evdref f ->
       let pos = get_polymorphic_positions !evdref f in
         refresh_polymorphic_positions args pos; t
     | App (f, args) when top && isEvar !evdref f -> 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 55817f1b76..756e2d4bc9 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -691,7 +691,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
     let sigma, resj =
       match EConstr.kind sigma resj.uj_val with
       | App (f,args) ->
-          if is_template_polymorphic !!env sigma f then
+          if Termops.is_template_polymorphic_ind !!env sigma f then
 	    (* Special case for inductive type applications that must be 
 	       refreshed right away. *)
             let c = mkApp (f, args) in
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 7e43c5e41d..62ad296ecb 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -130,7 +130,7 @@ let retype ?(polyprop=true) sigma =
          subst1 b (type_of (push_rel (LocalDef (name,b,c1)) env) c2)
     | Fix ((_,i),(_,tys,_)) -> tys.(i)
     | CoFix (i,(_,tys,_)) -> tys.(i)
-    | App(f,args) when is_template_polymorphic env sigma f ->
+    | App(f,args) when Termops.is_template_polymorphic_ind env sigma f ->
 	let t = type_of_global_reference_knowing_parameters env f args in
         strip_outer_cast sigma (subst_type env sigma t (Array.to_list args))
     | App(f,args) ->
@@ -156,7 +156,7 @@ let retype ?(polyprop=true) sigma =
       let dom = sort_of env t in
       let rang = sort_of (push_rel (LocalAssum (name,t)) env) c2 in
       Typeops.sort_of_product env dom rang
-    | App(f,args) when is_template_polymorphic env sigma f ->
+    | App(f,args) when Termops.is_template_polymorphic_ind env sigma f ->
       let t = type_of_global_reference_knowing_parameters env f args in
         sort_of_atomic_type env sigma t args
     | App(f,args) -> sort_of_atomic_type env sigma (type_of env f) args
@@ -190,14 +190,14 @@ let get_sort_family_of ?(truncation_style=false) ?(polyprop=true) env sigma t =
 	let s2 = sort_family_of (push_rel (LocalAssum (name,t)) env) c2 in
 	if not (is_impredicative_set env) &&
 	   s2 == InSet && sort_family_of env t == InType then InType else s2
-    | App(f,args) when is_template_polymorphic env sigma f ->
+    | App(f,args) when Termops.is_template_polymorphic_ind env sigma f ->
         if truncation_style then InType else
 	let t = type_of_global_reference_knowing_parameters env f args in
         Sorts.family (sort_of_atomic_type env sigma t args)
     | App(f,args) ->
 	Sorts.family (sort_of_atomic_type env sigma (type_of env f) args)
     | Lambda _ | Fix _ | Construct _ -> retype_error NotAType
-    | Ind _ when truncation_style && is_template_polymorphic env sigma t -> InType
+    | Ind _ when truncation_style && Termops.is_template_polymorphic_ind env sigma t -> InType
     | _ -> 
       Sorts.family (decomp_sort env sigma (type_of env t))
   in sort_family_of env t
diff --git a/proofs/logic.ml b/proofs/logic.ml
index b8612cd2c0..4d5711c195 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -384,7 +384,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
 
       | App (f,l) ->
 	let (acc',hdty,sigma,applicand) =
-	  if is_template_polymorphic env sigma (EConstr.of_constr f) then
+          if Termops.is_template_polymorphic_ind env sigma (EConstr.of_constr f) then
 	    let ty = 
 	      (* Template polymorphism of definitions and inductive types *)
 	      let firstmeta = Array.findi (fun i x -> occur_meta sigma (EConstr.of_constr x)) l in
@@ -447,7 +447,7 @@ and mk_hdgoals sigma goal goalacc trm =
 
     | App (f,l) ->
 	let (acc',hdty,sigma,applicand) =
-	  if is_template_polymorphic env sigma (EConstr.of_constr f)
+          if Termops.is_template_polymorphic_ind env sigma (EConstr.of_constr f)
 	  then
 	    let l' = meta_free_prefix sigma l in
 	   (goalacc,EConstr.Unsafe.to_constr (type_of_global_reference_knowing_parameters env sigma (EConstr.of_constr f) l'),sigma,f)