From af0a04b8e16c2554e0c747da6d625799b332f5fe Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Wed, 11 Oct 2017 19:41:23 +0200 Subject: Remove Sorts.contents --- plugins/cc/ccalgo.ml | 4 ++-- plugins/ltac/taccoerce.ml | 9 +++++---- 2 files changed, 7 insertions(+), 6 deletions(-) (limited to 'plugins') diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index 4c6156a38..4a691e442 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -130,8 +130,8 @@ type cinfo= ci_nhyps: int} (* # projectable args *) let family_eq f1 f2 = match f1, f2 with - | Prop Pos, Prop Pos - | Prop Null, Prop Null + | Set, Set + | Prop, Prop | Type _, Type _ -> true | _ -> false diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index cc9c2046d..84baea964 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -199,11 +199,12 @@ let id_of_name = function let basename = Nametab.basename_of_global ref in basename | Sort s -> - begin + begin match ESorts.kind sigma s with - | Sorts.Prop _ -> Label.to_id (Label.make "Prop") - | Sorts.Type _ -> Label.to_id (Label.make "Type") - end + | Sorts.Prop -> Label.to_id (Label.make "Prop") + | Sorts.Set -> Label.to_id (Label.make "Set") + | Sorts.Type _ -> Label.to_id (Label.make "Type") + end | _ -> fail() -- cgit v1.2.3