Imported Upstream version 8.0pl3upstream/8.0pl3

8 files changed, 28 insertions, 56 deletions

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
@@ -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 =
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 *)