diff options
Diffstat (limited to 'contrib/correctness/psyntax.ml4')
| -rw-r--r-- | contrib/correctness/psyntax.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/correctness/psyntax.ml4 b/contrib/correctness/psyntax.ml4 index 59a32bafb..591076bdd 100644 --- a/contrib/correctness/psyntax.ml4 +++ b/contrib/correctness/psyntax.ml4 @@ -548,7 +548,7 @@ let _ = if not (is_mutable v) then begin let c = Entries.ParameterEntry (trad_ml_type_v ren env v), - Libnames.NeverDischarge in + Decl_kinds.IsAssumption Decl_kinds.Definitional in List.iter (fun id -> ignore (Declare.declare_constant id c)) ids; if_verbose (is_assumed false) ids |