From 72b9a7df489ea47b3e5470741fd39f6100d31676 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Sat, 18 Aug 2007 20:34:57 +0000 Subject: Imported Upstream version 8.1.pl1+dfsg --- pretyping/pretyping.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'pretyping/pretyping.ml') diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 0b00c82c..0db64a52 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: pretyping.ml 9338 2006-11-03 13:09:53Z herbelin $ *) +(* $Id: pretyping.ml 9976 2007-07-12 11:58:30Z msozeau $ *) open Pp open Util @@ -571,13 +571,13 @@ module Pretyping_F (Coercion : Coercion.S) = struct ((fun vtyc env -> pretype vtyc env isevars lvar),isevars) tycon env (* loc *) (po,tml,eqns) - | RCast(loc,c,k,t) -> + | RCast (loc,c,k) -> let cj = match k with CastCoerce -> let cj = pretype empty_tycon env isevars lvar c in evd_comb1 (Coercion.inh_coerce_to_base loc env) isevars cj - | CastConv k -> + | CastConv (k,t) -> let tj = pretype_type empty_valcon env isevars lvar t in let cj = pretype (mk_tycon tj.utj_val) env isevars lvar c in (* User Casts are for helping pretyping, experimentally not to be kept*) -- cgit v1.2.3