From 05dff3bdaaf474e67b0878bc2dd0952427ce277e Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 22 Jun 2018 16:09:23 +0200 Subject: universes_of_constr don't include universes of monomorphic constants Apparently it was not useful. I don't remember what I was thinking when I added it. --- vernac/comDefinition.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'vernac/comDefinition.ml') diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index f55c852c0..a8d794642 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -93,7 +93,7 @@ let interp_definition pl bl poly red_option c ctypopt = let tyopt = Option.map (fun ty -> Term.it_mkProd_or_LetIn (EConstr.to_constr ~abort_on_undefined_evars:false evd ty) ctx) tyopt in (* Keep only useful universes. *) let uvars_fold uvars c = - Univ.LSet.union uvars (universes_of_constr env evd (of_constr c)) + Univ.LSet.union uvars (universes_of_constr evd (of_constr c)) in let uvars = List.fold_left uvars_fold Univ.LSet.empty (Option.List.cons tyopt [c]) in let evd = Evd.restrict_universe_context evd uvars in -- cgit v1.2.3