diff options
Diffstat (limited to 'contrib/correctness/psyntax.ml4')
| -rw-r--r-- | contrib/correctness/psyntax.ml4 | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/contrib/correctness/psyntax.ml4 b/contrib/correctness/psyntax.ml4 index e9bb7c88f9..5e0f9ad428 100644 --- a/contrib/correctness/psyntax.ml4 +++ b/contrib/correctness/psyntax.ml4 @@ -539,7 +539,8 @@ let _ = Util.errorlabstrm "PROGVARIABLE" [< 'sTR"Clash with previous constant "; pr_id id >]) ids; - let v = Pdb.db_type_v [] (out_typev d) in + let v = out_typev d in + Pdb.check_type_v (all_refs ()) v; let env = empty in let ren = update empty_ren "" [] in let v = Ptyping.cic_type_v env ren v in |