Merge pull request #612 from SkySkimmer/fix-congruence

Fix call to congruence after coq/coq#19032
mattam82 · Jul 9, 2024 · 7863db3 · 7863db3
2 parents abed609 + 1bbd487
commit 7863db3
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/principles_proofs.ml b/src/principles_proofs.ml
@@ -916,7 +916,7 @@ let solve_rec_eq simpltac subst =
             [((Locus.OnlyOccurrences [1]), Evaluable.EvalConstRef f_cst); 
               ((Locus.OnlyOccurrences [1]), Evaluable.EvalConstRef funf_cst)]
         in tclTHENLIST [unfolds; simpltac; pi_tac ()]
-      with Not_found -> tclORELSE reflexivity (congruence_tac 10 []))
+      with Not_found -> tclORELSE reflexivity (congruence_tac (Some 10) []))
   | _ -> reflexivity
   end