diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-03-13 17:35:47 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-03-13 17:35:47 +0000 |
| commit | 729b9a0a10eec0c67680b738ca52b4e85cb23f1b (patch) | |
| tree | f177b08cec55fb70ff0e41faf8b8e7d421ddbc08 /test-suite/success/setoid_test.v | |
| parent | c9931180560b7b343427811be0f14281bc791bda (diff) | |
Fix inductive_template building ill-typed evars, and update test-suite scripts
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13909 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/success/setoid_test.v')
| -rw-r--r-- | test-suite/success/setoid_test.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/success/setoid_test.v b/test-suite/success/setoid_test.v index 63ca8aff4..19693d70c 100644 --- a/test-suite/success/setoid_test.v +++ b/test-suite/success/setoid_test.v @@ -144,7 +144,7 @@ Section mult. Goal forall x, (fold _ _ (fun x => ab A x) (add A x) = anat _ (fold _ _ (ab nat) (add _ x))). Proof. intros. setoid_rewrite fold_lemma. - change (fold A A (fun x0 : A, ab A x0) x = anat A (fold A nat (ab nat) x)). + change (fold A A (fun x0 : A => ab A x0) x = anat A (fold A nat (ab nat) x)). Abort. End mult. |