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

9 files changed, 144 insertions, 57 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index c2d8921e..abe4fcc1 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: cases.ml 12167 2009-06-06 20:07:22Z herbelin $ *)
+(* $Id: cases.ml 13112 2010-06-10 19:58:23Z herbelin $ *)
 
 open Util
 open Names
@@ -851,7 +851,7 @@ let rec map_predicate f k ccl = function
   | Abstract _ :: rest ->
       map_predicate f (k+1) ccl rest
 
-let noccurn_predicate = map_predicate noccurn
+let noccur_predicate_between n = map_predicate (noccur_between n)
 
 let liftn_predicate n = map_predicate (liftn n)
 
@@ -1122,13 +1122,16 @@ let build_branch current deps (realnames,dep) pb eqns const_info =
   (* into  "Gamma; typs; curalias |- tms" *)
   let tomatch = lift_tomatch_stack const_info.cs_nargs pb.tomatch in
 
+  let pred_is_not_dep =
+    noccur_predicate_between 1 (List.length realnames + 1) pb.pred tomatch in
+
   let typs'' = 
     list_map2_i
       (fun i (na,t) deps ->
 	let dep = match dep with
 	  | Name _ as na',k -> (if na <> Anonymous then na else na'),k
 	  | Anonymous,KnownNotDep ->
-	      if deps = [] && noccurn_predicate 1 pb.pred tomatch then
+	      if deps = [] && pred_is_not_dep then
 		(Anonymous,KnownNotDep)
 	      else
 		(force_name na,KnownDep)
@@ -1801,7 +1804,8 @@ let prepare_predicate loc typing_fun evdref env tomatchs sign tycon pred =
 	   let t2 = mkExistential env ~src:(loc, CasesType) evdref2 in
            let arsign = extract_arity_signature env tomatchs sign in
            let names2 = List.rev (List.map (List.map pi1) arsign) in
-	   let nal2,pred2 = build_initial_predicate KnownNotDep names2 t2 in
+           let pred2 = lift (List.length names2) t2 in
+	   let nal2,pred2 = build_initial_predicate KnownNotDep names2 pred2 in
 	   [evdref, nal1, pred1; evdref2, nal2, pred2])
 
   (* Some type annotation *)
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index 51952f4f..0bfef04a 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: clenv.ml 11897 2009-02-09 19:28:02Z barras $ *)
+(* $Id: clenv.ml 13126 2010-06-13 11:09:51Z herbelin $ *)
 
 open Pp
 open Util
@@ -410,8 +410,9 @@ let clenv_unify_binding_type clenv c t u =
     try
       let evd,c = w_coerce_to_type (cl_env clenv) clenv.evd c t u in
       TypeProcessed, { clenv with evd = evd }, c
-    with e when precatchable_exception e ->
-      TypeNotProcessed, clenv, c
+    with
+      | PretypeError (_,NotClean _) as e -> raise e
+      | e when precatchable_exception e -> TypeNotProcessed, clenv, c
 
 let clenv_assign_binding clenv k (sigma,c) =
   let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in
@@ -436,11 +437,11 @@ let clenv_match_args bl clenv =
 	  clenv_assign_binding clenv k sc)
       clenv bl
 
+exception NoSuchBinding
+
 let clenv_constrain_last_binding c clenv =
   let all_mvs = collect_metas clenv.templval.rebus in
-  let k =
-    try list_last all_mvs 
-    with Failure _ -> anomaly "clenv_constrain_with_bindings" in
+  let k = try list_last all_mvs with Failure _ -> raise NoSuchBinding in
   clenv_assign_binding clenv k (Evd.empty,c)
 
 let clenv_constrain_dep_args hyps_only bl clenv =
diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli
index 9b2d6e29..4c5535b3 100644
--- a/pretyping/clenv.mli
+++ b/pretyping/clenv.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: clenv.mli 10856 2008-04-27 16:15:34Z herbelin $ i*)
+(*i $Id: clenv.mli 13126 2010-06-13 11:09:51Z herbelin $ i*)
 
 (*i*)
 open Util
@@ -94,6 +94,8 @@ type arg_bindings = open_constr explicit_bindings
 val clenv_independent : clausenv -> metavariable list
 val clenv_missing : clausenv -> metavariable list
 
+(** for the purpose of inversion tactics *)
+exception NoSuchBinding
 val clenv_constrain_last_binding : constr -> clausenv -> clausenv
 
 (* defines metas corresponding to the name of the bindings *)
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 73dc5d46..20cbba94 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: detyping.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: detyping.ml 12887 2010-03-27 15:57:02Z herbelin $ *)
 
 open Pp
 open Util
@@ -329,7 +329,6 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl =
             n, aliastyp, Some typ
   in
   let constructs = Array.init (Array.length bl) (fun i -> (indsp,i+1)) in
-  let eqnl = detype_eqns constructs consnargsl bl in
   let tag =
     try 
       if !Flags.raw_print then
@@ -357,8 +356,10 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl =
 	RIf (dl,tomatch,(alias,pred),
              Option.get nondepbrs.(0),Option.get nondepbrs.(1))
       else
+	let eqnl = detype_eqns constructs consnargsl bl in
 	RCases (dl,tag,pred,[tomatch,(alias,aliastyp)],eqnl)
   | _ ->
+      let eqnl = detype_eqns constructs consnargsl bl in
       RCases (dl,tag,pred,[tomatch,(alias,aliastyp)],eqnl)
 
 let detype_sort = function
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 043a326d..18e79e85 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: evarconv.ml 12205 2009-06-22 16:10:15Z barras $ *)
+(* $Id: evarconv.ml 12268 2009-08-11 09:02:16Z herbelin $ *)
 
 open Pp
 open Util
@@ -66,6 +66,10 @@ let apprec_nohdbeta env evd c =
     | (Case _ | Fix _) -> applist (evar_apprec env evd [] c)
     | _ -> c
 
+let position_problem l2r = function
+  | CONV -> None
+  | CUMUL -> Some l2r
+
 (* [check_conv_record (t1,l1) (t2,l2)] tries to decompose the problem
    (t1 l1) = (t2 l2) into a problem
 
@@ -177,9 +181,11 @@ let rec evar_conv_x env evd pbty term1 term2 =
         let term1 = apprec_nohdbeta env evd term1 in
         let term2 = apprec_nohdbeta env evd term2 in
         if is_undefined_evar evd term1 then
-          solve_simple_eqn evar_conv_x env evd (pbty,destEvar term1,term2)
+          solve_simple_eqn evar_conv_x env evd
+	    (position_problem true pbty,destEvar term1,term2)
         else if is_undefined_evar evd term2 then
-          solve_simple_eqn evar_conv_x env evd (pbty,destEvar term2,term1)
+          solve_simple_eqn evar_conv_x env evd
+	    (position_problem false pbty,destEvar term2,term1)
         else
           evar_eqappr_x env evd pbty
             (decompose_app term1) (decompose_app term2)
@@ -193,14 +199,14 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
             let (deb1,rest1) = list_chop (List.length l1-List.length l2) l1 in
             ise_and i
               [(fun i -> solve_simple_eqn evar_conv_x env i
-	        (pbty,ev2,applist(term1,deb1)));
+	        (position_problem false pbty,ev2,applist(term1,deb1)));
               (fun i -> ise_list2 i
                   (fun i -> evar_conv_x env i CONV) rest1 l2)]
 	  else
 	    let (deb2,rest2) = list_chop (List.length l2-List.length l1) l2 in
             ise_and i
               [(fun i -> solve_simple_eqn evar_conv_x env i
-	          (pbty,ev1,applist(term2,deb2)));
+	          (position_problem true pbty,ev1,applist(term2,deb2)));
               (fun i -> ise_list2 i
                   (fun i -> evar_conv_x env i CONV) l1 rest2)]
 	and f2 i =
@@ -224,7 +230,8 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	    (* Preserve generality (except that CCI has no eta-conversion) *)
 	    let t2 = nf_evar (evars_of evd) (applist appr2) in
 	    let t2 = solve_pattern_eqn env l1 t2 in
-	    solve_simple_eqn evar_conv_x env evd (pbty,ev1,t2)
+	    solve_simple_eqn evar_conv_x env evd
+	      (position_problem true pbty,ev1,t2)
 	  else if
             List.length l1 <= List.length l2
 	  then
@@ -256,7 +263,8 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	    (* Preserve generality (except that CCI has no eta-conversion) *)
 	    let t1 = nf_evar (evars_of evd) (applist appr1) in
 	    let t1 = solve_pattern_eqn env l2 t1 in
-	    solve_simple_eqn evar_conv_x env evd (pbty,ev2,t1)
+	    solve_simple_eqn evar_conv_x env evd
+	      (position_problem false pbty,ev2,t1)
 	  else if
        	    List.length l2 <= List.length l1
 	  then
@@ -324,7 +332,8 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	  (* Preserve generality (except that CCI has no eta-conversion) *)
 	  let t2 = nf_evar (evars_of evd) (applist appr2) in
 	  let t2 = solve_pattern_eqn env l1 t2 in
-	  solve_simple_eqn evar_conv_x env evd (pbty,ev1,t2)
+	  solve_simple_eqn evar_conv_x env evd
+	    (position_problem true pbty,ev1,t2)
 	else
 	  (* Postpone the use of an heuristic *)
 	  add_conv_pb (pbty,env,applist appr1,applist appr2) evd,
@@ -339,7 +348,8 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	  (* Preserve generality (except that CCI has no eta-conversion) *)
 	  let t1 = nf_evar (evars_of evd) (applist appr1) in
 	  let t1 = solve_pattern_eqn env l2 t1 in
-	  solve_simple_eqn evar_conv_x env evd (pbty,ev2,t1)
+	  solve_simple_eqn evar_conv_x env evd
+	    (position_problem false pbty,ev2,t1)
 	else
 	  (* Postpone the use of an heuristic *)
 	  add_conv_pb (pbty,env,applist appr1,applist appr2) evd,
@@ -505,7 +515,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 ~choose:true evar_conv_x env i (CONV,ev1,t2))]
+	solve_simple_eqn ~choose:true evar_conv_x env i (None,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 994da427..fbaac79b 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: evarutil.ml 12107 2009-04-25 19:58:24Z herbelin $ *)
+(* $Id: evarutil.ml 13116 2010-06-12 15:18:07Z herbelin $ *)
 
 open Util
 open Pp
@@ -113,11 +113,27 @@ let push_dependent_evars sigma emap =
       (sigma',emap') (collect_evars emap' ccl))
     emap (sigma,emap)
 
+let push_duplicated_evars sigma emap c	=
+  let rec collrec (one,(sigma,emap) as acc) c =
+    match kind_of_term c with
+    | Evar (evk,_) when not (Evd.mem sigma evk) ->
+       if List.mem evk one then
+         let sigma' = Evd.add sigma evk (Evd.find emap	evk) in
+         let emap' = Evd.remove emap evk in
+         (one,(sigma',emap'))
+       else
+         (evk::one,(sigma,emap))
+    | _ ->
+       fold_constr collrec acc	c
+  in   
+  snd (collrec ([],(sigma,emap)) c)
+
 (* replaces a mapping of existentials into a mapping of metas.
    Problem if an evar appears in the type of another one (pops anomaly) *)
 let evars_to_metas sigma (emap, c) =
   let emap = nf_evars emap in
   let sigma',emap' = push_dependent_evars sigma emap in
+  let sigma',emap' = push_duplicated_evars sigma' emap' c in
   let change_exist evar =
     let ty = nf_betaiota emap (existential_type emap evar) in
     let n = new_meta() in
@@ -559,6 +575,7 @@ let rec expansions_of_var env x =
  *)
 
 exception NotUnique
+exception NotUniqueInType of types
 
 type evar_projection = 
 | ProjectVar 
@@ -570,12 +587,13 @@ let rec find_projectable_vars with_evars env sigma y subst =
     if y = y' or expand_var env y = expand_var env y'
     then (idc,(y'=y,(id,ProjectVar)))
     else if with_evars & isEvar y' then
+      (* TODO: infer conditions for being of unifiable types *)
       let (evk,argsv as t) = destEvar y' in
       let evi = Evd.find sigma evk in
       let subst = make_projectable_subst sigma evi argsv in
       let l = find_projectable_vars with_evars env sigma y subst in
       match l with 
-      | [id',p] -> (idc,(true,(id,ProjectEvar (t,evi,id',p))))
+      | [id',p] -> (idc,(true,(id,ProjectEvar(t,evi,id',p))))
       | _ -> failwith ""
     else failwith "" in
   let l = map_succeed is_projectable subst in
@@ -596,6 +614,12 @@ let project_with_effects env sigma effects t subst =
   effects := p :: !effects;
   c
 
+let rec find_solution_type evarenv = function
+  | (id,ProjectVar)::l -> pi3 (lookup_named id evarenv)
+  | [id,ProjectEvar _] -> (* bugged *) pi3 (lookup_named id evarenv)
+  | (id,ProjectEvar _)::l -> find_solution_type evarenv l
+  | [] -> assert false
+
 (* In case the solution to a projection problem requires the instantiation of
  * subsidiary evars, [do_projection_effects] performs them; it
  * also try to instantiate the type of those subsidiary evars if their
@@ -709,7 +733,7 @@ let filter_along f projs v =
  * such that "hyps' |- ?e : T"
  *)
 
-let do_restrict_hyps_virtual evd evk filter =
+let restrict_hyps evd evk filter =
     (* What to do with dependencies?
        Assume we have x:A, y:B(x), z:C(x,y) |- ?e:T(x,y,z) and restrict on y.
        - If y is in a non-erasable position in C(x,y) (i.e. it is not below an
@@ -726,15 +750,15 @@ let do_restrict_hyps_virtual evd evk filter =
     let filter,_ = List.fold_right (fun oldb (l,filter) ->
       if oldb then List.hd filter::l,List.tl filter else (false::l,filter))
       oldfilter ([],List.rev filter) in
-    new_evar evd env ~src:(evar_source evk evd)
-      ~filter:filter evi.evar_concl
+    (env,evar_source evk evd,filter,evi.evar_concl)
 
 let do_restrict_hyps evd evk projs =
   let filter = List.map filter_of_projection projs in
   if List.for_all (fun x -> x) filter then
     evd,evk
   else
-    let evd,nc = do_restrict_hyps_virtual evd evk filter in
+    let env,src,filter,ccl = restrict_hyps evd evk filter in
+    let evd,nc = new_evar evd env ~src ~filter ccl in
     let evd = Evd.evar_define evk nc evd in
     let evk',_ = destEvar nc in
     evd,evk'
@@ -854,7 +878,9 @@ let rec invert_definition choose env evd (evk,argsv as ev) rhs =
       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
+	| (id,p)::_::_ ->
+	    if choose then (mkVar id, p)
+	    else raise (NotUniqueInType(find_solution_type (evar_env evi) sols))
       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
@@ -862,14 +888,15 @@ let rec invert_definition choose env evd (evk,argsv as ev) rhs =
       c
     with
       | Not_found -> raise (NotInvertibleUsingOurAlgorithm t)
-      | NotUnique ->
+      | NotUniqueInType ty ->
 	  if not !progress then raise NotEnoughInformationToProgress;
 	  (* No unique projection but still restrict to where it is possible *)
 	  let ts = expansions_of_var env t in
 	  let test c = isEvar c or List.mem c ts in
 	  let filter = array_map_to_list test argsv in
 	  let args' = filter_along (fun x -> x) filter argsv in
-	  let evd,evar = do_restrict_hyps_virtual !evdref evk filter in
+	  let evarenv,src,filter,_ = restrict_hyps !evdref evk filter in
+	  let evd,evar = new_evar !evdref evarenv ~src ~filter ty in
 	  let evk',_ = destEvar evar in
 	  let pb = (Reduction.CONV,env,mkEvar(evk',args'),t) in
 	  evdref := Evd.add_conv_pb pb evd;
@@ -1122,6 +1149,24 @@ let solve_refl conv_algo env evd evk argsv1 argsv2 =
   let pb = (Reduction.CONV,env,mkEvar(evk,argsv1),mkEvar(evk,argsv2)) in
   Evd.add_conv_pb pb evd
 
+(* Util *)
+
+let check_instance_type conv_algo env evd ev1 t2 =
+  let t2 = nf_evar (evars_of evd) t2 in
+  if has_undefined_evars evd t2 then
+    (* May contain larger constraints than needed: don't want to
+       commit to an equal solution while only subtyping is requested *)
+    evd
+  else
+    let typ2 = Retyping.get_type_of env (evars_of evd) (refresh_universes t2) in
+    if isEvar typ2 then (* Don't want to commit too early too *) evd
+    else
+      let typ1 = existential_type (evars_of evd) ev1 in
+      let evd,b = conv_algo env evd Reduction.CUMUL typ2 typ1 in
+      if b then evd else
+	user_err_loc (fst (evar_source (fst ev1) evd),"",
+	  str "Unable to find a well-typed instantiation")
+
 (* Tries to solve problem t1 = t2.
  * Precondition: t1 is an uninstantiated evar
  * Returns an optional list of evars that were instantiated, or None
@@ -1136,15 +1181,23 @@ let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1)
 	  if evk1 = evk2 then
 	    solve_refl conv_algo env evd evk1 args1 args2
 	  else
-	    if pbty = Reduction.CONV 
+	    if pbty = None
 	    then solve_evar_evar evar_define env evd ev1 ev2
-	    else add_conv_pb (pbty,env,mkEvar ev1,t2) evd
+	    else if pbty = Some true then
+	      add_conv_pb (Reduction.CUMUL,env,mkEvar ev1,t2) evd
+	    else
+	      add_conv_pb (Reduction.CUMUL,env,t2,mkEvar ev1) evd
       | _ ->
+	  let evd =
+	    if pbty = Some false then
+	      check_instance_type conv_algo env evd ev1 t2 
+	    else
+	      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 evenv = evar_unfiltered_env evi in
 	      let evc = nf_isevar evd evi.evar_concl in
 		match evi.evar_body with 
 		| Evar_defined body -> 
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index cb54f400..eef41da3 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 12053 2009-04-06 16:20:42Z msozeau $ i*)
+(*i $Id: evarutil.mli 12268 2009-08-11 09:02:16Z herbelin $ i*)
 
 (*i*)
 open Util
@@ -80,7 +80,7 @@ val solve_refl :
     evar_defs
 val solve_simple_eqn :
   (env ->  evar_defs -> conv_pb -> constr -> constr -> evar_defs * bool)
-  -> ?choose:bool -> env ->  evar_defs -> conv_pb * existential * constr ->
+  -> ?choose:bool -> env ->  evar_defs -> bool option * existential * constr ->
     evar_defs * bool
 
 (* [check_evars env initial_sigma extended_sigma c] fails if some
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 740b2ca8..f579afa6 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: tacred.ml 11897 2009-02-09 19:28:02Z barras $ *)
+(* $Id: tacred.ml 12233 2009-07-08 22:50:56Z herbelin $ *)
 
 open Pp
 open Util
@@ -137,20 +137,27 @@ let _ =
       Summary.survive_module = false;
       Summary.survive_section = false }
 
-(* Check that c is an "elimination constant"
+(* [compute_consteval] determines whether c is an "elimination constant"
 
-   either [xn:An]..[x1:A1](<P>Case (Rel i) of f1..fk end g1 ..gp)
+   either [yn:Tn]..[y1:T1](match yi with f1..fk end g1 ..gp)
 
-   or     [xn:An]..[x1:A1](Fix(f|t) (Rel i1) ..(Rel ip))
-          with i1..ip distinct variables not occuring in t 
+   or     [yn:Tn]..[y1:T1](Fix(f|t) yi1..yip)
+          with yi1..yip distinct variables among the yi, not occurring in t 
 
-   In the second case, keep relevenant information ([i1,Ai1;..;ip,Aip],n)
-   in order to compute an equivalent of Fix(f|t)[xi<-ai] as 
+   In the second case, [check_fix_reversibility [T1;...;Tn] args fix] 
+   checks that [args] is a subset of disjoint variables in y1..yn (a necessary
+   condition for reversibility). It also returns the relevant
+   information ([i1,Ti1;..;ip,Tip],n) in order to compute an
+   equivalent of Fix(f|t) such that
 
-      [yip:Bip]..[yi1:Bi1](F bn..b1) 
-   == [yip:Bip]..[yi1:Bi1](Fix(f|t)[xi<-ai] (Rel p)..(Rel 1))
+   g := [xp:Tip']..[x1:Ti1'](f a1..an)
+     == [xp:Tip']..[x1:Ti1'](Fix(f|t) yi1..yip)
 
-   with bj=aj if j<>ik and bj=(Rel c) and Bic=Aic[xn..xic-1 <- an..aic-1]
+   with a_k:=y_k if k<>i_j, a_k:=args_k otherwise, and 
+   Tij':=Tij[x1..xi(j-1) <- a1..ai(j-1)]
+
+   Note that the types Tk, when no i_j=k, must not be dependent on
+   the xp..x1.
 *)
 
 let check_fix_reversibility labs args ((lv,i),(_,tys,bds)) =
@@ -172,8 +179,14 @@ let check_fix_reversibility labs args ((lv,i),(_,tys,bds)) =
          | _ -> 
 	     raise Elimconst) args
   in
-  if not (list_distinct (List.map fst li)) then 
+  let reversible_rels = List.map fst li in
+  if not (list_distinct reversible_rels) then 
     raise Elimconst;
+  list_iter_i (fun i t_i ->
+    if not (List.mem_assoc (i+1) li) then
+      let fvs = List.map ((+) (i+1)) (Intset.elements (free_rels t_i)) in
+      if list_intersect fvs reversible_rels <> [] then raise Elimconst)
+    labs;
   let k = lv.(i) in
   if k < nargs then
 (*  Such an optimisation would need eta-expansion 
@@ -294,19 +307,22 @@ let rev_firstn_liftn fn ln =
 (* If f is bound to EliminationFix (n',infos), then n' is the minimal
    number of args for starting the reduction and infos is
    (nbfix,[(yi1,Ti1);...;(yip,Tip)],n) indicating that f converts
-   to some [y1:T1,...,yn:Tn](Fix(..) yip .. yi1) where we can remark that
-   yij = Rel(n+1-j)
+   to some [y1:T1,...,yn:Tn](Fix(..) yip .. yi1) where the y_{i_j} consist in a
+   disjoint subset of the yi, i.e. 1 <= ij <= n and the ij are disjoint (in
+   particular, p <= n).
+
+   f is applied to largs := arg1 .. argn and we need for recursive
+   calls to build the function
 
-   f is applied to largs and we need for recursive calls to build the function
       g := [xp:Tip',...,x1:Ti1'](f a1 ... an)
 
    s.t. (g u1 ... up) reduces to (Fix(..) u1 ... up)
 
    This is made possible by setting 
-      a_k:=z_j    if k=i_j
-      a_k:=y_k    otherwise
+      a_k:=x_j    if k=i_j for some j
+      a_k:=arg_k  otherwise
 
-   The type Tij' is Tij[yn..yi(j-1)..y1 <- ai(j-1)..a1]
+   The type Tij' is Tij[yi(j-1)..y1 <- ai(j-1)..a1]
 *)
 
 let x = Name (id_of_string "x")
@@ -328,7 +344,7 @@ let make_elim_fun (names,(nbfix,lv,n)) largs =
       | Some (minargs,ref) ->
           let body = applistc (mkEvalRef ref) la in
           let g = 
-            list_fold_left_i (fun q (* j from comment is n+1-q *) c (ij,tij) ->
+            list_fold_left_i (fun q (* j = n+1-q *) c (ij,tij) ->
               let subst = List.map (lift (-q)) (list_firstn (n-ij) la) in
               let tij' = substl (List.rev subst) tij in
 	      mkLambda (x,tij',c)) 1 body (List.rev lv)
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index bfd601e2..c92f1fc6 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: unification.ml 12163 2009-06-06 17:36:47Z herbelin $ *)
+(* $Id: unification.ml 12268 2009-08-11 09:02:16Z herbelin $ *)
 
 open Pp
 open Util
@@ -517,7 +517,7 @@ let order_metas metas =
 (* Solve an equation ?n[x1=u1..xn=un] = t where ?n is an evar *)
 
 let solve_simple_evar_eqn env evd ev rhs =
-  let evd,b = solve_simple_eqn Evarconv.evar_conv_x env evd (CONV,ev,rhs) in
+  let evd,b = solve_simple_eqn Evarconv.evar_conv_x env evd (None,ev,rhs) in
   if not b then error_cannot_unify env (evars_of evd) (mkEvar ev,rhs);
   let (evd,b) = Evarconv.consider_remaining_unif_problems env evd in
   if not b then error "Cannot solve unification constraints";