Inner types are now reduced and arrows are created when

products have dummy binders.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1050 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 13 insertions, 6 deletions

diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index 3e52f311d..f1cdd1019 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -236,11 +236,14 @@ let print_term inner_types l env csr =
   in
 
   let inner_type_display env term =
-   let type_of_term = R.get_type_of env (Evd.empty) term in
-   match R.get_sort_of env (Evd.empty) type_of_term with
-      T.Prop T.Null -> InnerProp type_of_term
-    | T.Prop _      -> InnerSet
-    | _             -> InnerType
+   let type_of_term =
+    Reduction.nf_betaiota env (Evd.empty)
+     (R.get_type_of env (Evd.empty) term)
+   in
+    match R.get_sort_of env (Evd.empty) type_of_term with
+       T.Prop T.Null -> InnerProp type_of_term
+     | T.Prop _      -> InnerSet
+     | _             -> InnerType
   in
 
 (*WHICH FORCE FUNCTION DEPENDS ON THE ORDERING YOU WANT
@@ -322,7 +325,11 @@ let print_term inner_types l env csr =
        X.xml_nempty "PROD" ["id", next_id]
 (force
         [< X.xml_nempty "source" [] (term_display idradix false l env t1) ;
-           X.xml_nempty "target" ["binder",(N.string_of_id nid')]
+           X.xml_nempty "target"
+            (if idradix = `T &&
+                T.noccurn 1 t2
+             then []
+             else ["binder",(N.string_of_id nid')])
             (term_display idradix false
              ((N.Name nid')::l)
              (E.push_rel_assum (N.Name nid', t1) env)