From 2c64a5ecd3b8916e9446324dc4c2acdba63a8ca6 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sun, 4 Nov 2007 19:17:22 +0000 Subject: [PATCH] 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. --- .../components/cic_exportation/cicExportation.ml | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/helm/software/components/cic_exportation/cicExportation.ml b/helm/software/components/cic_exportation/cicExportation.ml index 37eff255b..71de7716a 100644 --- a/helm/software/components/cic_exportation/cicExportation.ml +++ b/helm/software/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 = -- 2.39.2