From 13928db651b2edb15bd3a251c49428edb42a3ba1 Mon Sep 17 00:00:00 2001
From: sacerdot
Date: Wed, 31 Mar 2004 09:35:47 +0000
Subject: Fake dependent types in constructors of inductive types are now
 preserved. The idea is:  1. constructors are always declare by hand by the
 user ==> binders always     have a meaning.  2. the binders are fundamental
 for record fields, even if the dependent     product is really non-dependent.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5621 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/xml/cic2acic.ml | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/contrib/xml/cic2acic.ml b/contrib/xml/cic2acic.ml
index 14c2521cc6..4a7c3823d6 100644
--- a/contrib/xml/cic2acic.ml
+++ b/contrib/xml/cic2acic.ml
@@ -354,8 +354,8 @@ let fresh_id seed ids_to_terms constr_to_ids ids_to_father_ids =
 let source_id_of_id id = "#source#" ^ id;;
 
 let acic_of_cic_context' computeinnertypes seed ids_to_terms constr_to_ids
- ids_to_father_ids ids_to_inner_sorts ids_to_inner_types pvars env idrefs
- evar_map t expectedty
+ ids_to_father_ids ids_to_inner_sorts ids_to_inner_types
+ pvars ?(fake_dependent_products=false) env idrefs evar_map t expectedty
 =
  let module D = DoubleTypeInference in
  let module E = Environ in
@@ -557,7 +557,7 @@ print_endline "PASSATO" ; flush stdout ;
                match n with
                   N.Anonymous -> N.Anonymous
                 | _ ->
-                  if T.noccurn 1 t then
+                  if not fake_dependent_products && T.noccurn 1 t then
                    N.Anonymous
                   else
                    N.Name
@@ -942,7 +942,8 @@ let acic_object_of_cic_object pvars sigma obj =
             List.map
              (function (name,ty) ->
                (name,
-                 acic_term_of_cic_term_context' env' idrefs Evd.empty ty None)
+                 acic_term_of_cic_term_context' ~fake_dependent_products:true
+                  env' idrefs Evd.empty ty None)
              ) cons
            in
             (id,name,inductive,acic_term_of_cic_term' ty None,acons)
-- 
cgit v1.2.3