From cb0a20de97e12a7511924a2ada74218b7c7ec9a3 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 15 Jun 2015 11:05:47 +0200
Subject: [PATCH] slight simpl tuning
---
lib/ModuRes/DecEnsemble.v | 2 +-
lib/ModuRes/SPred.v | 1 +
2 files changed, 2 insertions(+), 1 deletion(-)
diff --git a/lib/ModuRes/DecEnsemble.v b/lib/ModuRes/DecEnsemble.v
index 439483357..0cb4d3e9a 100644
--- a/lib/ModuRes/DecEnsemble.v
+++ b/lib/ModuRes/DecEnsemble.v
@@ -95,7 +95,7 @@ Notation "de1 # de2" := (de1 ∩ de2 == de_emp) (at level 70) : de_scope.
in the context that also occurs in one of the <de>s. In this case, it can help to
do the specialization manually, and call de_tauto directly.
*)
-Ltac de_unfold := unfold de_cap, de_cup, de_minus, de_compl, const; unlock; simpl.
+Ltac de_unfold := unfold de_cap, de_cup, de_minus, de_compl; unlock; simpl.
Ltac de_in_destr := simpl;
repeat (match goal with
| [ |- context[dec_eq ?i ?j] ] => destruct (dec_eq i j); first try subst j; try contradiction_eq; simpl
diff --git a/lib/ModuRes/SPred.v b/lib/ModuRes/SPred.v
index f89346aa2..e8dcc2fdb 100644
--- a/lib/ModuRes/SPred.v
+++ b/lib/ModuRes/SPred.v
@@ -20,6 +20,7 @@ Section Props.
fun n => match n with
| O => True
| S _ => P end.
+ Global Arguments sp_constF _ !n /.
Program Definition sp_const P :=
p[(sp_constF P)].
Next Obligation.
--
GitLab