diff options
| author | Matthieu Sozeau | 2016-01-19 14:09:55 -0500 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-01-19 14:32:06 -0500 |
| commit | cbef33066dd526516c03474ffb35457047093808 (patch) | |
| tree | 1c2e36433957211c69a9915ef7d39b3aac5587e3 /tactics | |
| parent | 13e969e644a6ad23f6d326f3e4a253ae0393da9c (diff) | |
Fix bug #4420: check_types was losing universe constraints.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tactics.ml | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 131730ebc0..b57fd70ee1 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -634,24 +634,27 @@ let check_types env sigma mayneedglobalcheck deep newc origc = let t1 = Retyping.get_type_of env sigma newc in if deep then begin let t2 = Retyping.get_type_of env sigma origc in - let sigma, t2 = Evarsolve.refresh_universes ~onlyalg:true (Some false) env sigma t2 in - if not (snd (infer_conv ~pb:Reduction.CUMUL env sigma t1 t2)) then + let sigma, t2 = Evarsolve.refresh_universes + ~onlyalg:true (Some false) env sigma t2 in + let sigma, b = infer_conv ~pb:Reduction.CUMUL env sigma t1 t2 in + if not b then if isSort (whd_betadeltaiota env sigma t1) && isSort (whd_betadeltaiota env sigma t2) - then - mayneedglobalcheck := true + then (mayneedglobalcheck := true; sigma) else errorlabstrm "convert-check-hyp" (str "Types are incompatible.") + else sigma end else if not (isSort (whd_betadeltaiota env sigma t1)) then errorlabstrm "convert-check-hyp" (str "Not a type.") + else sigma (* Now we introduce different instances of the previous tacticals *) let change_and_check cv_pb mayneedglobalcheck deep t env sigma c = let sigma, t' = t sigma in - check_types env sigma mayneedglobalcheck deep t' c; + let sigma = check_types env sigma mayneedglobalcheck deep t' c in let sigma, b = infer_conv ~pb:cv_pb env sigma t' c in if not b then errorlabstrm "convert-check-hyp" (str "Not convertible."); sigma, t' |