From dbc820f0df53218e730eba34b44a3b1901f13b9e Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 2 Mar 2018 15:50:32 +0100 Subject: Deprecate mixing univ minimization and evm normalization functions. Normalization sounds like it should be semantically noop. --- vernac/comFixpoint.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'vernac/comFixpoint.ml') diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 1466fa243..7b382dacc 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -224,7 +224,7 @@ 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 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 -- cgit v1.2.3