Bug fixed: conjectures were printed in the wrong order.

diff --git a/helm/gTopLevel/cic2Xml.ml b/helm/gTopLevel/cic2Xml.ml
index fa7d729d98a74c104950b026d4414c1ce4c23f6d..57d4fc7e4e086386d05919cc9c349e6248b11cac 100644 (file)
--- a/helm/gTopLevel/cic2Xml.ml
+++ b/helm/gTopLevel/cic2Xml.ml
@@ -295,7 +295,7 @@ let print_object uri ~ids_to_inner_sorts =
                         (print_term ids_to_inner_sorts t)
                     >]
                 >])
-              [<>] (List.rev conjectures) ;
+              [<>] conjectures ;
              X.xml_nempty "body" [] (print_term ids_to_inner_sorts bo) >]
         in
         let xml_for_current_proof_type =