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

10 files changed, 86 insertions, 56 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index a4880f5e..c2d8921e 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: cases.ml 11897 2009-02-09 19:28:02Z barras $ *)
+(* $Id: cases.ml 12167 2009-06-06 20:07:22Z herbelin $ *)
 
 open Util
 open Names
@@ -130,7 +130,7 @@ let push_rel_defs =
 (* We have x1:t1...xn:tn,xi':ti,y1..yk |- c and re-generalize
    over xi:ti to get x1:t1...xn:tn,xi':ti,y1..yk |- c[xi:=xi'] *)
 
-let regeneralize_rel i k j = if j = i+k then k else if j < i+k then j else j
+let regeneralize_rel i k j = if j = i+k then k+1 else j
 
 let rec regeneralize_index i k t = match kind_of_term t with
   | Rel j when j = i+k -> mkRel (k+1)
@@ -605,19 +605,13 @@ let find_dependencies_signature deps_in_rhs typs =
   let _,l = List.fold_right2 find_dependencies deps_in_rhs typs (k,[]) in
   List.map (fun (_,deps,_) -> deps) l
 
-(******)
+(* Assume we had terms t1..tq to match in a context xp:Tp,...,x1:T1 |-
+   and xn:Tn has just been regeneralized into x:Tn so that the terms
+   to match are now to be considered in the context xp:Tp,...,x1:T1,x:Tn |-.
 
-(* A Pushed term to match has just been substituted by some
-   constructor t = (ci x1...xn) and the terms x1 ... xn have been added to
-   match 
-
-   - all terms to match and to push (dependent on t by definition)
-     must have (Rel depth) substituted by t and Rel's>depth lifted by n
-   - all pushed terms to match (non dependent on t by definition) must
-     be lifted by n
-
-  We start with depth=1
-*)
+   [regeneralize_index_tomatch n tomatch] updates t1..tq so that
+   former references to xn are now references to x. Note that t1..tq
+   are already adjusted to the context xp:Tp,...,x1:T1,x:Tn |-. *)
 
 let regeneralize_index_tomatch n =
   let rec genrec depth = function
@@ -661,6 +655,13 @@ let replace_tomatch n c =
 let liftn_rel_declaration n k = map_rel_declaration (liftn n k)
 let substnl_rel_declaration sigma k = map_rel_declaration (substnl sigma k)
 
+(* [liftn_tomatch_stack]: a term to match has just been substituted by
+   some constructor t = (ci x1...xn) and the terms x1 ... xn have been
+   added to match; all pushed terms to match must be lifted by n
+   (knowing that [Abstract] introduces a binder in the list of pushed
+   terms to match).
+*)
+
 let rec liftn_tomatch_stack n depth = function
   | [] -> []
   | Pushed ((c,tm),l,dep)::rest ->
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 4c5ebe3e..043a326d 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: evarconv.ml 11897 2009-02-09 19:28:02Z barras $ *)
+(* $Id: evarconv.ml 12205 2009-06-22 16:10:15Z barras $ *)
 
 open Pp
 open Util
@@ -474,11 +474,11 @@ and conv_record env evd (c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2)) =
   let (evd',ks,_) =
     List.fold_left
       (fun (i,ks,m) b ->
-	 if m=0 then (i,t2::ks, n-1) else
+	 if m=n then (i,t2::ks, m-1) else
 	 let dloc = (dummy_loc,InternalHole) in
          let (i',ev) = new_evar i env ~src:dloc (substl ks b) in
-	 (i', ev :: ks, n - 1))
-      (evd,[],n) bs
+	 (i', ev :: ks, m - 1))
+      (evd,[],List.length bs - 1) bs
   in
   ise_and evd'
     [(fun i ->
@@ -505,7 +505,7 @@ let first_order_unification env evd (ev1,l1) (term2,l2) =
       if is_defined_evar i ev1 then
 	evar_conv_x env i CONV t2 (mkEvar ev1)
       else
-	solve_simple_eqn evar_conv_x env i (CONV,ev1,t2))]
+	solve_simple_eqn ~choose:true evar_conv_x env i (CONV,ev1,t2))]
 
 let choose_less_dependent_instance evk evd term args =
   let evi = Evd.find (evars_of evd) evk in
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index c0c0b941..994da427 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: evarutil.ml 11897 2009-02-09 19:28:02Z barras $ *)
+(* $Id: evarutil.ml 12107 2009-04-25 19:58:24Z herbelin $ *)
 
 open Util
 open Pp
@@ -673,7 +673,11 @@ let invert_arg_from_subst env k sigma subst_in_env c_in_env_extended_with_k_bind
 
 let invert_arg env k sigma (evk,args_in_env) c_in_env_extended_with_k_binders =
   let subst_in_env = make_projectable_subst sigma (Evd.find sigma evk) args_in_env in
-  invert_arg_from_subst env k sigma subst_in_env c_in_env_extended_with_k_binders
+  let res = invert_arg_from_subst env k sigma subst_in_env c_in_env_extended_with_k_binders in
+  match res with
+  | Invertible (UniqueProjection (c,_)) when occur_evar evk c -> CannotInvert
+  | _ -> res
+
 
 let effective_projections =
   map_succeed (function Invertible c -> c | _ -> failwith"")
@@ -836,7 +840,7 @@ let expand_rhs env sigma subst rhs =
 exception NotInvertibleUsingOurAlgorithm of constr
 exception NotEnoughInformationToProgress
 
-let rec invert_definition env evd (evk,argsv as ev) rhs =
+let rec invert_definition choose env evd (evk,argsv as ev) rhs =
   let evdref = ref evd in
   let progress = ref false in
   let evi = Evd.find (evars_of evd) evk in
@@ -847,7 +851,11 @@ let rec invert_definition env evd (evk,argsv as ev) rhs =
     (* Evar/Var problem: unifiable iff variable projectable from ev subst *)
     try 
       let sols = find_projectable_vars true env (evars_of !evdref) t subst in
-      let c, p = filter_solution sols in
+      let c, p = match sols with
+	| [] -> raise Not_found
+	| [id,p] -> (mkVar id, p)
+	| (id,p)::_::_ -> if choose then (mkVar id, p) else raise NotUnique
+      in
       let ty = lazy (Retyping.get_type_of env (evars_of !evdref) t) in
       let evd = do_projection_effects evar_define env ty !evdref p in
       evdref := evd;
@@ -923,9 +931,9 @@ and occur_existential evm c =
     | _ -> iter_constr occrec c
   in try occrec c; false with Occur -> true
 
-and evar_define env (evk,_ as ev) rhs evd =
+and evar_define ?(choose=false) env (evk,_ as ev) rhs evd =
   try
-    let (evd',body) = invert_definition env evd ev rhs in
+    let (evd',body) = invert_definition choose env evd ev rhs in
     if occur_meta body then error "Meta cannot occur in evar body.";
     (* invert_definition may have instantiate some evars of rhs with evk *)
     (* so we recheck acyclicity *)
@@ -1120,7 +1128,7 @@ let solve_refl conv_algo env evd evk argsv1 argsv2 =
  * if the problem couldn't be solved. *)
 
 (* Rq: uncomplete algorithm if pbty = CONV_X_LEQ ! *)
-let solve_simple_eqn conv_algo env evd (pbty,(evk1,args1 as ev1),t2) =
+let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1),t2) =
   try
     let t2 = whd_evar (evars_of evd) t2 in
     let evd = match kind_of_term t2 with
@@ -1132,15 +1140,18 @@ let solve_simple_eqn conv_algo env evd (pbty,(evk1,args1 as ev1),t2) =
 	    then solve_evar_evar evar_define env evd ev1 ev2
 	    else add_conv_pb (pbty,env,mkEvar ev1,t2) evd
       | _ ->
-	  let evd = evar_define env ev1 t2 evd in
+	  let evd = evar_define ~choose env ev1 t2 evd in
 	  let evm = evars_of evd in
 	  let evi = Evd.find evm evk1 in
 	    if occur_existential evm evi.evar_concl then
 	      let evenv = evar_env evi in
 	      let evc = nf_isevar evd evi.evar_concl in
-	      let body = match evi.evar_body with Evar_defined b -> b | Evar_empty -> assert false in
-	      let ty = nf_isevar evd (Retyping.get_type_of_with_meta evenv evm (metas_of evd) body) in
-		add_conv_pb (Reduction.CUMUL,evenv,ty,evc) evd
+		match evi.evar_body with 
+		| Evar_defined body -> 
+		    let ty = nf_isevar evd (Retyping.get_type_of_with_meta evenv evm (metas_of evd) body) in
+		      add_conv_pb (Reduction.CUMUL,evenv,ty,evc) evd
+		| Evar_empty -> (* Resulted in a constraint *) 
+		    evd
 	    else evd
     in
     let (evd,pbs) = extract_changed_conv_pbs evd status_changed in
@@ -1251,8 +1262,8 @@ let define_evar_as_abstraction abs evd (ev,args) =
   let evrng =
     fst (destEvar rng), array_cons (mkRel 1) (Array.map (lift 1) args) in
   let prod' = abs (Name nvar, mkEvar evdom, mkEvar evrng) in
-  (evd3,prod')
-
+    (evd3,prod')
+      
 let define_evar_as_product evd (ev,args) =
   define_evar_as_abstraction (fun t -> mkProd t) evd (ev,args)
 
@@ -1263,7 +1274,6 @@ let define_evar_as_sort evd (ev,args) =
   let s = new_Type () in
   Evd.evar_define ev s evd, destSort s
 
-
 (* We don't try to guess in which sort the type should be defined, since
    any type has type Type. May cause some trouble, but not so far... *)
 
@@ -1275,27 +1285,26 @@ let judge_of_new_Type () = Typeops.judge_of_type (new_univ ())
    an evar instantiate it with the product of 2 new evars. *)
 
 let split_tycon loc env evd tycon = 
-  let rec real_split c = 
-    let sigma = evars_of evd in
-    let t = whd_betadeltaiota env sigma c in
+  let rec real_split evd c = 
+    let t = whd_betadeltaiota env (Evd.evars_of evd) c in
       match kind_of_term t with
 	| Prod (na,dom,rng) -> evd, (na, dom, rng)
 	| Evar ev when not (Evd.is_defined_evar evd ev) ->
 	    let (evd',prod) = define_evar_as_product evd ev in
 	    let (_,dom,rng) = destProd prod in
 	      evd',(Anonymous, dom, rng)
-	| _ -> error_not_product_loc loc env sigma c
+	| _ -> error_not_product_loc loc env (Evd.evars_of evd) c
   in
     match tycon with
       | None -> evd,(Anonymous,None,None)
       | Some (abs, c) ->
 	  (match abs with
 	       None -> 
-		 let evd', (n, dom, rng) = real_split c in
+		 let evd', (n, dom, rng) = real_split evd c in
 		   evd', (n, mk_tycon dom, mk_tycon rng)
 	     | Some (init, cur) ->
 		 if cur = 0 then 
-		   let evd', (x, dom, rng) = real_split c in
+		   let evd', (x, dom, rng) = real_split evd c in
 		     evd, (Anonymous, 
 			  Some (None, dom), 
 			  Some (None, rng))
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index a687fdf0..cb54f400 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: evarutil.mli 11745 2009-01-04 18:43:08Z herbelin $ i*)
+(*i $Id: evarutil.mli 12053 2009-04-06 16:20:42Z msozeau $ i*)
 
 (*i*)
 open Util
@@ -53,11 +53,11 @@ val make_pure_subst : evar_info -> constr array -> (identifier * constr) list
 (***********************************************************)
 (* Instantiate evars *)
 
-(* [evar_define env ev c] try to instantiate [ev] with [c] (typed in [env]),
+(* [evar_define choose env ev c] try to instantiate [ev] with [c] (typed in [env]),
    possibly solving related unification problems, possibly leaving open
-   some problems that cannot be solved in a unique way;
-   failed if the instance is not valid for the given [ev] *)
-val evar_define : env -> existential -> constr -> evar_defs -> evar_defs
+   some problems that cannot be solved in a unique way (except if choose is
+   true); fails if the instance is not valid for the given [ev] *)
+val evar_define : ?choose:bool -> env -> existential -> constr -> evar_defs -> evar_defs
 
 (***********************************************************)
 (* Evars/Metas switching... *)
@@ -80,7 +80,7 @@ val solve_refl :
     evar_defs
 val solve_simple_eqn :
   (env ->  evar_defs -> conv_pb -> constr -> constr -> evar_defs * bool)
-  -> env ->  evar_defs -> conv_pb * existential * constr ->
+  -> ?choose:bool -> env ->  evar_defs -> conv_pb * existential * constr ->
     evar_defs * bool
 
 (* [check_evars env initial_sigma extended_sigma c] fails if some
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 1cac9011..c0f820a2 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: pretyping.ml 11576 2008-11-10 19:13:15Z msozeau $ *)
+(* $Id: pretyping.ml 12053 2009-04-06 16:20:42Z msozeau $ *)
 
 open Pp
 open Util
@@ -443,7 +443,13 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	  inh_conv_coerce_to_tycon loc env evdref resj tycon
 	    
     | RLetIn(loc,name,c1,c2)      ->
-	let j = pretype empty_tycon env evdref lvar c1 in
+	let j = 
+	  match c1 with
+	  | RCast (loc, c, CastConv (DEFAULTcast, t)) ->
+	      let tj = pretype_type empty_valcon env evdref lvar t in		
+		pretype (mk_tycon tj.utj_val) env evdref lvar c
+	  | _ -> pretype empty_tycon env evdref lvar c1
+	in
 	let t = refresh_universes j.uj_type in
 	let var = (name,Some j.uj_val,t) in
         let tycon = lift_tycon 1 tycon in
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 7c4023b9..711f332e 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: recordops.ml 11576 2008-11-10 19:13:15Z msozeau $ *)
+(* $Id: recordops.ml 12187 2009-06-13 19:36:59Z msozeau $ *)
 
 open Util
 open Pp
@@ -65,8 +65,11 @@ let subst_structure (_,subst,((kn,i),id,kl,projs as obj)) =
     if projs' == projs && kn' == kn && id' == id then obj else
       ((kn',i),id',kl,projs')
 
+let discharge_constructor (ind, n) = 
+  (Lib.discharge_inductive ind, n)
+
 let discharge_structure (_,(ind,id,kl,projs)) =
-  Some (Lib.discharge_inductive ind, id, kl,
+  Some (Lib.discharge_inductive ind, discharge_constructor id, kl,
         List.map (Option.map Lib.discharge_con) projs)
 
 let (inStruc,outStruc) =
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index f93212f8..4f38fbb3 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: termops.ml 11639 2008-11-27 17:48:32Z barras $ *)
+(* $Id: termops.ml 12058 2009-04-08 10:54:59Z herbelin $ *)
 
 open Pp
 open Util
@@ -1017,6 +1017,15 @@ let assums_of_rel_context sign =
         | None -> (na, t)::l)
     sign ~init:[]
 
+let fold_map_rel_context f env sign =
+  let rec aux env acc = function
+    | d::sign ->
+	aux (push_rel d env) (map_rel_declaration (f env) d :: acc) sign
+    | [] ->
+	acc
+  in
+  aux env [] (List.rev sign)
+
 let map_rel_context_with_binders f sign =
   let rec aux k = function
     | d::sign -> map_rel_declaration (f k) d :: aux (k-1) sign
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index d44c762e..e0bbe7b5 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: termops.mli 11639 2008-11-27 17:48:32Z barras $ i*)
+(*i $Id: termops.mli 12058 2009-04-08 10:54:59Z herbelin $ i*)
 
 open Util
 open Pp
@@ -241,6 +241,8 @@ val process_rel_context : (rel_declaration -> env -> env) -> env -> env
 val assums_of_rel_context : rel_context -> (name * constr) list
 val lift_rel_context : int -> rel_context -> rel_context
 val substl_rel_context : constr list -> rel_context -> rel_context
+val fold_map_rel_context :
+  (env -> constr -> constr) -> env -> rel_context -> rel_context
 val map_rel_context_with_binders : 
   (int -> constr -> constr) -> rel_context -> rel_context
 val fold_named_context_both_sides :
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 8680e578..216a0611 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -7,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: typeclasses.ml 11576 2008-11-10 19:13:15Z msozeau $ i*)
+(*i $Id: typeclasses.ml 12189 2009-06-15 05:08:44Z msozeau $ i*)
 
 (*i*)
 open Names
@@ -381,7 +381,7 @@ let solve_instanciation_problem = ref (fun _ _ _ -> assert false)
 let resolve_typeclasses ?(onlyargs=false) ?(split=true) ?(fail=true) env evd =
   if not (has_typeclasses (Evd.evars_of evd)) then evd
   else
-    !solve_instanciations_problem env (Evarutil.nf_evar_defs evd) onlyargs split fail
+    !solve_instanciations_problem env evd onlyargs split fail
 
 let resolve_one_typeclass env evm t =
   !solve_instanciation_problem env evm t
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index fb29196c..bfd601e2 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: unification.ml 11897 2009-02-09 19:28:02Z barras $ *)
+(* $Id: unification.ml 12163 2009-06-06 17:36:47Z herbelin $ *)
 
 open Pp
 open Util
@@ -492,7 +492,7 @@ let w_coerce env evd mv c =
 let unify_to_type env evd flags c u =
   let sigma = evars_of evd in
   let c = refresh_universes c in
-  let t = get_type_of_with_meta env sigma (metas_of evd) c in
+  let t = get_type_of_with_meta env sigma (List.map (on_snd (nf_meta evd)) (metas_of evd)) (nf_meta evd c) in
   let t = Tacred.hnf_constr env sigma (nf_betaiota sigma (nf_meta evd t)) in
   let u = Tacred.hnf_constr env sigma u in
   try unify_0 env sigma Cumul flags t u
@@ -500,7 +500,7 @@ let unify_to_type env evd flags c u =
 
 let unify_type env evd flags mv c =
   let mvty = Typing.meta_type evd mv in
-  if occur_meta_or_existential mvty then
+  if occur_meta_or_existential mvty or is_arity env (evars_of evd) mvty then
     unify_to_type env evd flags c mvty
   else ([],[])