diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-12-27 10:19:29 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-12-27 10:19:29 +0100 |
| commit | f6857ce53ecf64b0086854495b4a8451f476d5b4 (patch) | |
| tree | 7c36a59b64fcd20b3666eca8de54b4fd33606cc1 /interp | |
| parent | 4969f9425cb0d5cd5bd735110886a0cbd2641588 (diff) | |
| parent | 21750c40ee3f7ef3103121db68aef4339dceba40 (diff) | |
Merge PR #6439: [api] Also deprecate constructors of Decl_kinds.
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/declare.ml | 2 | ||||
| -rw-r--r-- | interp/dumpglob.ml | 3 |
2 files changed, 2 insertions, 3 deletions
diff --git a/interp/declare.ml b/interp/declare.ml index 5be07e09e..d1b79ffcd 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -349,7 +349,7 @@ let dummy_one_inductive_entry mie = { let dummy_inductive_entry (_,m) = ([],{ mind_entry_params = []; mind_entry_record = None; - mind_entry_finite = Decl_kinds.BiFinite; + mind_entry_finite = Declarations.BiFinite; mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds; mind_entry_universes = Monomorphic_ind_entry Univ.ContextSet.empty; mind_entry_private = None; diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index 0197cf9ae..d7962e29a 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -68,6 +68,7 @@ let pause () = previous_state := !glob_output; glob_output := NoGlob let continue () = glob_output := !previous_state open Decl_kinds +open Declarations let type_of_logical_kind = function | IsDefinition def -> @@ -111,14 +112,12 @@ 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 - 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" |