diff options
Diffstat (limited to 'vernac/comFixpoint.ml')
| -rw-r--r-- | vernac/comFixpoint.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index a794c2db06..7b382dacc3 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -224,8 +224,9 @@ let interp_recursive ~program_mode ~cofix fixl notations = (* Instantiate evars and check all are resolved *) let sigma = solve_unif_constraints_with_heuristics env_rec sigma in - let sigma, _ = nf_evars_and_universes sigma in - let fixdefs = List.map (fun c -> Option.map EConstr.(to_constr sigma) c) fixdefs in + let sigma = Evd.minimize_universes sigma in + (* XXX: We still have evars here in Program *) + let fixdefs = List.map (fun c -> Option.map EConstr.(to_constr ~abort_on_undefined_evars:false sigma) c) fixdefs in let fixtypes = List.map EConstr.(to_constr sigma) fixtypes in let fixctxs = List.map (fun (_,ctx) -> ctx) fixctxs in |