aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
diff options
context:
space:
mode:
authorGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2017-10-11 19:41:23 +0200
committerGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-06-26 13:52:52 +0200
commitaf0a04b8e16c2554e0c747da6d625799b332f5fe (patch)
treedc73cbe7d56a1eea7bb7c22ab1576d0ffa673b11 /tactics
parenta1fc621b943dbf904705dc88ed27c26daf4c5e72 (diff)
Remove Sorts.contents
Diffstat (limited to 'tactics')
-rw-r--r--tactics/class_tactics.ml2
-rw-r--r--tactics/equality.ml2
-rw-r--r--tactics/inv.ml2
3 files changed, 3 insertions, 3 deletions
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 (