diff options
Diffstat (limited to 'pretyping/detyping.ml')
| -rw-r--r-- | pretyping/detyping.ml | 10 |
1 files changed, 5 insertions, 5 deletions
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) |