diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-05-03 13:37:41 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-05-03 13:37:41 +0200 |
| commit | 3c795ba6b5728e8a0a699ab15c773c52c48f33e4 (patch) | |
| tree | 7a95c75037ddc1c729bc496c13084d350f9f29a1 /pretyping/coercion.ml | |
| parent | 4bff930da2c029a66eaf5378e5abd2cc35554f8f (diff) | |
| parent | 15d415729962eddde2cd1d58e03449c8526ba626 (diff) | |
Merge PR#411: Mention template polymorphism in the documentation.
Diffstat (limited to 'pretyping/coercion.ml')
| -rw-r--r-- | pretyping/coercion.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index c26e7458e..e6c0075c5 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -478,8 +478,8 @@ let rec inh_conv_coerce_to_fail loc env evd rigidonly v t c1 = (* 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 retype the term because sort-polymorphism may have *) - (* weaken its type *) + (* Note: we retype the term because template polymorphism may have *) + (* weakened its type *) let name = match name with | Anonymous -> Name Namegen.default_dependent_ident | _ -> name in |