diff options
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/correctness/psyntax.ml4 | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/contrib/correctness/psyntax.ml4 b/contrib/correctness/psyntax.ml4 index b85a50790f..77d2616532 100644 --- a/contrib/correctness/psyntax.ml4 +++ b/contrib/correctness/psyntax.ml4 @@ -546,9 +546,11 @@ let _ = let ren = update empty_ren "" [] in let v = Ptyping.cic_type_v env ren v in if not (is_mutable v) then begin - let c = trad_ml_type_v ren env v in + let c = + Safe_typing.ParameterEntry (trad_ml_type_v ren env v), + Declare.NeverDischarge in List.iter - (fun id -> ignore (Declare.declare_parameter id c)) ids; + (fun id -> ignore (Declare.declare_constant id c)) ids; if_verbose (is_assumed false) ids end; if not (is_pure v) then begin |