Properly reinstate old-style polymorphism in the kernel and pretyping/retyping.

TODO fix interface on knowing_parameters to avoid useless array allocations.

4 files changed, 30 insertions, 13 deletions

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 7777de514..0ef8d3f3c 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -545,6 +545,21 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref lvar t =
 	      	resj [hj]
     in
     let resj = apply_rec env 1 fj candargs args in
+    let resj =
+      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))
+		->
+	    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
+      | _ -> resj 
+    in
       inh_conv_coerce_to_tycon loc env evdref resj tycon
 
   | GLambda(loc,name,bk,c1,c2)      ->
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index ccb9420fd..9aecd2d1f 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -154,9 +154,9 @@ 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 -> *)
-    (* 	let t = type_of_global_reference_knowing_parameters env f args in *)
-    (*     sort_of_atomic_type env sigma t args *)
+    | App(f,args) when isGlobalRef 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
     | Lambda _ | Fix _ | Construct _ -> retype_error NotAType
     | _ -> decomp_sort env sigma (type_of env t)
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index b3fa53eee..ee7538b22 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -868,7 +868,10 @@ let isGlobalRef c =
   | Const _ | Ind _ | Construct _ | Var _ -> true
   | _ -> false
 
-let has_polymorphic_type c = (Global.lookup_constant c).Declarations.const_polymorphic
+let has_polymorphic_type c =
+  match (Global.lookup_constant c).Declarations.const_type with
+  | Declarations.TemplateArity _ -> true
+  | _ -> false
 
 let base_sort_cmp pb s0 s1 =
   match (s0,s1) with
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index f7379b4a0..dbd83bb42 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -734,21 +734,20 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
 	error_cannot_unify (fst curenvnb) sigma (cM,cN)
     else error_cannot_unify (fst curenvnb) sigma (cM,cN)
       in
-  let evd = sigma in
   let res = 
-    if occur_meta_or_undefined_evar evd m || occur_meta_or_undefined_evar evd n
+    if occur_meta_or_undefined_evar sigma m || occur_meta_or_undefined_evar sigma n
       || subterm_restriction conv_at_top flags then None
     else 
       let sigma, b = match flags.modulo_conv_on_closed_terms with
-      | Some convflags -> infer_conv ~pb:cv_pb ~ts:convflags env sigma m n
-      | _ -> constr_cmp cv_pb sigma flags m n in
+	| Some convflags -> infer_conv ~pb:cv_pb ~ts:convflags env sigma m n
+	| _ -> constr_cmp cv_pb sigma flags m n in
 	if b then Some sigma
 	else if (match flags.modulo_conv_on_closed_terms, flags.modulo_delta with
-            | Some (cv_id, cv_k), (dl_id, dl_k) ->
-                Id.Pred.subset dl_id cv_id && Cpred.subset dl_k cv_k
-            | None,(dl_id, dl_k) ->
-                Id.Pred.is_empty dl_id && Cpred.is_empty dl_k)
-      then error_cannot_unify env sigma (m, n) else None
+        | Some (cv_id, cv_k), (dl_id, dl_k) ->
+          Id.Pred.subset dl_id cv_id && Cpred.subset dl_k cv_k
+        | None,(dl_id, dl_k) ->
+          Id.Pred.is_empty dl_id && Cpred.is_empty dl_k)
+	then error_cannot_unify env sigma (m, n) else None
   in 
     match res with 
     | Some sigma -> sigma, ms, es