Fake dependent products in inductive definition types are no longer replaced

with non dependent products. The main motivation is that inductive definition
parameters often occurs as non-dependent products in the product types,
but the binder names are still necessary to render the definition in the
usual Coq way.


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

1 files changed, 6 insertions, 2 deletions

diff --git a/contrib/xml/cic2acic.ml b/contrib/xml/cic2acic.ml
index 22e9670d50..4a7c0c8adf 100644
--- a/contrib/xml/cic2acic.ml
+++ b/contrib/xml/cic2acic.ml
@@ -846,7 +846,8 @@ let acic_object_of_cic_object pvars sigma obj =
 (*CSC: either in the environment or in the named context (in the case *)
 (*CSC: of variables. Is this a problem?                               *)
   let env = Global.env () in
-  let acic_term_of_cic_term' = acic_term_of_cic_term_context' env [] sigma in
+  let acic_term_of_cic_term' ?fake_dependent_products =
+   acic_term_of_cic_term_context' ?fake_dependent_products env [] sigma in
 (*CSC: the fresh_id is not stored anywhere. This _MUST_ be fixed using *)
 (*CSC: a modified version of the already existent fresh_id function    *)
   let fresh_id () =
@@ -943,7 +944,10 @@ let acic_object_of_cic_object pvars sigma obj =
                   env' idrefs Evd.empty ty None)
              ) cons
            in
-            (id,name,inductive,acic_term_of_cic_term' ty None,acons)
+            let aty =
+             acic_term_of_cic_term' ~fake_dependent_products:true ty None
+            in
+             (id,name,inductive,aty,acons)
          ) (List.rev idrefs) tys
        in
        A.AInductiveDefinition (fresh_id (),atys,params,paramsno)