diff options
Diffstat (limited to 'contrib/subtac/subtac_pretyping_F.ml')
| -rw-r--r-- | contrib/subtac/subtac_pretyping_F.ml | 23 |
1 files changed, 14 insertions, 9 deletions
diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml index 559b6ac1..00d37f35 100644 --- a/contrib/subtac/subtac_pretyping_F.ml +++ b/contrib/subtac/subtac_pretyping_F.ml @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: subtac_pretyping_F.ml 11282 2008-07-28 11:51:53Z msozeau $ *) +(* $Id: subtac_pretyping_F.ml 11576 2008-11-10 19:13:15Z msozeau $ *) open Pp open Util @@ -276,14 +276,19 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct | RApp (loc,f,args) -> let length = List.length args in - let ftycon = - if length > 0 then - match tycon with - | None -> None - | Some (None, ty) -> mk_abstr_tycon length ty - | Some (Some (init, cur), ty) -> - Some (Some (length + init, length + cur), ty) - else tycon + let ftycon = + let ty = + if length > 0 then + match tycon with + | None -> None + | Some (None, ty) -> mk_abstr_tycon length ty + | Some (Some (init, cur), ty) -> + Some (Some (length + init, length + cur), ty) + else tycon + in + match ty with + | Some (_, t) when Subtac_coercion.disc_subset t = None -> ty + | _ -> None in let fj = pretype ftycon env isevars lvar f in let floc = loc_of_rawconstr f in |