summaryrefslogtreecommitdiff
path: root/test-suite/success/specialize.v
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/success/specialize.v')
-rw-r--r--test-suite/success/specialize.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/success/specialize.v b/test-suite/success/specialize.v
index 4929ae4c..57837321 100644
--- a/test-suite/success/specialize.v
+++ b/test-suite/success/specialize.v
@@ -2,7 +2,7 @@
Goal forall a b c : nat, a = b -> b = c -> forall d, a+d=c+d.
intros.
-(* "compatibility" mode: specializing a global name
+(* "compatibility" mode: specializing a global name
means a kind of generalize *)
specialize trans_equal. intros _.