diff options
| author |  Samuel Mimram <smimram@debian.org> | 2006-01-19 22:34:29 +0000 |
|---|---|---|
| committer | Samuel Mimram <smimram@debian.org> | 2006-01-19 22:34:29 +0000 |
| commit | 018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 (patch) | |
| tree | fbb91e2f74c73bb867ab62c58f248a704bbe6dec /pretyping/pretyping.ml | |
| parent | 6497f27021fec4e01f2182014f2bb1989b4707f9 (diff) | |
Imported Upstream version 8.0pl3upstream/8.0pl3
Diffstat (limited to 'pretyping/pretyping.ml')
| -rw-r--r-- | pretyping/pretyping.ml | 10 |
1 files changed, 4 insertions, 6 deletions
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 @@ -162,13 +162,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 } with Not_found -> @@ -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 = |