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

TODO fix interface on knowing_parameters to avoid useless array allocations.

1 files changed, 15 insertions, 0 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)      ->