From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Wed, 21 Jul 2010 09:46:51 +0200 Subject: Imported Upstream snapshot 8.3~beta0+13298 --- test-suite/ideal-features/evars_subst.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'test-suite/ideal-features/evars_subst.v') diff --git a/test-suite/ideal-features/evars_subst.v b/test-suite/ideal-features/evars_subst.v index 6f9f86a9..b3dfb33c 100644 --- a/test-suite/ideal-features/evars_subst.v +++ b/test-suite/ideal-features/evars_subst.v @@ -3,12 +3,12 @@ (* Let n be the number of let-in. The complexity comes from the fact that each implicit arguments of f was in a larger and larger - context. To compute the type of "let _ := f ?Tn 0 in f ?T 0", + context. To compute the type of "let _ := f ?Tn 0 in f ?T 0", "f ?Tn 0" is substituted in the type of "f ?T 0" which is ?T. This type is an evar instantiated on the n variables denoting the "f ?Ti 0". One obtain "?T[1;...;n-1;f ?Tn[1;...;n-1] 0]". To compute the type of "let _ := f ?Tn-1 0 in let _ := f ?Tn 0 in f ?T 0", another - substitution is done leading to + substitution is done leading to "?T[1;...;n-2;f ?Tn[1;...;n-2] 0;f ?Tn[1;...;n-2;f ?Tn[1;...;n-2] 0] 0]" and so on. At the end, we get a term of exponential size *) @@ -25,7 +25,7 @@ Time Check let _ := f _ 0 in let _ := f _ 0 in let _ := f _ 0 in - + let _ := f _ 0 in let _ := f _ 0 in let _ := f _ 0 in -- cgit v1.2.3