diff options
| author | Arnaud Spiwack | 2014-09-03 11:40:27 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-09-04 10:25:54 +0200 |
| commit | b18b40878f071b6c7d67d1a2d031370f7a498d0b (patch) | |
| tree | 595398248a70dd2607c983c5dd3eb8913614b084 /interp | |
| parent | ac2fdfb222083faa9c3893194e020bed38555ddb (diff) | |
Print [Variant] types with the keyword [Variant].
Involves changing the [mind_finite] field in the kernel from a bool to the trivalued type [Decl_kinds.recursivity_kind]. This is why so many files are (unfortunately) affected. It would not be very surprising if some bug was introduced.
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/dumpglob.ml | 17 |
1 files changed, 13 insertions, 4 deletions
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index bf9d2c0b99..87c8cb04d9 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -111,10 +111,19 @@ let type_of_global_ref gr = | Globnames.IndRef ind -> let (mib,oib) = Inductive.lookup_mind_specif (Global.env ()) ind in if mib.Declarations.mind_record <> None then - if mib.Declarations.mind_finite then "rec" - else "corec" - else if mib.Declarations.mind_finite then "ind" - else "coind" + let open Decl_kinds in + begin match mib.Declarations.mind_finite with + | Finite -> "indrec" + | BiFinite -> "rec" + | CoFinite -> "corec" + end + else + let open Decl_kinds in + begin match mib.Declarations.mind_finite with + | Finite -> "ind" + | BiFinite -> "variant" + | CoFinite -> "coind" + end | Globnames.ConstructRef _ -> "constr" let remove_sections dir = |