From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sun, 4 Nov 2007 19:17:22 +0000 (+0000)
Subject: The type parameters in an inductive type declaration should be the left ones,
X-Git-Tag: 0.4.95@7852~56
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=c9bd61016355fe5ff3440709aa4fb18fe36219fe

The type parameters in an inductive type declaration should be the left ones,
that are replicated in every constructor. They used to be listed n times for
an inductive type with n constructors.
---

diff --git a/components/cic_exportation/cicExportation.ml b/components/cic_exportation/cicExportation.ml
index 37eff255b..71de7716a 100644
--- a/components/cic_exportation/cicExportation.ml
+++ b/components/cic_exportation/cicExportation.ml
@@ -374,7 +374,8 @@ let ppty current_module_name =
 (* ppinductiveType (typename, inductive, arity, cons)                       *)
 (* pretty-prints a single inductive definition                              *)
 (* (typename, inductive, arity, cons)                                       *)
-let ppinductiveType current_module_name (typename, inductive, arity, cons) =
+let ppinductiveType current_module_name nparams (typename, inductive, arity, cons)
+=
  match analyze_type [] arity with
     `Sort Cic.Prop -> ""
   | `Statement
@@ -385,10 +386,10 @@ let ppinductiveType current_module_name (typename, inductive, arity, cons) =
     else (
      let abstr,scons =
       List.fold_right
-       (fun (id,ty) (abstr,i) ->
+       (fun (id,ty) (_abstr,i) -> (* we should verify _abstr = abstr' *)
           let abstr',sargs = ppty current_module_name [] ty in
           let sargs = String.concat " * " sargs in
-           abstr'@abstr,
+           abstr',
            String.capitalize id ^
             (if sargs = "" then "" else " of " ^ sargs) ^
             (if i = "" then "" else "\n | ") ^ i)
@@ -467,7 +468,7 @@ let ppobj current_module_name obj =
           pp ~metasenv:conjectures ty [] 
    | C.InductiveDefinition (l, params, nparams, _) ->
       List.fold_right
-       (fun x i -> ppinductiveType current_module_name x ^ i) l ""
+       (fun x i -> ppinductiveType current_module_name nparams x ^ i) l ""
 ;;
 
 let ppobj current_module_name obj =