diff options
Diffstat (limited to 'vernac/vernacentries.ml')
| -rw-r--r-- | vernac/vernacentries.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index ef8631fbb6..824bf35b1d 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -550,7 +550,7 @@ let start_lemma_com ~program_mode ~poly ~scope ~kind ?using ?hook thms = let env0 = Global.env () in let flags = Pretyping.{ all_no_fail_flags with program_mode } in let decl = fst (List.hd thms) in - let evd, udecl = Constrexpr_ops.interp_univ_decl_opt env0 (snd decl) in + let evd, udecl = Constrintern.interp_univ_decl_opt env0 (snd decl) in let evd, thms = interp_lemma ~program_mode ~flags ~scope env0 evd thms in let mut_analysis = RecLemmas.look_for_possibly_mutual_statements evd thms in let evd = Evd.minimize_universes evd in |