From cd902906499c85cf8af69ecb44f4960750de2771 Mon Sep 17 00:00:00 2001 From: sacerdot Date: Tue, 6 Apr 2004 19:52:03 +0000 Subject: 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 --- contrib/xml/cic2acic.ml | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/contrib/xml/cic2acic.ml b/contrib/xml/cic2acic.ml index 22e9670d5..4a7c0c8ad 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) -- cgit v1.2.3