diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-04-08 14:08:50 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-04-08 14:08:50 +0000 |
| commit | 31c44227059be9227f8fc921f74a80094f9bbcfe (patch) | |
| tree | 7d0d1b6aa6586470ad9fb508574d69709447111e /pretyping | |
| parent | 7cc81d4bebb993ea6f71290a808a74439465cdde (diff) | |
Applying and reworking Tom Prince's patch for test-suite/failure/universes2.v
which did not test what it was supposed to test
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13970 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/coercion.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 5503a147a..389761aeb 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -202,7 +202,7 @@ module Default = struct (* We eta-expand (hence possibly modifying the original term!) *) (* and look for a coercion c:u1->t1 s.t. fun x:u1 => v' (c x)) *) (* has type forall (x:u1), u2 (with v' recursively obtained) *) - (* Note: we retupe the term because sort-polymorphism may have *) + (* Note: we retype the term because sort-polymorphism may have *) (* weaken its type *) let name = match name with | Anonymous -> Name (id_of_string "x") |