diff options
| author | Emilio Jesus Gallego Arias | 2017-12-15 19:09:15 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-12-23 19:50:55 +0100 |
| commit | 21750c40ee3f7ef3103121db68aef4339dceba40 (patch) | |
| tree | 0d431861ae07801be81224e6123f151a24c84d41 /tactics | |
| 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 'tactics')
| -rw-r--r-- | tactics/hipattern.ml | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index 2c8ca19722..a3a3e0a9e9 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -48,7 +48,7 @@ let match_with_non_recursive_type sigma t = let (hdapp,args) = decompose_app sigma t in (match EConstr.kind sigma hdapp with | Ind (ind,u) -> - if (Global.lookup_mind (fst ind)).mind_finite == Decl_kinds.CoFinite then + if (Global.lookup_mind (fst ind)).mind_finite == CoFinite then Some (hdapp,args) else None diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 508040ec18..4ee0a8a7b2 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1492,7 +1492,7 @@ let simplest_ecase c = general_case_analysis true None (c,NoBindings) exception IsNonrec -let is_nonrec mind = (Global.lookup_mind (fst mind)).mind_finite == Decl_kinds.BiFinite +let is_nonrec mind = (Global.lookup_mind (fst mind)).mind_finite == Declarations.BiFinite let find_ind_eliminator ind s gl = let gr = lookup_eliminator ind s in |