Imported Upstream version 8.1.pl1+dfsgupstream/8.1.pl1+dfsg

13 files changed, 77 insertions, 60 deletions

diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index 9e902126..30f68083 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: cases.mli 8741 2006-04-26 22:30:32Z herbelin $ i*)
+(*i $Id: cases.mli 9976 2007-07-12 11:58:30Z msozeau $ i*)
 
 (*i*)
 open Util
@@ -32,10 +32,20 @@ type pattern_matching_error =
 
 exception PatternMatchingError of env * pattern_matching_error
 
+val raise_pattern_matching_error : (loc * env * pattern_matching_error) -> 'a
+
 val error_wrong_numarg_constructor_loc : loc -> env -> constructor -> int -> 'a
 
 val error_wrong_numarg_inductive_loc : loc -> env -> inductive -> int -> 'a
 
+val error_bad_constructor_loc : loc -> constructor -> inductive -> 'a
+
+val error_bad_pattern_loc : loc -> constructor -> constr -> 'a
+
+val error_wrong_predicate_arity_loc : loc -> env -> constr -> constr -> constr -> 'a
+
+val error_needs_inversion : env -> constr -> types -> 'a
+
 (*s Compilation of pattern-matching. *)
 
 module type S = sig
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index abe31e06..29dbe83d 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: clenv.ml 9279 2006-10-25 15:51:24Z herbelin $ *)
+(* $Id: clenv.ml 9665 2007-02-21 17:08:10Z herbelin $ *)
 
 open Pp
 open Util
@@ -54,7 +54,7 @@ let cl_sigma ce = evars_of ce.env
 let subst_clenv sub clenv = 
   { templval = map_fl (subst_mps sub) clenv.templval;
     templtyp = map_fl (subst_mps sub) clenv.templtyp;
-    env = subst_evar_defs sub clenv.env;
+    env = subst_evar_defs_light sub clenv.env;
     templenv = clenv.templenv }
 
 let clenv_nf_meta clenv c = nf_meta clenv.env c
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index ff435bfc..4a2e5ee3 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: detyping.ml 9535 2007-01-26 09:26:08Z jforest $ *)
+(* $Id: detyping.ml 9976 2007-07-12 11:58:30Z msozeau $ *)
 
 open Pp
 open Util
@@ -355,12 +355,15 @@ let detype_sort = function
 (**********************************************************************)
 (* Main detyping function                                             *)
 
-let rec detype isgoal avoid env t =
+let detype_anonymous = ref (fun loc n -> anomaly "detype: index to an anonymous variable")
+let set_detype_anonymous f = detype_anonymous := f
+
+let rec detype (isgoal:bool) avoid env t =
   match kind_of_term (collapse_appl t) with
     | Rel n ->
       (try match lookup_name_of_rel n env with
 	 | Name id   -> RVar (dl, id)
-	 | Anonymous -> anomaly "detype: index to an anonymous variable"
+	 | Anonymous -> !detype_anonymous dl n
        with Not_found ->
 	 let s = "_UNBOUND_REL_"^(string_of_int n)
 	 in RVar (dl, id_of_string s))
@@ -374,8 +377,7 @@ let rec detype isgoal avoid env t =
 	  RVar (dl, id))
     | Sort s -> RSort (dl,detype_sort s)
     | Cast (c1,k,c2) ->
-	RCast(dl,detype isgoal avoid env c1, CastConv k,
-              detype isgoal avoid env c2)
+	RCast(dl,detype isgoal avoid env c1, CastConv (k, detype isgoal avoid env c2))
     | Prod (na,ty,c) -> detype_binder isgoal BProd avoid env na ty c
     | Lambda (na,ty,c) -> detype_binder isgoal BLambda avoid env na ty c
     | LetIn (na,b,_,c) -> detype_binder isgoal BLetIn avoid env na b c
@@ -627,14 +629,18 @@ let rec subst_rawconstr subst raw =
       let ref',_ = subst_global subst ref in 
 	if ref' == ref then raw else
 	  RHole (loc,InternalHole)
-  | RHole (loc, (BinderType _ | QuestionMark | CasesType |
+  | RHole (loc, (BinderType _ | QuestionMark _ | CasesType |
       InternalHole | TomatchTypeParameter _)) -> raw
 
-  | RCast (loc,r1,k,r2) -> 
-      let r1' = subst_rawconstr subst r1 and r2' = subst_rawconstr subst r2 in
-	if r1' == r1 && r2' == r2 then raw else
-	  RCast (loc,r1',k,r2')
-
+  | RCast (loc,r1,k) -> 
+      (match k with 
+	   CastConv (k,r2) ->
+	     let r1' = subst_rawconstr subst r1 and r2' = subst_rawconstr subst r2 in
+	       if r1' == r1 && r2' == r2 then raw else
+		 RCast (loc,r1', CastConv (k,r2'))
+	 | CastCoerce -> 
+	     let r1' = subst_rawconstr subst r1 in
+	       if r1' == r1 then raw else RCast (loc,r1',k))
   | RDynamic _ -> raw
 
 (* Utilities to transform kernel cases to simple pattern-matching problem *)
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index bbe2fcc9..7ac7162f 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: detyping.mli 8831 2006-05-19 09:29:54Z herbelin $ i*)
+(*i $Id: detyping.mli 9976 2007-07-12 11:58:30Z msozeau $ i*)
 
 (*i*)
 open Util
@@ -44,7 +44,7 @@ val detype_sort : sorts -> rawsort
 val lookup_name_as_renamed  : env -> constr -> identifier -> int option
 val lookup_index_as_renamed : env -> constr -> int -> int option
 
-
+val set_detype_anonymous : (loc -> int -> rawconstr) -> unit
 val force_wildcard : unit -> bool
 val synthetize_type : unit -> bool
 val force_if : case_info -> bool
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 3c4a23ec..2764633b 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: evarconv.ml 9141 2006-09-15 10:07:01Z herbelin $ *)
+(* $Id: evarconv.ml 9665 2007-02-21 17:08:10Z herbelin $ *)
 
 open Pp
 open Util
@@ -327,7 +327,7 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	  solve_simple_eqn evar_conv_x env isevars (pbty,ev1,t2)
 	else
 	  (* Postpone the use of an heuristic *)
-	  add_conv_pb (pbty,applist(term1,l1),applist(term2,l2)) isevars,
+	  add_conv_pb (pbty,env,applist(term1,l1),applist(term2,l2)) isevars,
 	  true
 
     | Rigid _, Flexible ev2 ->
@@ -342,7 +342,7 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	  solve_simple_eqn evar_conv_x env isevars (pbty,ev2,t1)
 	else
 	  (* Postpone the use of an heuristic *)
-	  add_conv_pb (pbty,applist(term1,l1),applist(term2,l2)) isevars,
+	  add_conv_pb (pbty,env,applist(term1,l1),applist(term2,l2)) isevars,
 	  true
 
     | MaybeFlexible flex1, Rigid _ ->
@@ -524,8 +524,7 @@ let first_order_unification env isevars pbty (term1,l1) (term2,l2) =
 let consider_remaining_unif_problems env isevars =
   let (isevars,pbs) = get_conv_pbs isevars (fun _ -> true) in
   List.fold_left
-    (fun (isevars,b as p) (pbty,t1,t2) ->
-      (* Pas le bon env pour le problème... *)
+    (fun (isevars,b as p) (pbty,env,t1,t2) ->
       if b then first_order_unification env isevars pbty 
 	(apprec_nohdbeta env isevars (whd_castappevar (evars_of isevars) t1))
 	(apprec_nohdbeta env isevars (whd_castappevar (evars_of isevars) t2))
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index b545bd38..6896ca69 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: evarutil.ml 9573 2007-01-31 20:18:18Z notin $ *)
+(* $Id: evarutil.ml 9869 2007-05-29 11:07:04Z herbelin $ *)
 
 open Util
 open Pp
@@ -424,6 +424,8 @@ let need_restriction k args = not (array_for_all (closedn k) args)
  * false. The problem is that we won't get the right error message.
  *)
 
+exception NotClean of constr
+
 let real_clean env isevars ev evi args rhs =
   let evd = ref isevars in
   let subst = List.map (fun (x,y) -> (y,mkVar x)) (list_uniquize args) in
@@ -434,7 +436,7 @@ let real_clean env isevars ev evi args rhs =
  	 else
 	   (* Flex/Rel problem: unifiable as a pattern iff Rel in ev scope *)
 	   (try List.assoc (mkRel (i-k)) subst 
-	    with Not_found -> if rigid then raise Exit else t)
+	    with Not_found -> if rigid then raise (NotClean t) else t)
       | Evar (ev,args) ->
           if Evd.is_defined_evar !evd (ev,args) then
             subs rigid k (existential_value (evars_of !evd) (ev,args))
@@ -460,7 +462,7 @@ let real_clean env isevars ev evi args rhs =
 		 or List.exists (fun (id',_,_) -> id=id') (evar_context evi)
 	     *)
              then t
-             else raise Exit)
+             else raise (NotClean t))
                
       | _ ->
 	  (* Flex/Rigid problem (or assimilated if not normal): we "imitate" *)
@@ -470,8 +472,8 @@ let real_clean env isevars ev evi args rhs =
   let rhs = whd_beta rhs (* heuristic *) in
   let body = 
     try subs true 0 rhs
-    with Exit -> 
-      error_not_clean env (evars_of !evd) ev rhs (evar_source ev !evd) in
+    with NotClean t -> 
+      error_not_clean env (evars_of !evd) ev t (evar_source ev !evd) in
   (!evd,body)
 
 (* [evar_define] solves the problem lhs = rhs when lhs is an uninstantiated
@@ -619,7 +621,7 @@ let solve_pattern_eqn env l1 c =
  * ass.
  *)
 
-let status_changed lev (pbty,t1,t2) =
+let status_changed lev (pbty,_,t1,t2) =
   try 
     List.mem (head_evar t1) lev or List.mem (head_evar t2) lev
   with Failure _ ->
@@ -678,7 +680,7 @@ let solve_simple_eqn conv_algo env isevars (pbty,(n1,args1 as ev1),t2) =
 	  evar_define env ev1 t2 isevars in
     let (isevars,pbs) = get_conv_pbs isevars (status_changed lsp) in
     List.fold_left
-      (fun (isevars,b as p) (pbty,t1,t2) ->
+      (fun (isevars,b as p) (pbty,env,t1,t2) ->
 	if b then conv_algo env isevars pbty t1 t2 else p) (isevars,true)
       pbs
   with e when precatchable_exception e ->
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index c68a7a73..69d4352f 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: evd.ml 9573 2007-01-31 20:18:18Z notin $ *)
+(* $Id: evd.ml 9976 2007-07-12 11:58:30Z msozeau $ *)
 
 open Pp
 open Util
@@ -358,24 +358,23 @@ let metamap_to_list m =
 type hole_kind =
   | ImplicitArg of global_reference * (int * identifier option)
   | BinderType of name
-  | QuestionMark
+  | QuestionMark of bool
   | CasesType
   | InternalHole
   | TomatchTypeParameter of inductive * int
 
 type conv_pb = Reduction.conv_pb
-type evar_constraint = conv_pb * constr * constr
+type evar_constraint = conv_pb * Environ.env * constr * constr
 type evar_defs =
     { evars : evar_map;
       conv_pbs : evar_constraint list;
       history : (existential_key * (loc * hole_kind)) list;
       metas : clbinding Metamap.t }
 
-let subst_evar_defs sub evd =
+let subst_evar_defs_light sub evd =
+  assert (evd.evars = (Evarmap.empty,UniverseMap.empty));
+  assert (evd.conv_pbs = []);
   { evd with
-    conv_pbs =
-      List.map (fun (k,t1,t2) ->(k,subst_mps sub t1,subst_mps sub t2))
-        evd.conv_pbs;
     metas = Metamap.map (map_clb (subst_mps sub)) evd.metas }
 
 let create_evar_defs sigma =
@@ -552,7 +551,7 @@ let pr_evar_map sigma =
 
 let pr_constraints pbs =
   h 0
-    (prlist_with_sep pr_fnl (fun (pbty,t1,t2) ->
+    (prlist_with_sep pr_fnl (fun (pbty,_,t1,t2) ->
       print_constr t1 ++ spc() ++
       str (match pbty with
 	| Reduction.CONV -> "=="
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index e1fc425b..ef6a3d7b 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: evd.mli 9573 2007-01-31 20:18:18Z notin $ i*)
+(*i $Id: evd.mli 9976 2007-07-12 11:58:30Z msozeau $ i*)
 
 (*i*)
 open Util
@@ -111,8 +111,8 @@ val map_clb : (constr -> constr) -> clbinding -> clbinding
 (* Unification state *)
 type evar_defs
 
-(* Substitution is not applied to the [evar_map] *)
-val subst_evar_defs : substitution -> evar_defs -> evar_defs
+(* Assume empty [evar_map] and [conv_pbs] *)
+val subst_evar_defs_light : substitution -> evar_defs -> evar_defs
 
 (* create an [evar_defs] with empty meta map: *)
 val create_evar_defs : evar_map -> evar_defs
@@ -123,7 +123,7 @@ val evars_reset_evd  : evar_map ->  evar_defs -> evar_defs
 type hole_kind =
   | ImplicitArg of global_reference * (int * identifier option)
   | BinderType of name
-  | QuestionMark
+  | QuestionMark of bool (* Can it be turned into an obligation ? *)
   | CasesType
   | InternalHole
   | TomatchTypeParameter of inductive * int
@@ -138,7 +138,7 @@ val evar_source : existential_key -> evar_defs -> loc * hole_kind
 
 (* Unification constraints *)
 type conv_pb = Reduction.conv_pb
-type evar_constraint = conv_pb * constr * constr
+type evar_constraint = conv_pb * Environ.env * constr * constr
 val add_conv_pb :  evar_constraint -> evar_defs -> evar_defs
 val get_conv_pbs : evar_defs -> (evar_constraint -> bool) -> 
   evar_defs * evar_constraint list
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index eb8a25eb..3060ee03 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: pattern.ml 8963 2006-06-19 18:54:49Z barras $ *)
+(* $Id: pattern.ml 9976 2007-07-12 11:58:30Z msozeau $ *)
 
 open Util
 open Names
@@ -233,7 +233,7 @@ let rec pat_of_raw metas vars = function
       PSort s
   | RHole _ ->
       PMeta None
-  | RCast (_,c,_,t) ->
+  | RCast (_,c,_) ->
       Options.if_verbose
         Pp.warning "Cast not taken into account in constr pattern";
       pat_of_raw metas vars c
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 0b00c82c..0db64a52 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: pretyping.ml 9338 2006-11-03 13:09:53Z herbelin $ *)
+(* $Id: pretyping.ml 9976 2007-07-12 11:58:30Z msozeau $ *)
 
 open Pp
 open Util
@@ -571,13 +571,13 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	  ((fun vtyc env -> pretype vtyc env isevars lvar),isevars)
 	  tycon env (* loc *) (po,tml,eqns)
 
-    | RCast(loc,c,k,t) ->
+    | RCast (loc,c,k) ->
 	let cj =
 	  match k with
 	      CastCoerce ->
 		let cj = pretype empty_tycon env isevars lvar c in
 		  evd_comb1 (Coercion.inh_coerce_to_base loc env) isevars cj
-	    | CastConv k ->
+	    | CastConv (k,t) ->
 		let tj = pretype_type empty_valcon env isevars lvar t in
 		let cj = pretype (mk_tycon tj.utj_val) env isevars lvar c in
 		  (* User Casts are for helping pretyping, experimentally not to be kept*)
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index d7e3ac77..aaf9e63d 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: rawterm.ml 9535 2007-01-26 09:26:08Z jforest $ *)
+(* $Id: rawterm.ml 9976 2007-07-12 11:58:30Z msozeau $ *)
 
 (*i*)
 open Util
@@ -47,8 +47,8 @@ type 'a bindings =
 
 type 'a with_bindings = 'a * 'a bindings
 
-type cast_type =
-  | CastConv of cast_kind
+type 'a cast_type =
+  | CastConv of cast_kind * 'a
   | CastCoerce (* Cast to a base type (eg, an underlying inductive type) *)
 
 type rawconstr = 
@@ -68,7 +68,7 @@ type rawconstr =
       rawconstr array * rawconstr array
   | RSort of loc * rawsort
   | RHole of (loc * hole_kind)
-  | RCast of loc * rawconstr * cast_type * rawconstr
+  | RCast of loc * rawconstr * rawconstr cast_type
   | RDynamic of loc * Dyn.t
 
 and rawdecl = name * rawconstr option * rawconstr
@@ -120,7 +120,7 @@ let map_rawconstr f = function
   | RRec (loc,fk,idl,bl,tyl,bv) ->
       RRec (loc,fk,idl,Array.map (List.map (map_rawdecl f)) bl,
             Array.map f tyl,Array.map f bv)
-  | RCast (loc,c,k,t) -> RCast (loc,f c,k,f t)
+  | RCast (loc,c,k) -> RCast (loc,f c, match k with CastConv (k,t) -> CastConv (k, f t) | x -> x)
   | (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) as x -> x
   
 
@@ -190,7 +190,7 @@ let occur_rawconstr id =
                 (na=Name id or not(occur_fix bl)) in
           occur_fix bl)
           idl bl tyl bv)
-    | RCast (loc,c,_,t) -> (occur c) or (occur t)
+    | RCast (loc,c,k) -> (occur c) or (match k with CastConv (_, t) -> occur t | CastCoerce -> false)
     | (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) -> false
 
   and occur_pattern (loc,idl,p,c) = not (List.mem id idl) & (occur c)
@@ -247,7 +247,8 @@ let free_rawvars  =
 	  vars bounded1 vs2 bv.(i)
 	in
 	array_fold_left_i vars_fix vs idl
-    | RCast (loc,c,_,t) -> vars bounded (vars bounded vs c) t
+    | RCast (loc,c,k) -> let v = vars bounded vs c in 
+	(match k with CastConv (_,t) -> vars bounded v t | _ -> v)
     | (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) -> vs
 
   and vars_pattern bounded vs (loc,idl,p,c) = 
@@ -280,7 +281,7 @@ let loc_of_rawconstr = function
   | RRec (loc,_,_,_,_,_) -> loc
   | RSort (loc,_) -> loc
   | RHole (loc,_) -> loc
-  | RCast (loc,_,_,_) -> loc
+  | RCast (loc,_,_) -> loc
   | RDynamic (loc,_) -> loc
 
 (**********************************************************************)
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index e5601705..546b36b0 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: rawterm.mli 9535 2007-01-26 09:26:08Z jforest $ i*)
+(*i $Id: rawterm.mli 9976 2007-07-12 11:58:30Z msozeau $ i*)
 
 (*i*)
 open Util
@@ -51,8 +51,8 @@ type 'a bindings =
 
 type 'a with_bindings = 'a * 'a bindings
 
-type cast_type =
-  | CastConv of cast_kind
+type 'a cast_type =
+  | CastConv of cast_kind * 'a
   | CastCoerce (* Cast to a base type (eg, an underlying inductive type) *)
 
 type rawconstr = 
@@ -72,7 +72,7 @@ type rawconstr =
       rawconstr array * rawconstr array
   | RSort of loc * rawsort
   | RHole of (loc * Evd.hole_kind)
-  | RCast of loc * rawconstr * cast_type * rawconstr
+  | RCast of loc * rawconstr * rawconstr cast_type
   | RDynamic of loc * Dyn.t
 
 and rawdecl = name * rawconstr option * rawconstr
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 006e14b3..92617820 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: tacred.ml 8793 2006-05-05 17:41:41Z barras $ *)
+(* $Id: tacred.ml 9762 2007-04-13 12:46:50Z herbelin $ *)
 
 open Pp
 open Util
@@ -365,7 +365,7 @@ let contract_cofix_use_function f (bodynum,(_,names,bodies as typedbodies)) =
     | Some c -> c in
 (*    match List.nth names j with Name id -> f id | _ -> assert false in*)
   let subbodies = list_tabulate make_Fi nbodies in
-  substl subbodies bodies.(bodynum)
+  substl (List.rev subbodies) bodies.(bodynum)
 
 let reduce_mind_case_use_function func env mia =
   match kind_of_term mia.mconstr with