From 018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Thu, 19 Jan 2006 22:34:29 +0000 Subject: Imported Upstream version 8.0pl3 --- pretyping/detyping.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'pretyping/detyping.ml') diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 41f63ace..040a185e 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: detyping.ml,v 1.75.2.4 2004/07/16 19:30:44 herbelin Exp $ *) +(* $Id: detyping.ml,v 1.75.2.5 2005/09/06 14:30:41 herbelin Exp $ *) open Pp open Util @@ -446,7 +446,7 @@ and detype_eqn tenv avoid env constr construct_nargs branch = let make_pat x avoid env b ids = if force_wildcard () & noccurn 1 b then PatVar (dummy_loc,Anonymous),avoid,(add_name Anonymous env),ids - else + else let id = next_name_away_with_default "x" x avoid in PatVar (dummy_loc,Name id),id::avoid,(add_name (Name id) env),id::ids in @@ -487,6 +487,6 @@ and detype_binder tenv bk avoid env na ty c = concrete_name (fst tenv) avoid env na c in let r = detype tenv avoid' (add_name na' env) c in match bk with - | BProd -> RProd (dummy_loc, na',detype tenv [] env ty, r) - | BLambda -> RLambda (dummy_loc, na',detype tenv [] env ty, r) - | BLetIn -> RLetIn (dummy_loc, na',detype tenv [] env ty, r) + | BProd -> RProd (dummy_loc, na',detype tenv avoid env ty, r) + | BLambda -> RLambda (dummy_loc, na',detype tenv avoid env ty, r) + | BLetIn -> RLetIn (dummy_loc, na',detype tenv avoid env ty, r) -- cgit v1.2.3