diff --git a/lib/ModuRes/DecEnsemble.v b/lib/ModuRes/DecEnsemble.v
index 439483357c5a273e3740dc892ce916801e6c0a04..0cb4d3e9a396e1532600699fef34dcbde87ce07c 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 f89346aa21c94412e568e900f4492bc60c14abbb..e8dcc2fdbf486aec5190e077a434e5623dd9f389 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.