diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-06-26 15:56:28 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-06-26 15:56:28 +0200 |
| commit | b98ae49d282f73343c1950e960f4b3bc7c28de70 (patch) | |
| tree | 53114d948cc278ca0a98e0a19e0ca9282ee891cd /vernac/comDefinition.ml | |
| parent | 0b8c1aa84dc7200b055d45cf528a83163dfd21f8 (diff) | |
| parent | 40114382c04aafa1c8e1c156ca24a5ad1aa4b9fb (diff) | |
Merge PR #7906: universes_of_constr don't include universes of monomorphic constants
Diffstat (limited to 'vernac/comDefinition.ml')
| -rw-r--r-- | vernac/comDefinition.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 |