From 2f15a81dcd6e5ada3f1b4fa6300e9a1347c8d12c Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Wed, 2 Feb 2005 14:11:41 +0000 Subject: [PATCH] added inductive_name field to inductive definitions so that this information is not lost at content level --- helm/ocaml/cic_omdoc/cic2content.ml | 1 + helm/ocaml/cic_omdoc/content.ml | 1 + helm/ocaml/cic_omdoc/content.mli | 1 + 3 files changed, 3 insertions(+) diff --git a/helm/ocaml/cic_omdoc/cic2content.ml b/helm/ocaml/cic_omdoc/cic2content.ml index aaf451256..81f0683c6 100644 --- a/helm/ocaml/cic_omdoc/cic2content.ml +++ b/helm/ocaml/cic_omdoc/cic2content.ml @@ -955,6 +955,7 @@ and fun (_,n,b,ty,l) -> `Inductive { K.inductive_id = gen_id inductive_prefix seed; + K.inductive_name = n; K.inductive_kind = b; K.inductive_type = ty; K.inductive_constructors = build_constructors seed l diff --git a/helm/ocaml/cic_omdoc/content.ml b/helm/ocaml/cic_omdoc/content.ml index ee7b8488d..9687e53fc 100644 --- a/helm/ocaml/cic_omdoc/content.ml +++ b/helm/ocaml/cic_omdoc/content.ml @@ -62,6 +62,7 @@ type 'term definition = type 'term inductive = { inductive_id : id ; + inductive_name : string; inductive_kind : bool; inductive_type : 'term; inductive_constructors : 'term declaration list diff --git a/helm/ocaml/cic_omdoc/content.mli b/helm/ocaml/cic_omdoc/content.mli index dcaa5c7b5..9a38ea4be 100644 --- a/helm/ocaml/cic_omdoc/content.mli +++ b/helm/ocaml/cic_omdoc/content.mli @@ -53,6 +53,7 @@ type 'term definition = type 'term inductive = { inductive_id : id ; + inductive_name : string; inductive_kind : bool; inductive_type : 'term; inductive_constructors : 'term declaration list -- 2.39.2