From 001ff72b2c17fb7b2fcaefa2555c115f0d909a03 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 28 Oct 2013 14:08:46 +0100 Subject: Initial work on reintroducing old-style polymorphism for compatibility (the stdlib does not compile entirely). --- plugins/xml/xmlcommand.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/xml') 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 -- cgit v1.2.3