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 --- tactics/class_tactics.ml | 2 +- tactics/equality.ml | 2 +- tactics/inv.ml | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) (limited to 'tactics') diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 773fc1520..9c5fdcd1c 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -477,7 +477,7 @@ let is_Prop env sigma concl = match EConstr.kind sigma ty with | Sort s -> begin match ESorts.kind sigma s with - | Prop Null -> true + | Prop -> true | _ -> false end | _ -> false diff --git a/tactics/equality.ml b/tactics/equality.ml index 91c577405..0e3921570 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -942,7 +942,7 @@ let rec build_discriminator env sigma true_0 false_0 dirn c = function let (cnum_nlams,cnum_env,kont) = descend_then env sigma c cnum in let newc = mkRel(cnum_nlams-argnum) in let subval = build_discriminator cnum_env sigma true_0 false_0 dirn newc l in - kont sigma subval (false_0,mkSort (Prop Null)) + kont sigma subval (false_0,mkProp) (* Note: discrimination could be more clever: if some elimination is not allowed because of a large impredicative constructor in the diff --git a/tactics/inv.ml b/tactics/inv.ml index 755494c2d..e467eacd9 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -495,7 +495,7 @@ let raw_inversion inv_kind id status names = (* Error messages of the inversion tactics *) let wrap_inv_error id = function (e, info) -> match e with | Indrec.RecursionSchemeError - (Indrec.NotAllowedCaseAnalysis (_,(Type _ | Prop Pos as k),i)) -> + (Indrec.NotAllowedCaseAnalysis (_,(Type _ | Set as k),i)) -> Proofview.tclENV >>= fun env -> Proofview.tclEVARMAP >>= fun sigma -> tclZEROMSG ( -- cgit v1.2.3