diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/declare.ml | 2 | ||||
| -rw-r--r-- | interp/dumpglob.ml | 3 | ||||
| -rw-r--r-- | interp/implicit_quantifiers.mli | 4 |
3 files changed, 4 insertions, 5 deletions
diff --git a/interp/declare.ml b/interp/declare.ml index 5be07e09ec..d1b79ffcdd 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 0197cf9ae2..d7962e29a6 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" diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli index f7c36c4e5f..bfe73160bb 100644 --- a/interp/implicit_quantifiers.mli +++ b/interp/implicit_quantifiers.mli @@ -38,10 +38,10 @@ val make_fresh : Id.Set.t -> Environ.env -> Id.t -> Id.t val implicits_of_glob_constr : ?with_products:bool -> Glob_term.glob_constr -> Impargs.manual_implicits val combine_params_freevar : - Id.Set.t -> (global_reference * bool) option * Context.Rel.Declaration.t -> + Id.Set.t -> global_reference option * Context.Rel.Declaration.t -> Constrexpr.constr_expr * Id.Set.t val implicit_application : Id.Set.t -> ?allow_partial:bool -> - (Id.Set.t -> (global_reference * bool) option * Context.Rel.Declaration.t -> + (Id.Set.t -> global_reference option * Context.Rel.Declaration.t -> Constrexpr.constr_expr * Id.Set.t) -> constr_expr -> constr_expr * Id.Set.t |