From ae39925d64cc51663ab3f2ad397501b435bd0e5e Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 30 Oct 2018 15:04:06 +0100
Subject: 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.
---
 proofs/logic.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'proofs')

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)
-- 
cgit v1.2.3