Initial work on reintroducing old-style polymorphism for compatibility (the stdlib does not compile entirely).

8 files changed, 21 insertions, 22 deletions

diff --git a/plugins/Derive/g_derive.ml4 b/plugins/Derive/g_derive.ml4
index 9137c3d28..c7db26fb8 100644
--- a/plugins/Derive/g_derive.ml4
+++ b/plugins/Derive/g_derive.ml4
@@ -8,7 +8,7 @@
 
 (*i camlp4deps: "grammar/grammar.cma"  i*)
 
-let classify_derive_command _ = Vernacexpr.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]),VtLater)
+let classify_derive_command _ = Vernacexpr.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[], false),VtLater)
 
 VERNAC COMMAND EXTEND Derive CLASSIFIED BY classify_derive_command
 | [ "Derive" ident(f) "From" constr(init) "Upto" constr(r) "As" ident(lemma) ] ->
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 74de31368..791294902 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -131,7 +131,7 @@ end
 exception Impossible
 
 let check_arity env cb =
-  let t = cb.const_type in
+  let t = Typeops.type_of_constant_type env cb.const_type in
   if Reduction.is_arity env t then raise Impossible
 
 let check_fix env cb i =
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 5b79f6d78..f7b677a1e 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -202,17 +202,15 @@ let parse_ind_args si args relmax =
 let oib_equal o1 o2 =
   Id.equal o1.mind_typename o2.mind_typename &&
   List.equal eq_rel_declaration o1.mind_arity_ctxt o2.mind_arity_ctxt &&
-  begin match o1.mind_arity, o2.mind_arity with
-  (* | Monomorphic {mind_user_arity=c1; mind_sort=s1}, *)
-  (*   Monomorphic {mind_user_arity=c2; mind_sort=s2} -> *)
-  (*     eq_constr c1 c2 && Sorts.equal s1 s2 *)
-  (* | ma1, ma2 -> Pervasives.(=) ma1 ma2 (\** FIXME: this one is surely wrong *\) end && *)
-  (*   Array.equal Id.equal o1.mind_consnames o2.mind_consnames *)
-  | {mind_user_arity=c1; mind_sort=s1},
-    {mind_user_arity=c2; mind_sort=s2} ->
-      eq_constr c1 c2 && Sorts.equal s1 s2
-  end &&
-  Array.equal Id.equal o1.mind_consnames o2.mind_consnames
+    begin
+      match o1.mind_arity, o2.mind_arity with
+      | RegularArity {mind_user_arity=c1; mind_sort=s1}, RegularArity {mind_user_arity=c2; mind_sort=s2} ->
+	eq_constr c1 c2 && Sorts.equal s1 s2
+      | {mind_user_arity=c1; mind_sort=s1},
+	{mind_user_arity=c2; mind_sort=s2} ->
+	eq_constr c1 c2 && Sorts.equal s1 s2
+    end &&
+    Array.equal Id.equal o1.mind_consnames o2.mind_consnames
 
 let mib_equal m1 m2 =
   Array.equal oib_equal m1.mind_packets m1.mind_packets &&
@@ -525,7 +523,8 @@ and mlt_env env r = match r with
 	   | _ -> None
        with Not_found ->
 	 let cb = Environ.lookup_constant kn env in
-	 let typ = cb.const_type (* FIXME not sure if we should instantiate univs here *) in
+	 let typ = Typeops.type_of_constant_type env cb.const_type
+ (* FIXME not sure if we should instantiate univs here *) in
 	 match cb.const_body with
 	   | Undef _ | OpaqueDef _ -> None
 	   | Def l_body ->
@@ -553,7 +552,7 @@ let record_constant_type env kn opt_typ =
     lookup_type kn
   with Not_found ->
     let typ = match opt_typ with
-      | None -> (lookup_constant kn env).const_type
+      | None -> Typeops.type_of_constant_type env (lookup_constant kn env).const_type
       | Some typ -> typ
     in let mlt = extract_type env [] 1 typ []
     in let schema = (type_maxvar mlt, mlt)
@@ -976,7 +975,7 @@ let extract_fixpoint env vkn (fi,ti,ci) =
 
 let extract_constant env kn cb =
   let r = ConstRef kn in
-  let typ = cb.const_type in
+  let typ = Global.type_of_global_unsafe r in
   let warn_info () = if not (is_custom r) then add_info_axiom r in
   let warn_log () = if not (constant_has_body cb) then add_log_axiom r
   in
@@ -1023,7 +1022,7 @@ let extract_constant env kn cb =
 
 let extract_constant_spec env kn cb =
   let r = ConstRef kn in
-  let typ = cb.const_type in
+  let typ = Global.type_of_global_unsafe r in
   match flag_of_type env typ with
     | (Logic, TypeScheme) -> Stype (r, [], Some (Tdummy Ktype))
     | (Logic, Default) -> Sval (r, Tdummy Kother)
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 133f4ada9..c48873c80 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -816,7 +816,7 @@ let extract_constant_inline inline r ids s =
   match g with
     | ConstRef kn ->
 	let env = Global.env () in
-	let typ = (Environ.lookup_constant kn env).const_type in
+	let typ = Global.type_of_global_unsafe (ConstRef kn) in
 	let typ = Reduction.whd_betadeltaiota env typ in
 	if Reduction.is_arity env typ
 	  then begin
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index a3af23dcd..f0c7b5a7f 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -964,7 +964,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
   let eq_rhs = nf_betaiotazeta (mkApp(compose_lam params f_body_with_params_and_other_fun,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i)))) in
 (*   observe (str "eq_rhs " ++  pr_lconstr eq_rhs); *)
   let type_ctxt,type_of_f = decompose_prod_n_assum (nb_params + nb_args)
-    ((*FIXME*)f_def.const_type) in
+    (Typeops.type_of_constant_type (Global.env ()) (*FIXME*)f_def.const_type) in
   let eqn = mkApp(Lazy.force eq,[|type_of_f;eq_lhs;eq_rhs|]) in
   let lemma_type = it_mkProd_or_LetIn eqn type_ctxt in
   let f_id = Label.to_id (con_label (fst (destConst f))) in
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index d6ad5575b..49f833590 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -771,7 +771,7 @@ let make_graph (f_ref:global_reference) =
 	   with_full_print (fun () ->
 		(Constrextern.extern_constr false env body,
 		 Constrextern.extern_type false env
-                   ((*FIXNE*) c_body.const_type)
+                   ((*FIXNE*) Typeops.type_of_constant_type env c_body.const_type)
 		)
 	     )
 	     ()
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index d0497f6f6..2e524a35f 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -139,7 +139,7 @@ let showind (id:Id.t) =
     print_string (string_of_name nm^":");
     prconstr tp; print_string "\n")
     ib1.mind_arity_ctxt;
-    Printf.printf "arity :"; prconstr ib1.mind_arity.mind_user_arity;
+    Printf.printf "arity :"; prconstr (Inductiveops.type_of_inductive (Global.env ()) ind1);
   Array.iteri
     (fun i x -> Printf.printf"type constr %d :" i ; prconstr x)
     ib1.mind_user_lc
diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml
index 3d655920b..8f47859da 100644
--- a/plugins/xml/xmlcommand.ml
+++ b/plugins/xml/xmlcommand.ml
@@ -380,7 +380,7 @@ let print internal glob_ref kind xml_library_root =
        let val0 = Declareops.body_of_constant cb in
        let typ = cb.Declarations.const_type in
        let hyps = cb.Declarations.const_hyps in
-       let typ = (* Typeops.type_of_constant_type (Global.env()) *) typ in
+       let typ = Typeops.type_of_constant_type (Global.env()) typ in
         Cic2acic.Constant kn,mk_constant_obj id val0 typ variables hyps
     | Globnames.IndRef (kn,_) ->
        let mib = Global.lookup_mind kn in