diff options
author | Stephane Glondu <steph@glondu.net> | 2009-02-01 00:54:43 +0100 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2009-02-01 00:54:43 +0100 |
commit | 9c775561f67ac558c2c408cfa873544e2fea7b0a (patch) | |
tree | 375ac16822f815477b36d50e49bb3cd9633aaa84 /contrib/subtac/subtac_pretyping_F.ml | |
parent | 3e6a1167fd397f2c72b48315e5d82f6c7e24703f (diff) | |
parent | cfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 (diff) |
Merge commit 'upstream/8.2.rc2+dfsg'
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 |