aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2014-10-11 21:22:45 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2014-10-16 22:28:42 +0200
commit282c4412574c955e9ff3bfdba1866b9afffa4955 (patch)
tree9bbd23629568bb4ba92ac605fd1771b9c384e6cb /test-suite
parent3c2723f77f5ab070f8232ce0cc626875120cfe41 (diff)
Relaxing again the test on types of replacements in tactic change
(continuation of 3087e0012eb12833a79b and 1f05decaea97f1dc). It may be the case that the new expression lives in a higher sorts and the context where it is substituted in supports it. So, it is too strong to expect that, when the substituted objects are types, the sort of the new one is smaller than the sort of the original one. Consider e.g. Goal @eq Type nat nat. change nat with (@id Type nat). which is a correct replacement, even if (id Type nat) is in a higher sort. Introducing typing in "contextually" would be a big change for a little numbers of uses, so we instead (hackily) recheck the whole term (even though typing with evars uses evar_conv which accept to unify Type with Set, leading to wrongly accept "Goal @eq Set nat nat. change nat with (@id Type nat).". Evar conv is however rejecting Prop=Type.)
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/success/change.v5
1 files changed, 5 insertions, 0 deletions
diff --git a/test-suite/success/change.v b/test-suite/success/change.v
index f775f818a..cd2dd77f9 100644
--- a/test-suite/success/change.v
+++ b/test-suite/success/change.v
@@ -45,3 +45,8 @@ Abort.
Goal True.
change ?x with x.
Abort.
+
+(* Check typability after change of type subterms *)
+Goal nat = nat :> Set.
+Fail change nat with (@id Type nat). (* would otherwise be ill-typed *)
+Abort.