From fbe0ea439ed3cf2ad933bd6094a36b5cebc5bd19 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 2 Sep 2020 12:32:29 +0200
Subject: Circumvent revealed bug of evar resolution for fixpoint

This is to be removed once #12920 is merged.
---
 vernac/comFixpoint.ml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 0f34adf1c7..564d24c1ea 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -247,6 +247,7 @@ let interp_fixpoint ?(check_recursivity=true) ~cofix l :
     (EConstr.rel_context * Impargs.manual_implicits * int option) list) =
   let (env,_,pl,evd),fix,info = interp_recursive ~program_mode:false ~cofix l in
   if check_recursivity then check_recursive true env evd fix;
+  let evd = Pretyping.(solve_remaining_evars all_no_fail_flags env evd) in
   let uctx,fix = ground_fixpoint env evd fix in
   (fix,pl,uctx,info)
 
-- 
cgit v1.2.3