Adapt to Coq PR #18921: change of return clause in Program Definition.

MetaCoq · Apr 10, 2024 · 10ed5fb · 10ed5fb
1 parent eb4ea19
commit 10ed5fb
Showing 1 changed file with 3 additions and 1 deletion.
diff --git a/safechecker/theories/PCUICSafeChecker.v b/safechecker/theories/PCUICSafeChecker.v
@@ -1946,7 +1946,9 @@ End monad_Alli_nth_forall.
     rename Heq_anonymous into eqp.
     sq. red. rewrite -eqp. exact I.
   Qed.
-  Next Obligation.  specialize_Σ H. sq. rewrite Heq_x. eauto. Qed.
+  (* Obligation automatically solved in the presence of Coq PR #18921
+  Next Obligation. specialize_Σ H. Show. sq. Show. rewrite Heq_x. eauto. Qed.
+  *)
   Next Obligation.
     specialize_Σ H. sq. red. intros. rewrite -Heq_x //.
     destruct ind_projs => //.