From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Wed, 2 Feb 2005 14:11:41 +0000 (+0000)
Subject: added inductive_name field to inductive definitions so that this
X-Git-Tag: V_0_1_0~64
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2f15a81dcd6e5ada3f1b4fa6300e9a1347c8d12c;p=helm.git

added inductive_name field to inductive definitions so that this
information is not lost at content level
---

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