diff options
Diffstat (limited to 'contrib/correctness/psyntax.ml4')
| -rw-r--r-- | contrib/correctness/psyntax.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/contrib/correctness/psyntax.ml4 b/contrib/correctness/psyntax.ml4 index 6f07ad93ee..59a32bafbb 100644 --- a/contrib/correctness/psyntax.ml4 +++ b/contrib/correctness/psyntax.ml4 @@ -547,8 +547,8 @@ let _ = let v = Ptyping.cic_type_v env ren v in if not (is_mutable v) then begin let c = - Safe_typing.ParameterEntry (trad_ml_type_v ren env v), - Nametab.NeverDischarge in + Entries.ParameterEntry (trad_ml_type_v ren env v), + Libnames.NeverDischarge in List.iter (fun id -> ignore (Declare.declare_constant id c)) ids; if_verbose (is_assumed false) ids |