diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-12-15 19:09:15 +0100 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-12-23 19:50:55 +0100 |
commit | 21750c40ee3f7ef3103121db68aef4339dceba40 (patch) | |
tree | 0d431861ae07801be81224e6123f151a24c84d41 /plugins/funind | |
parent | dea75d74c222c25f6aa6c38506ac7a51b339e9c6 (diff) |
[api] Also deprecate constructors of Decl_kinds.
Unfortunately OCaml doesn't deprecate the constructors of a type when
the type alias is deprecated.
In this case it means that we don't get rid of the kernel dependency
unless we deprecate the constructors too.
Diffstat (limited to 'plugins/funind')
-rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 6 | ||||
-rw-r--r-- | plugins/funind/merge.ml | 8 |
2 files changed, 7 insertions, 7 deletions
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 97066e531..b4e17c5d1 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1498,7 +1498,7 @@ let do_build_inductive try with_full_print (Flags.silently (ComInductive.do_mutual_inductive rel_inds (Flags.is_universe_polymorphism ()) false false)) - Decl_kinds.Finite + Declarations.Finite with | UserError(s,msg) as e -> let _time3 = System.get_time () in @@ -1509,7 +1509,7 @@ let do_build_inductive in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac Vernacexpr.(VernacExpr(VernacInductive(GlobalNonCumulativity,false,Decl_kinds.Finite,repacked_rel_inds))) + Ppvernac.pr_vernac Vernacexpr.(VernacExpr(VernacInductive(GlobalNonCumulativity,false,Declarations.Finite,repacked_rel_inds))) ++ fnl () ++ msg in @@ -1524,7 +1524,7 @@ let do_build_inductive in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac Vernacexpr.(VernacExpr(VernacInductive(GlobalNonCumulativity,false,Decl_kinds.Finite,repacked_rel_inds))) + Ppvernac.pr_vernac Vernacexpr.(VernacExpr(VernacInductive(GlobalNonCumulativity,false,Declarations.Finite,repacked_rel_inds))) ++ fnl () ++ CErrors.print reraise in diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 9fcb35f89..8f5d3f22f 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -20,10 +20,10 @@ open Names open Term open Constr open Vars -open Declarations open Glob_term open Glob_termops open Decl_kinds +open Declarations open Context.Rel.Declaration module RelDecl = Context.Rel.Declaration @@ -353,8 +353,8 @@ let ind2name = Id.of_string "__ind2" be co-inductive, and for the moment they must not be mutual either. *) let verify_inds mib1 mib2 = - if mib1.mind_finite == Decl_kinds.CoFinite then error "First argument is coinductive"; - if mib2.mind_finite == Decl_kinds.CoFinite then error "Second argument is coinductive"; + if mib1.mind_finite == CoFinite then error "First argument is coinductive"; + if mib2.mind_finite == CoFinite then error "Second argument is coinductive"; if not (Int.equal mib1.mind_ntypes 1) then error "First argument is mutual"; if not (Int.equal mib2.mind_ntypes 1) then error "Second argument is mutual"; () @@ -891,7 +891,7 @@ let merge_inductive (ind1: inductive) (ind2: inductive) (* Declare inductive *) let indl,_,_ = ComInductive.extract_mutual_inductive_declaration_components [(indexpr,[])] in let mie,pl,impls = ComInductive.interp_mutual_inductive indl [] - false (* non-cumulative *) false (*FIXMEnon-poly *) false (* means not private *) Decl_kinds.Finite (* means: not coinductive *) in + false (* non-cumulative *) false (*FIXMEnon-poly *) false (* means not private *) Finite (* means: not coinductive *) in (* Declare the mutual inductive block with its associated schemes *) ignore (ComInductive.declare_mutual_inductive_with_eliminations mie pl impls) |