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/cases.ml | 7 ++----- pretyping/coercion.ml | 6 +----- pretyping/detyping.ml | 10 +++++----- pretyping/evarconv.ml | 27 +++++++++++---------------- pretyping/pretyping.ml | 10 ++++------ pretyping/recordops.ml | 10 +--------- pretyping/recordops.mli | 9 +-------- pretyping/tacred.ml | 5 +++-- 8 files changed, 28 insertions(+), 56 deletions(-) (limited to 'pretyping') diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 378eee30..4aff508f 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: cases.ml,v 1.111.2.4 2004/12/09 20:07:01 herbelin Exp $ *) +(* $Id: cases.ml,v 1.111.2.5 2005/04/29 16:31:03 herbelin Exp $ *) open Util open Names @@ -171,10 +171,7 @@ let pred_case_ml env sigma isrec (IndType (indf,realargs)) (i,ft) = open Pp let mssg_may_need_inversion () = - str "This pattern-matching is not exhaustive." - -let mssg_this_case_cannot_occur () = - "This pattern-matching is not exhaustive." + str "Found a matching with no clauses on a term unknown to have an empty inductive type" (* Utils *) let make_anonymous_patvars = diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index f214388f..be78eb2c 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -5,7 +5,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coercion.ml,v 1.38.6.1 2004/07/16 19:30:44 herbelin Exp $ *) +(* $Id: coercion.ml,v 1.38.6.2 2005/11/29 21:40:52 letouzey Exp $ *) open Util open Names @@ -60,10 +60,6 @@ let inh_pattern_coerce_to loc pat ind1 ind2 = (* appliquer le chemin de coercions p à hj *) let apply_coercion env p hj typ_cl = - if !compter then begin - nbpathc := !nbpathc +1; - nbcoer := !nbcoer + (List.length p) - end; try fst (List.fold_left (fun (ja,typ_cl) i -> 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) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 0ee95a0f..2264f82b 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: evarconv.ml,v 1.44.6.2 2004/11/26 23:51:39 herbelin Exp $ *) +(* $Id: evarconv.ml,v 1.44.6.3 2005/11/29 21:40:52 letouzey Exp $ *) open Util open Names @@ -380,21 +380,16 @@ and conv_record env isevars (c,bs,(params,params1),(us,us2),(ts,ts1),c1) = (new_isevar isevars env dloc (substl ks b)) :: ks) [] bs in - if (list_for_all2eq - (fun u1 u -> evar_conv_x env isevars CONV u1 (substl ks u)) - us2 us) - & - (list_for_all2eq - (fun x1 x -> evar_conv_x env isevars CONV x1 (substl ks x)) - params1 params) - & (list_for_all2eq (evar_conv_x env isevars CONV) ts ts1) - & (evar_conv_x env isevars CONV c1 (applist (c,(List.rev ks)))) - then - (*TR*) (if !compter then (nbstruc:=!nbstruc+1; - nbimplstruc:=!nbimplstruc+(List.length ks);true) - else true) - else false - + (list_for_all2eq + (fun u1 u -> evar_conv_x env isevars CONV u1 (substl ks u)) + us2 us) + & + (list_for_all2eq + (fun x1 x -> evar_conv_x env isevars CONV x1 (substl ks x)) + params1 params) + & (list_for_all2eq (evar_conv_x env isevars CONV) ts ts1) + & (evar_conv_x env isevars CONV c1 (applist (c,(List.rev ks)))) + let the_conv_x env isevars t1 t2 = evar_conv_x env isevars CONV t1 t2 let the_conv_x_leq env isevars t1 t2 = evar_conv_x env isevars CUMUL t1 t2 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 = diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index f34d5624..3e73cfee 100755 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: recordops.ml,v 1.26.2.1 2004/07/16 19:30:46 herbelin Exp $ *) +(* $Id: recordops.ml,v 1.26.2.2 2005/11/29 21:40:52 letouzey Exp $ *) open Util open Pp @@ -20,14 +20,6 @@ open Libobject open Library open Classops -let nbimpl = ref 0 -let nbpathc = ref 0 -let nbcoer = ref 0 -let nbstruc = ref 0 -let nbimplstruc = ref 0 - -let compter = ref false - (*s Une structure S est un type inductif non récursif à un seul constructeur (de nom par défaut Build_S) *) diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index 66c1f34d..a458b7b3 100755 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: recordops.mli,v 1.15.2.1 2004/07/16 19:30:46 herbelin Exp $ i*) +(*i $Id: recordops.mli,v 1.15.2.2 2005/11/29 21:40:52 letouzey Exp $ i*) (*i*) open Names @@ -18,13 +18,6 @@ open Libobject open Library (*i*) -val nbimpl : int ref -val nbpathc : int ref -val nbcoer : int ref -val nbstruc : int ref -val nbimplstruc : int ref -val compter : bool ref - type struc_typ = { s_CONST : identifier; s_PARAM : int; diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index f225e79f..e8bde1f3 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tacred.ml,v 1.75.2.6 2004/12/29 10:17:10 herbelin Exp $ *) +(* $Id: tacred.ml,v 1.75.2.7 2005/11/02 13:18:43 herbelin Exp $ *) open Pp open Util @@ -204,13 +204,14 @@ let invert_name labs l na0 env sigma ref = function match refi with | None -> None | Some ref -> - match reference_opt_value sigma env ref with + try match reference_opt_value sigma env ref with | None -> None | Some c -> let labs',ccl = decompose_lam c in let _, l' = whd_betalet_stack ccl in let labs' = List.map snd labs' in if labs' = labs & l = l' then Some ref else None + with Not_found (* Undefined ref *) -> None else Some ref | Anonymous -> None (* Actually, should not occur *) -- cgit v1.2.3