diff options
| author | filliatr | 2001-06-27 15:12:30 +0000 |
|---|---|---|
| committer | filliatr | 2001-06-27 15:12:30 +0000 |
| commit | b590f4d243811f2e59e6d75b36e93ca8a957f9b5 (patch) | |
| tree | 426813f7034c3b1554ddbcb2a56ea99d261ba3fe /contrib/correctness/psyntax.ml4 | |
| parent | bf86a8e1a180d60d5a065b5af5ff14b5286a2015 (diff) | |
correction d'un bug de Correctness (pour Y Bertot)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1812 85f007b7-540e-0410-9357-904b9bb8a0f7
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 |