diff options
Diffstat (limited to 'vernac/comFixpoint.ml')
| -rw-r--r-- | vernac/comFixpoint.ml | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 1c141c014..b5b8697d2 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -173,11 +173,12 @@ let interp_recursive ~program_mode ~cofix fixl notations = | None , acc -> acc | x , None -> x | Some ls , Some us -> - let lsu = ls.univdecl_instance and usu = us.univdecl_instance in + let open UState in + let lsu = ls.univdecl_instance and usu = us.univdecl_instance in if not (CList.for_all2eq (fun x y -> Id.equal x.CAst.v y.CAst.v) lsu usu) then user_err Pp.(str "(co)-recursive definitions should all have the same universe binders"); Some us) fixl None in - let sigma, decl = Univdecls.interp_univ_decl_opt env all_universes in + let sigma, decl = interp_univ_decl_opt env all_universes in let sigma, (fixctxs, fiximppairs, fixannots) = on_snd List.split3 @@ List.fold_left_map (fun sigma -> interp_fix_context env sigma ~cofix) sigma fixl in @@ -199,9 +200,7 @@ let interp_recursive ~program_mode ~cofix fixl notations = try let sigma, h_term = fix_proto sigma in let app = mkApp (h_term, [|sort; t|]) in - let _evd = ref sigma in - let res = Typing.e_solve_evars env _evd app in - !_evd, res + Typing.solve_evars env sigma app with e when CErrors.noncritical e -> sigma, t in sigma, LocalAssum (id,fixprot) :: env' @@ -224,8 +223,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 @@ -233,7 +233,7 @@ let interp_recursive ~program_mode ~cofix fixl notations = (env,rec_sign,decl,sigma), (fixnames,fixdefs,fixtypes), List.combine3 fixctxs fiximps fixannots let check_recursive isfix env evd (fixnames,fixdefs,_) = - check_evars_are_solved env evd Evd.empty; + check_evars_are_solved env evd (Evd.from_env env); if List.for_all Option.has_some fixdefs then begin let fixdefs = List.map Option.get fixdefs in check_mutuality env evd isfix (List.combine fixnames fixdefs) |