Fix interface for template polymorphism, cleaning up code in all typing algorithms.

5 files changed, 12 insertions, 14 deletions

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 0ef8d3f3c2..3f14de2828 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -549,15 +549,12 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref lvar t =
       match evar_kind_of_term !evdref resj.uj_val with
       | App (f,args) ->
         let f = whd_evar !evdref f in
-          begin match kind_of_term f with
-          | Ind _ | Const _
-	      when isInd f || has_polymorphic_type (fst (destConst f))
-		->
+          if is_template_polymorphic env f then
 	    let sigma = !evdref in
 	    let c = mkApp (f,Array.map (whd_evar sigma) args) in
 	    let t = Retyping.get_type_of env sigma c in
 	      make_judge c (* use this for keeping evars: resj.uj_val *) t
-          | _ -> resj end
+	  else resj
       | _ -> resj 
     in
       inh_conv_coerce_to_tycon loc env evdref resj tycon
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 9aecd2d1f0..4ba6b01dc8 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -124,7 +124,7 @@ let retype ?(polyprop=true) sigma =
          subst1 b (type_of (push_rel (name,Some b,c1) env) c2)
     | Fix ((_,i),(_,tys,_)) -> tys.(i)
     | CoFix (i,(_,tys,_)) -> tys.(i)
-    | App(f,args) when isGlobalRef f ->
+    | App(f,args) when is_template_polymorphic env f ->
 	let t = type_of_global_reference_knowing_parameters env f args in
         strip_outer_cast (subst_type env sigma t (Array.to_list args))
     | App(f,args) ->
@@ -154,7 +154,7 @@ let retype ?(polyprop=true) sigma =
 	  | Prop Pos, (Type u2) -> Type (Univ.sup Univ.type0_univ u2)
 	  | Prop Null, (Type _ as s) -> s
 	  | Type u1, Type u2 -> Type (Univ.sup u1 u2))
-    | App(f,args) when isGlobalRef f ->
+    | App(f,args) when is_template_polymorphic env 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
@@ -170,7 +170,7 @@ let retype ?(polyprop=true) sigma =
 	let s2 = sort_family_of (push_rel (name,None,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 isGlobalRef f ->
+    | App(f,args) when is_template_polymorphic env f ->
 	let t = type_of_global_reference_knowing_parameters env f args in
         family_of_sort (sort_of_atomic_type env sigma t args)
     | App(f,args) ->
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index ee7538b225..27c1d252d3 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -868,9 +868,10 @@ let isGlobalRef c =
   | Const _ | Ind _ | Construct _ | Var _ -> true
   | _ -> false
 
-let has_polymorphic_type c =
-  match (Global.lookup_constant c).Declarations.const_type with
-  | Declarations.TemplateArity _ -> true
+let is_template_polymorphic env f =
+  match kind_of_term f with
+  | Ind ind -> Environ.template_polymorphic_ind ind env
+  | Const c -> Environ.template_polymorphic_constant c env
   | _ -> false
 
 let base_sort_cmp pb s0 s1 =
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index eec4a9b9d8..6ef3d11da7 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -271,7 +271,7 @@ val is_section_variable : Id.t -> bool
 
 val isGlobalRef : constr -> bool
 
-val has_polymorphic_type : constant -> bool
+val is_template_polymorphic : env -> constr -> bool
 
 (** Combinators on judgments *)
 
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index cc473bd86e..339ca19fb0 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -207,12 +207,12 @@ let rec execute env evdref cstr =
         let jl = execute_array env evdref args in
 	let j =
 	  match kind_of_term f with
-	    | Ind ind ->
+	    | Ind ind when Environ.template_polymorphic_ind ind env ->
 		(* Sort-polymorphism of inductive types *)
 		make_judge f
 		  (inductive_type_knowing_parameters env ind
 		    (Evarutil.jv_nf_evar !evdref jl))
-	    | Const cst ->
+	    | Const cst when Environ.template_polymorphic_constant cst env ->
 		(* Sort-polymorphism of inductive types *)
 		make_judge f
 		  (constant_type_knowing_parameters env cst