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/pretyping.ml | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) (limited to 'pretyping/pretyping.ml') diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 36df9c8a..bb0e74bb 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: pretyping.ml,v 1.123.2.3 2004/07/16 19:30:45 herbelin Exp $ *) +(* $Id: pretyping.ml,v 1.123.2.5 2005/11/29 21:40:52 letouzey Exp $ *) open Pp open Util @@ -161,13 +161,13 @@ let strip_meta id = (* For Grammar v7 compatibility *) let pretype_id loc env (lvar,unbndltacvars) id = let id = strip_meta id in (* May happen in tactics defined by Grammar *) - try - List.assoc id lvar - with Not_found -> try let (n,typ) = lookup_rel_id id (rel_context env) in { uj_val = mkRel n; uj_type = type_app (lift n) typ } with Not_found -> + try + List.assoc id lvar + with Not_found -> try let (_,_,typ) = lookup_named id env in { uj_val = mkVar id; uj_type = typ } @@ -238,7 +238,6 @@ let rec pretype tycon env isevars lvar = function anomaly "Found a pattern variable in a rawterm to type" | RHole (loc,k) -> - if !compter then nbimpl:=!nbimpl+1; (match tycon with | Some ty -> { uj_val = new_isevar isevars env (loc,k) ty; uj_type = ty } @@ -892,7 +891,6 @@ let rec pretype tycon env isevars lvar = function (* [pretype_type valcon env isevars lvar c] coerces [c] into a type *) and pretype_type valcon env isevars lvar = function | RHole loc -> - if !compter then nbimpl:=!nbimpl+1; (match valcon with | Some v -> let s = -- cgit v1.2.3