aboutsummaryrefslogtreecommitdiff
path: root/kernel/constr.ml
diff options
context:
space:
mode:
authorGaetan Gilbert2017-04-25 14:31:15 +0200
committerGaetan Gilbert2017-04-27 21:42:01 +0200
commit87910d7be9bd50de4db80f70c6e287c7c7994460 (patch)
treeff0c9daa7ff73f0eb19e8b62ea6f689b154f314b /kernel/constr.ml
parent5eb09af1e3686d6ac518b9eafe7cfcebd2b16375 (diff)
Fix 4.04 warnings
Diffstat (limited to 'kernel/constr.ml')
-rw-r--r--kernel/constr.ml22
1 files changed, 0 insertions, 22 deletions
diff --git a/kernel/constr.ml b/kernel/constr.ml
index 5a7561bf50..71efe90322 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -978,28 +978,6 @@ module Hcaseinfo = Hashcons.Make(CaseinfoHash)
let case_info_hash = CaseinfoHash.hash
-module Hsorts =
- Hashcons.Make(
- struct
- open Sorts
-
- type t = Sorts.t
- type u = universe -> universe
- let hashcons huniv = function
- Prop c -> Prop c
- | Type u -> Type (huniv u)
- let eq s1 s2 =
- s1 == s2 ||
- match (s1,s2) with
- (Prop c1, Prop c2) -> c1 == c2
- | (Type u1, Type u2) -> u1 == u2
- |_ -> false
- let hash = function
- | Prop Null -> 0 | Prop Pos -> 1
- | Type u -> 2 + Universe.hash u
- end)
-
-(* let hcons_sorts = Hashcons.simple_hcons Hsorts.generate hcons_univ *)
let hcons_caseinfo = Hashcons.simple_hcons Hcaseinfo.generate Hcaseinfo.hcons hcons_ind
let hcons =