summaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cases.ml7
-rw-r--r--pretyping/coercion.ml6
-rw-r--r--pretyping/detyping.ml10
-rw-r--r--pretyping/evarconv.ml27
-rw-r--r--pretyping/pretyping.ml10
-rwxr-xr-xpretyping/recordops.ml10
-rwxr-xr-xpretyping/recordops.mli9
-rw-r--r--pretyping/tacred.ml5
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 *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-02 08:31:55 +0000