Hack to deal with remaining evars in fixpoints.

coq · Sep 2, 2023 · 7d14b17 · 7d14b17
1 parent 5b84786
commit 7d14b17
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
@@ -1396,6 +1396,7 @@ and knht info e t stk =
     | LetIn (n,b,t,c) ->
       { mark = Red; term = FLetIn (n, mk_clos e b, mk_clos e t, c, e) }, stk
     | Evar ev ->
+(try
       begin match info.i_cache.i_sigma.evar_expand ev with
       | EvarDefined c -> knht info e c stk
       | EvarUndefined (evk, args) ->
@@ -1405,6 +1406,8 @@ and knht info e t stk =
         else
           (mk_irrelevant, skip_irrelevant_stack info stk)
       end
+with Assert_failure _ ->
+          { mark = Ntrl; term = FAtom t }, stk)
     | Array(u,t,def,ty) ->
       let len = Array.length t in
       let ty = mk_clos e ty in