Imported Upstream version 8.2~beta4+dfsgupstream/8.2.beta4+dfsg

31 files changed, 315 insertions, 358 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 1d7da3f3..9482bf92 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: cases.ml 11085 2008-06-10 08:54:43Z herbelin $ *)
+(* $Id: cases.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
 
 open Util
 open Names
@@ -114,8 +114,8 @@ let force_name =
 
 open Pp
 
-let mssg_may_need_inversion () =
-  str "Found a matching with no clauses on a term unknown to have an empty inductive type"
+let msg_may_need_inversion () =
+  strbrk "Found a matching with no clauses on a term unknown to have an empty inductive type."
 
 (* Utils *)
 let make_anonymous_patvars n =
@@ -535,7 +535,7 @@ let set_used_pattern eqn = eqn.used := true
 
 let extract_rhs pb =
   match pb.mat with 
-    | [] -> errorlabstrm "build_leaf" (mssg_may_need_inversion())
+    | [] -> errorlabstrm "build_leaf" (msg_may_need_inversion())
     | eqn::_ ->
 	set_used_pattern eqn;
         eqn.rhs
@@ -1654,7 +1654,7 @@ let extract_arity_signature env0 tomatchl tmsign =
 	    | None -> [na,Option.map (lift n) bo,lift n typ]
 	    | Some (loc,_,_,_) -> 
  	    user_err_loc (loc,"",
-	    str "Unexpected type annotation for a term of non inductive type"))
+	    str"Unexpected type annotation for a term of non inductive type."))
       | IsInd (term,IndType(indf,realargs),_) ->
           let indf' = lift_inductive_family n indf in
 	  let (ind,params) = dest_ind_family indf' in
@@ -1663,7 +1663,7 @@ let extract_arity_signature env0 tomatchl tmsign =
 	    match t with
 	      | Some (loc,ind',nparams,realnal) ->
 		  if ind <> ind' then
-		    user_err_loc (loc,"",str "Wrong inductive type");
+		    user_err_loc (loc,"",str "Wrong inductive type.");
 		  if List.length params <> nparams
 		    or nrealargs <> List.length realnal then
 		      anomaly "Ill-formed 'in' clause in cases";
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 83ba05bb..b5a5709e 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: classops.ml 10840 2008-04-23 21:29:34Z herbelin $ *)
+(* $Id: classops.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
 
 open Util
 open Pp
@@ -376,7 +376,7 @@ let coercion_of_reference r =
   let ref = Nametab.global r in
   if not (coercion_exists ref) then
     errorlabstrm "try_add_coercion" 
-      (Nametab.pr_global_env Idset.empty ref ++ str" is not a coercion");
+      (Nametab.pr_global_env Idset.empty ref ++ str" is not a coercion.");
   ref
 
 module CoercionPrinting =
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index 03f84809..8dfec2be 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: clenv.ml 11166 2008-06-22 13:23:35Z herbelin $ *)
+(* $Id: clenv.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
 
 open Pp
 open Util
@@ -377,11 +377,11 @@ let check_bindings bl =
     | NamedHyp s :: _ -> 
 	errorlabstrm ""
 	  (str "The variable " ++ pr_id s ++ 
-	   str " occurs more than once in binding list");
+	   str " occurs more than once in binding list.");
     | AnonHyp n :: _ ->
 	errorlabstrm ""
 	  (str "The position " ++ int n ++
-	   str " occurs more than once in binding list")
+	   str " occurs more than once in binding list.")
     | [] -> ()
 
 let meta_of_binder clause loc mvs = function
@@ -389,17 +389,17 @@ let meta_of_binder clause loc mvs = function
   | AnonHyp n ->
       try List.nth mvs (n-1)
       with (Failure _|Invalid_argument _) ->
-        errorlabstrm "" (str "No such binder")
+        errorlabstrm "" (str "No such binder.")
 
 let error_already_defined b =
   match b with
     | NamedHyp id ->
         errorlabstrm ""
           (str "Binder name \"" ++ pr_id id ++
-           str"\" already defined with incompatible value")
+           str"\" already defined with incompatible value.")
     | AnonHyp n ->
         anomalylabstrm ""
-          (str "Position " ++ int n ++ str" already defined")
+          (str "Position " ++ int n ++ str" already defined.")
 
 let clenv_unify_binding_type clenv c t u =
   if isMeta (fst (whd_stack u)) then
@@ -440,7 +440,7 @@ 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 _ -> error "clenv_constrain_with_bindings" in
+    with Failure _ -> anomaly "clenv_constrain_with_bindings" in
   clenv_assign_binding clenv k (Evd.empty,c)
 
 let clenv_constrain_dep_args hyps_only bl clenv =
@@ -451,8 +451,9 @@ let clenv_constrain_dep_args hyps_only bl clenv =
     if List.length occlist = List.length bl then
       List.fold_left2 clenv_assign_binding clenv occlist bl
     else 
-      error ("Not the right number of missing arguments (expected "
-	     ^(string_of_int (List.length occlist))^")")
+      errorlabstrm "" 
+	(strbrk "Not the right number of missing arguments (expected " ++
+	 int (List.length occlist) ++ str ").")
 
 (****************************************************************)
 (* Clausal environment for an application *)
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 3c37a49f..3074c4c4 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 10883 2008-05-05 13:55:24Z herbelin $ *)
+(* $Id: coercion.ml 11282 2008-07-28 11:51:53Z msozeau $ *)
 
 open Util
 open Names
@@ -43,6 +43,10 @@ module type S = sig
   val inh_coerce_to_base : loc ->
     env -> evar_defs -> unsafe_judgment -> evar_defs * unsafe_judgment
     
+  (* [inh_coerce_to_prod env isevars t] coerces [t] to a product type *)
+  val inh_coerce_to_prod : loc ->
+    env -> evar_defs -> type_constraint_type -> evar_defs * type_constraint_type
+
   (* [inh_conv_coerce_to loc env evd j t] coerces [j] to an object of type 
      [t]; i.e. it inserts a coercion into [j], if needed, in such a way [t] and
      [j.uj_type] are convertible; it fails if no coercion is applicable *)
@@ -160,6 +164,8 @@ module Default = struct
 
   let inh_coerce_to_base loc env evd j = (evd, j)
 
+  let inh_coerce_to_prod loc env evd t = (evd, t)
+
   let inh_coerce_to_fail env evd rigidonly v t c1 =
     if rigidonly & not (Heads.is_rigid env c1 && Heads.is_rigid env t)
     then
diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli
index b1c8e893..8705080f 100644
--- a/pretyping/coercion.mli
+++ b/pretyping/coercion.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: coercion.mli 10840 2008-04-23 21:29:34Z herbelin $ i*)
+(*i $Id: coercion.mli 11282 2008-07-28 11:51:53Z msozeau $ i*)
 
 (*i*)
 open Util
@@ -39,6 +39,10 @@ module type S = sig
      type its base type (the notion depends on the coercion system) *)
   val inh_coerce_to_base : loc ->
     env -> evar_defs -> unsafe_judgment -> evar_defs * unsafe_judgment
+
+  (* [inh_coerce_to_prod env isevars t] coerces [t] to a product type *)
+  val inh_coerce_to_prod : loc ->
+    env -> evar_defs -> type_constraint_type -> evar_defs * type_constraint_type
     
   (* [inh_conv_coerce_to loc env isevars j t] coerces [j] to an object of type 
      [t]; i.e. it inserts a coercion into [j], if needed, in such a way [t] and
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 81bb41ef..73dc5d46 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: detyping.ml 11073 2008-06-08 20:24:51Z herbelin $ *)
+(* $Id: detyping.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
 
 open Pp
 open Util
@@ -49,14 +49,14 @@ let encode_bool r =
   let (_,lc as x) = encode_inductive r in
   if not (has_two_constructors lc) then
     user_err_loc (loc_of_reference r,"encode_if",
-      str "This type has not exactly two constructors");
+      str "This type has not exactly two constructors.");
   x
 
 let encode_tuple r =
   let (_,lc as x) = encode_inductive r in
   if not (isomorphic_to_tuple lc) then
     user_err_loc (loc_of_reference r,"encode_tuple",
-      str "This type cannot be seen as a tuple type");
+      str "This type cannot be seen as a tuple type.");
   x
 
 module PrintingCasesMake =
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 58951302..323cd06f 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: evarconv.ml 11157 2008-06-21 10:45:51Z herbelin $ *)
+(* $Id: evarconv.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
 
 open Pp
 open Util
@@ -99,21 +99,21 @@ let check_conv_record (t1,l1) (t2,l2) =
 	      lookup_canonical_conversion 
 		(proji, Sort_cs (family_of_sort s)),[]
 	  | _ -> 
-	      let c2 = try global_of_constr t2 with _ -> raise Not_found in
+	      let c2 = global_of_constr t2 in
 		lookup_canonical_conversion (proji, Const_cs c2),l2
       with Not_found -> 
 	lookup_canonical_conversion (proji,Default_cs),[]
     in
-    let { o_DEF = c; o_INJ=n; o_TABS = bs; o_TPARAMS = params; o_TCOMPS = us } 
-	= canon_s in
+    let { o_DEF = c; o_INJ=n; o_TABS = bs; 
+          o_TPARAMS = params; o_NPARAMS = nparams; o_TCOMPS = us } = canon_s in
     let params1, c1, extra_args1 =
-      match list_chop (List.length params) l1 with 
+      match list_chop nparams l1 with 
 	| params1, c1::extra_args1 -> params1, c1, extra_args1
-	| _ -> assert false in
+	| _ -> raise Not_found in
     let us2,extra_args2 = list_chop (List.length us) l2_effective in
     c,bs,(params,params1),(us,us2),(extra_args1,extra_args2),c1,
     (n,applist(t2,l2))
-  with _ -> 
+  with Failure _ | Not_found -> 
     raise Not_found
 
 (* Precondition: one of the terms of the pb is an uninstantiated evar,
@@ -272,33 +272,42 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	ise_try evd [f1; f4]
 
     | MaybeFlexible flex1, MaybeFlexible flex2 ->
-	let f2 i =
-          if flex1 = flex2 then
-            ise_list2 i (fun i -> evar_conv_x env i CONV) l1 l2
-          else (i,false)
-	and f3 i =
+	let f1 i =
+	  if flex1 = flex2 then
+	    ise_list2 i (fun i -> evar_conv_x env i CONV) l1 l2
+	  else
+	     (i,false)
+	and f2 i =
 	  (try conv_record env i
              (try check_conv_record appr1 appr2
 	      with Not_found -> check_conv_record appr2 appr1)
            with Not_found -> (i,false))
-	and f4 i =
+	and f3 i =
           (* heuristic: unfold second argument first, exception made
              if the first argument is a beta-redex (expand a constant
-             only if necessary) *)
-          let val2 =
-            match kind_of_term flex1 with
-                Lambda _ -> None
-              | _ -> eval_flexible_term env flex2 in
-	  match val2 with
+             only if necessary) or the second argument is potentially
+             usable as a canonical projection *)
+	  if isLambda flex1 or is_open_canonical_projection (evars_of i) appr2
+	  then
+	    match eval_flexible_term env flex1 with
+	    | Some v1 ->
+		evar_eqappr_x env i pbty (evar_apprec env i l1 v1) appr2
+	    | None ->
+		match eval_flexible_term env flex2 with
+		| Some v2 ->
+		    evar_eqappr_x env i pbty appr1 (evar_apprec env i l2 v2)
+		| None -> (i,false)
+	  else
+	    match eval_flexible_term env flex2 with
 	    | Some v2 ->
 		evar_eqappr_x env i pbty appr1 (evar_apprec env i l2 v2)
 	    | None ->
 		match eval_flexible_term env flex1 with
-		  | Some v1 ->
-		      evar_eqappr_x env i pbty (evar_apprec env i l1 v1) appr2
-		  | None -> (i,false)
+		| Some v1 ->
+		    evar_eqappr_x env i pbty (evar_apprec env i l1 v1) appr2
+		| None -> (i,false)
 	in 
-	ise_try evd [f2; f3; f4]
+	ise_try evd [f1; f2; f3]
 
     | Flexible ev1, Rigid _ ->
 	if 
@@ -496,7 +505,7 @@ let choose_less_dependent_instance evk evd term args =
   let evi = Evd.find (evars_of evd) evk in
   let subst = make_pure_subst evi args in
   let subst' = List.filter (fun (id,c) -> c = term) subst in
-  if subst' = [] then error "Too complex unification problem" else
+  if subst' = [] then error "Too complex unification problem." else
   Evd.evar_define evk (mkVar (fst (List.hd subst'))) evd
 
 let apply_conversion_problem_heuristic env evd pbty t1 t2 =
@@ -506,12 +515,12 @@ let apply_conversion_problem_heuristic env evd pbty t1 t2 =
   let (term2,l2 as appr2) = decompose_app t2 in
   match kind_of_term term1, kind_of_term term2 with
   | Evar (evk1,args1), (Rel _|Var _) when l1 = [] & l2 = [] ->
-      (* The typical kind of constraint coming from patter-matching return
+      (* The typical kind of constraint coming from pattern-matching return
          type inference *)
       assert (array_for_all (fun a -> a = term2 or isEvar a) args1);
       choose_less_dependent_instance evk1 evd term2 args1, true
   | (Rel _|Var _), Evar (evk2,args2) when l1 = [] & l2 = [] ->
-      (* The typical kind of constraint coming from patter-matching return
+      (* The typical kind of constraint coming from pattern-matching return
          type inference *)
       assert (array_for_all ((=) term1) args2);
       choose_less_dependent_instance evk2 evd term1 args2, true
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index fafce268..130e23b8 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: evarutil.ml 11127 2008-06-14 15:39:46Z herbelin $ *)
+(* $Id: evarutil.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
 
 open Util
 open Pp
@@ -374,42 +374,41 @@ let restrict_upon_filter evd evi evk p args =
   else
     evd,evk,args
 
-exception Dependency_error of identifier
+let collect_vars c =
+  let rec collrec acc c =
+    match kind_of_term c with
+    | Var id -> list_add_set id acc
+    | _      -> fold_constr collrec acc c
+  in
+  collrec [] c
 
-module EvkOrd = 
-struct
-  type t = Term.existential_key
-  let compare = Pervasives.compare
-end
+type clear_dependency_error =
+| OccurHypInSimpleClause of identifier option
+| EvarTypingBreak of existential
 
-module EvkSet = Set.Make(EvkOrd)
+exception ClearDependencyError of identifier * clear_dependency_error
 
-let rec check_and_clear_in_constr evdref c ids hist =
+let rec check_and_clear_in_constr evdref err ids c =
   (* returns a new constr where all the evars have been 'cleaned'
      (ie the hypotheses ids have been removed from the contexts of
-     evars *)
+     evars) *)
   let check id' = 
     if List.mem id' ids then
-      raise (Dependency_error id')
+      raise (ClearDependencyError (id',err))
   in 
     match kind_of_term c with
-      | ( Rel _ | Meta _ | Sort _ ) -> c
-
-      | ( Const _ | Ind _ | Construct _ ) -> 
-	  let vars = Environ.vars_of_global (Global.env()) c in
-	    List.iter check vars; c
+      | Var id' ->
+	  check id'; c
 
-      | Var id' ->  
-	  check id'; mkVar id'
+      | ( Const _ | Ind _ | Construct _ ) ->
+          let vars = Environ.vars_of_global (Global.env()) c in
+            List.iter check vars; c
 
       | Evar (evk,l as ev) -> 
 	  if Evd.is_defined_evar !evdref ev then
 	    (* If evk is already defined we replace it by its definition *)
-	    let nc = nf_evar (evars_of !evdref) c in 
-	      (check_and_clear_in_constr evdref nc ids hist)
-	  else if EvkSet.mem evk hist then
-	    (* Loop detection => do nothing *)
-	    c
+	    let nc = whd_evar (evars_of !evdref) c in 
+	      (check_and_clear_in_constr evdref err ids nc)
 	  else 
 	    (* We check for dependencies to elements of ids in the
 	       evar_info corresponding to e and in the instance of
@@ -418,16 +417,32 @@ let rec check_and_clear_in_constr evdref c ids hist =
 	       removed *)
 	    let evi = Evd.find (evars_of !evdref) evk in
 	    let ctxt = Evd.evar_filtered_context evi in
-	    let (nhyps,nargs,rids) = 
+	    let (nhyps,nargs,rids) =
 	      List.fold_right2 
 		(fun (rid,ob,c as h) a (hy,ar,ri) ->
-		  match kind_of_term a with
-		    | Var id -> if List.mem id ids then (hy,ar,id::ri) else (h::hy,a::ar,ri)
-		    | _ -> (h::hy,a::ar,ri)
-		) 	      
+		  (* Check if some id to clear occurs in the instance
+		     a of rid in ev and remember the dependency *)
+		  match 
+		    List.filter (fun id -> List.mem id ids) (collect_vars a)
+		  with
+		  | id :: _ -> (hy,ar,(rid,id)::ri)
+		  | _ ->
+		  (* Check if some rid to clear in the context of ev
+		     has dependencies in another hyp of the context of ev
+		     and transitively remember the dependency *)
+		  match List.filter (fun (id,_) -> occur_var_in_decl (Global.env()) id h) ri with
+		  | rid' :: _ -> (hy,ar,(rid,List.assoc rid ri)::ri)
+		  | _ ->
+		  (* No dependency at all, we can keep this ev's context hyp *)
+		      (h::hy,a::ar,ri))
 		ctxt (Array.to_list l) ([],[],[]) in
-	    (* nconcl must be computed ids (non instanciated hyps) *)
-	    let nconcl = check_and_clear_in_constr evdref (evar_concl evi) rids (EvkSet.add evk hist) in
+	    (* Check if some rid to clear in the context of ev has dependencies
+	       in the type of ev and adjust the source of the dependency *)
+	    let nconcl =
+	      try check_and_clear_in_constr evdref (EvarTypingBreak ev)
+		    (List.map fst rids) (evar_concl evi) 
+	      with ClearDependencyError (rid,err) -> 
+		raise (ClearDependencyError (List.assoc rid rids,err)) in
 
 	    let env = Sign.fold_named_context push_named nhyps ~init:(empty_env) in
 	    let ev'= e_new_evar evdref env ~src:(evar_source evk !evdref) nconcl in
@@ -435,24 +450,19 @@ let rec check_and_clear_in_constr evdref c ids hist =
 	      let (evk',_) = destEvar ev' in
 		mkEvar(evk', Array.of_list nargs)
 
-      | _ -> map_constr (fun c -> check_and_clear_in_constr evdref c ids hist) c
+      | _ -> map_constr (check_and_clear_in_constr evdref err ids) c
 
 let clear_hyps_in_evi evdref hyps concl ids =
-  (* clear_evar_hyps erases hypotheses ids in hyps, checking if some
+  (* clear_hyps_in_evi erases hypotheses ids in hyps, checking if some
      hypothesis does not depend on a element of ids, and erases ids in
      the contexts of the evars occuring in evi *)
-  let nconcl = try check_and_clear_in_constr evdref concl ids EvkSet.empty
-    with Dependency_error id' -> error (string_of_id id' ^ " is used in conclusion") in
-  let (nhyps,_) = 
-    let check_context (id,ob,c) = 
-      try
-	(id,
-	(match ob with 
-	    None -> None
-	  | Some b -> Some (check_and_clear_in_constr evdref b ids EvkSet.empty)),
-	check_and_clear_in_constr evdref c ids EvkSet.empty)
-      with Dependency_error id' -> error (string_of_id id' ^ " is used in hypothesis "
-					   ^ string_of_id id) 
+  let nconcl =
+    check_and_clear_in_constr evdref (OccurHypInSimpleClause None) ids concl in
+  let nhyps = 
+    let check_context (id,ob,c) =
+      let err = OccurHypInSimpleClause (Some id) in
+      (id, Option.map (check_and_clear_in_constr evdref err ids) ob,
+	check_and_clear_in_constr evdref err ids c)
     in
     let check_value vk =
       match !vk with
@@ -469,6 +479,7 @@ let clear_hyps_in_evi evdref hyps concl ids =
   in
   (nhyps,nconcl)
 
+
 (* Expand rels and vars that are bound to other rels or vars so that 
    dependencies in variables are canonically associated to the most ancient
    variable in its family of aliased variables *)
@@ -883,7 +894,7 @@ let rec invert_definition env evd (evk,argsv as ev) rhs =
 and evar_define env (evk,_ as ev) rhs evd =
   try
     let (evd',body) = invert_definition env evd ev rhs in
-    if occur_meta body then error "Meta cannot occur in evar body";
+    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 *)
     if occur_evar evk body then error_occur_check env (evars_of evd) evk body;
@@ -1057,22 +1068,7 @@ let check_evars env initial_sigma evd c =
 	  if not (Evd.mem initial_sigma evk) then
             let (loc,k) = evar_source evk evd in
 	    let evi = nf_evar_info sigma (Evd.find sigma evk) in
-	    let explain =
-	      let f (_,_,t1,t2) =
-		(try head_evar t1 = evk with Failure _ -> false)
-		or (try head_evar t2 = evk with Failure _ -> false) in
-	      let check_several c inst =
-		let _,argsv = destEvar c in
-		let l = List.filter (eq_constr inst) (Array.to_list argsv) in
-		let n = List.length l in
-		(* Maybe should we select one instead of failing ... *)
-		if n >= 2 then Some (SeveralInstancesFound n) else None in
-	      match List.filter f (snd (extract_all_conv_pbs evd)) with
-	      | (_,_,t1,t2)::_ ->
-		  if isEvar t2 then check_several t2 t1 
-		  else check_several t1 t2
-	      | [] -> None
-	    in  error_unsolvable_implicit loc env sigma evi k explain
+	    error_unsolvable_implicit loc env sigma evi k None
       | _ -> iter_constr proc_rec c
   in proc_rec c
 
@@ -1183,11 +1179,12 @@ let split_tycon loc env evd tycon =
 		 if cur = 0 then 
 		   let evd', (x, dom, rng) = real_split c in
 		     evd, (Anonymous, 
-			       Some (Some (init, 0), dom), 
-			       Some (Some (init, 0), rng))
+			  Some (None, dom), 
+			  Some (None, rng))
 		 else
-		   evd, (Anonymous, None, Some (Some (init, pred cur), c)))
-
+		   evd, (Anonymous, None, 
+			Some (if cur = 1 then None,c else Some (init, pred cur), c)))
+	    
 let valcon_of_tycon x = 
   match x with
     | Some (None, t) -> Some t
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index c915d4b0..ca446c01 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 11136 2008-06-18 10:41:34Z herbelin $ i*)
+(*i $Id: evarutil.mli 11309 2008-08-06 10:30:35Z herbelin $ i*)
 
 (*i*)
 open Util
@@ -172,7 +172,15 @@ val pr_tycon_type : env -> type_constraint_type -> Pp.std_ppcmds
 val pr_tycon : env -> type_constraint -> Pp.std_ppcmds
 
 
-(**********************************)
-(* Removing hyps in evars'context *)
+(*********************************************************************)
+(* Removing hyps in evars'context;                                   *)
+(* raise OccurHypInSimpleClause if the removal breaks dependencies   *)
+
+type clear_dependency_error =
+| OccurHypInSimpleClause of identifier option
+| EvarTypingBreak of existential
+
+exception ClearDependencyError of identifier * clear_dependency_error
+
 val clear_hyps_in_evi : evar_defs ref -> named_context_val -> types ->
   identifier list -> named_context_val * types
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 76a5ff26..bf3cd623 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: evd.ml 11166 2008-06-22 13:23:35Z herbelin $ *)
+(* $Id: evd.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
 
 open Pp
 open Util
@@ -523,6 +523,8 @@ let pr_sort_constraints (_,sm) = pr_sort_cstrs sm
 
 let meta_list evd = metamap_to_list evd.metas
 
+let find_meta evd mv = Metamap.find mv evd.metas
+
 let undefined_metas evd =
   List.sort Pervasives.compare (map_succeed (function
     | (n,Clval(_,_,typ)) -> failwith ""
@@ -598,13 +600,13 @@ let meta_with_name evd id =
   match mvnodef, mvl with
     | _,[]  -> 
 	errorlabstrm "Evd.meta_with_name"
-          (str"No such bound variable " ++ pr_id id)
+          (str"No such bound variable " ++ pr_id id ++ str".")
     | ([n],_|_,[n]) -> 
 	n
     | _  -> 
 	errorlabstrm "Evd.meta_with_name"
           (str "Binder name \"" ++ pr_id id ++
-           str"\" occurs more than once in clause")
+           strbrk "\" occurs more than once in clause.")
 
 
 let meta_merge evd1 evd2 =
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 1acc811b..5810f93d 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -7,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: evd.mli 10883 2008-05-05 13:55:24Z herbelin $ i*)
+(*i $Id: evd.mli 11309 2008-08-06 10:30:35Z herbelin $ i*)
 
 (*i*)
 open Util
@@ -100,6 +100,8 @@ val sig_sig : 'a sigma -> evar_map
 (*********************************************************************)
 (* Meta map *)
 
+module Metamap : Map.S with type key = metavariable
+
 module Metaset : Set.S with type elt = metavariable
 
 val meta_exists : (metavariable -> bool) -> Metaset.t -> bool
@@ -197,6 +199,7 @@ val extract_all_conv_pbs : evar_defs -> evar_defs * evar_constraint list
 
 
 (* Metas *)
+val find_meta : evar_defs -> metavariable -> clbinding
 val meta_list : evar_defs -> (metavariable * clbinding) list
 val meta_defined : evar_defs -> metavariable -> bool
 (* [meta_fvalue] raises [Not_found] if meta not in map or [Anomaly] if
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 2325baec..b4b8f0b8 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: indrec.ml 10410 2007-12-31 13:11:55Z msozeau $ *)
+(* $Id: indrec.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
 
 open Pp
 open Util
@@ -591,12 +591,10 @@ let lookup_eliminator ind_sp s =
   try constr_of_global (Nametab.locate (make_short_qualid id))
   with Not_found ->
     errorlabstrm "default_elim"
-      (str "Cannot find the elimination combinator " ++
-       pr_id id ++ spc () ++
-       str "The elimination of the inductive definition " ++
-       pr_id id ++ spc () ++ str "on sort " ++ 
-       spc () ++ pr_sort_family s ++
-       str " is probably not allowed")
+      (strbrk "Cannot find the elimination combinator " ++
+       pr_id id ++ strbrk ", the elimination of the inductive definition " ++
+       pr_id id ++ strbrk " on sort " ++ pr_sort_family s ++
+       strbrk " is probably not allowed.")
 
 
 (*  let env = Global.env() in
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 0daff713..127cd0f2 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: inductiveops.ml 10114 2007-09-06 07:36:14Z herbelin $ *)
+(* $Id: inductiveops.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
 
 open Util
 open Names
@@ -31,6 +31,11 @@ let type_of_constructor env cstr =
   Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in
  Inductive.type_of_constructor cstr specif
 
+(* Return constructor types in user form *)
+let type_of_constructors env ind =
+ let specif = Inductive.lookup_mind_specif env ind in
+  Inductive.type_of_constructors ind specif
+
 (* Return constructor types in normal form *)
 let arities_of_constructors env ind =
  let specif = Inductive.lookup_mind_specif env ind in
@@ -87,7 +92,7 @@ let mis_nf_constructor_type (ind,mib,mip) j =
   and ntypes = mib.mind_ntypes
   and nconstr = Array.length mip.mind_consnames in
   let make_Ik k = mkInd ((fst ind),ntypes-k-1) in 
-  if j > nconstr then error "Not enough constructors in the type";
+  if j > nconstr then error "Not enough constructors in the type.";
   substl (list_tabulate make_Ik ntypes) specif.(j-1)
 
 (* Arity of constructors excluding parameters and local defs *)
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 9e370fec..1d24659c 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: inductiveops.mli 9707 2007-03-15 16:36:15Z herbelin $ i*)
+(*i $Id: inductiveops.mli 11301 2008-08-04 19:41:18Z herbelin $ i*)
 
 open Names
 open Term
@@ -22,6 +22,7 @@ val type_of_inductive    : env -> inductive -> types
 
 (* Return type as quoted by the user *)
 val type_of_constructor  : env -> constructor -> types
+val type_of_constructors : env -> inductive -> types array
 
 (* Return constructor types in normal form *)
 val arities_of_constructors : env -> inductive -> types array
diff --git a/pretyping/matching.ml b/pretyping/matching.ml
index aaa4c3f0..d066a58d 100644
--- a/pretyping/matching.ml
+++ b/pretyping/matching.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: matching.ml 10451 2008-01-18 17:20:28Z barras $ *)
+(* $Id: matching.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
 
 (*i*)
 open Util
@@ -85,7 +85,7 @@ let matches_core convert allow_partial_app pat c =
 	    List.map
 	      (function
 		 | PRel n -> n
-		 | _ -> error "Only bound indices allowed in second order pattern matching")
+		 | _ -> error "Only bound indices allowed in second order pattern matching.")
 	      args in
 	  let frels = Intset.elements (free_rels cT) in
 	  if list_subset frels relargs then
@@ -185,7 +185,7 @@ let matches_core convert allow_partial_app pat c =
   in 
   Sort.list (fun (a,_) (b,_) -> a<b) (sorec [] [] pat c)
 
-let matches = matches_core None false
+let matches = matches_core None true
 
 let pmatches = matches_core None true
 
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 5df5c9fb..057f9d1c 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: pattern.ml 10785 2008-04-13 21:41:54Z herbelin $ *)
+(* $Id: pattern.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
 
 open Util
 open Names
@@ -133,7 +133,7 @@ let map_pattern f = map_pattern_with_binders (fun () -> ()) (fun () -> f) ()
 
 let rec instantiate_pattern lvar = function
   | PVar id as x -> (try Lazy.force(List.assoc id lvar) with Not_found -> x)
-  | (PFix _ | PCoFix _) -> error ("Not instantiable pattern")
+  | (PFix _ | PCoFix _) -> error ("Non instantiable pattern.")
   | c -> map_pattern (instantiate_pattern lvar) c
 
 let rec liftn_pattern k n = function
@@ -264,7 +264,7 @@ let rec pat_of_raw metas vars = function
              
   | r ->
       let loc = loc_of_rawconstr r in
-      user_err_loc (loc,"pattern_of_rawconstr", Pp.str "Pattern not supported")
+      user_err_loc (loc,"pattern_of_rawconstr", Pp.str"Non supported pattern.")
 
 and pat_of_raw_branch loc metas vars ind brs i =
   let bri = List.filter
@@ -272,23 +272,23 @@ and pat_of_raw_branch loc metas vars ind brs i =
         (_,_,[PatCstr(_,c,lv,Anonymous)],_) -> snd c = i+1
       | (loc,_,_,_) ->
           user_err_loc (loc,"pattern_of_rawconstr",
-                        Pp.str "Not supported pattern")) brs in
+                        Pp.str "Non supported pattern.")) brs in
   match bri with
     | [(_,_,[PatCstr(_,(indsp,_),lv,_)],br)] ->
 	if ind <> None & ind <> Some indsp then
           user_err_loc (loc,"pattern_of_rawconstr",
-            Pp.str "All constructors must be in the same inductive type");
+            Pp.str "All constructors must be in the same inductive type.");
         let lna =
           List.map
             (function PatVar(_,na) -> na
               | PatCstr(loc,_,_,_) ->
                   user_err_loc (loc,"pattern_of_rawconstr",
-                                Pp.str "Not supported pattern")) lv in
+                                Pp.str "Non supported pattern.")) lv in
         let vars' = List.rev lna @ vars in 
 	List.length lv, rev_it_mkPLambda lna (pat_of_raw metas vars' br)
     | _ -> user_err_loc (loc,"pattern_of_rawconstr",
                          str "No unique branch for " ++ int (i+1) ++
-                         str"-th constructor")
+                         str"-th constructor.")
 
 let pattern_of_rawconstr c =
   let metas = ref [] in
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 5f0999cb..a3246bc8 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: pretyping.ml 11047 2008-06-03 23:08:00Z msozeau $ *)
+(* $Id: pretyping.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
 
 open Pp
 open Util
@@ -66,7 +66,7 @@ let search_guard loc env possible_indexes fixdefs =
 	    try check_fix env fix; raise (Found indexes) 
 	    with TypeError _ -> ())
 	 (list_combinations possible_indexes); 
-       let errmsg = "cannot guess decreasing argument of fix" in 
+       let errmsg = "Cannot guess decreasing argument of fix." in 
        if loc = dummy_loc then error errmsg else 
 	 user_err_loc (loc,"search_guard", Pp.str errmsg)
      with Found indexes -> indexes)
@@ -244,7 +244,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
     try (* To build a nicer ltac error message *)
       match List.assoc id unbndltacvars with
       | None -> user_err_loc (loc,"",
-	  str "variable " ++ pr_id id ++ str " should be bound to a term")
+	  str "Variable " ++ pr_id id ++ str " should be bound to a term.")
       | Some id0 -> Pretype_errors.error_var_not_found_loc loc id0
     with Not_found ->
       error_var_not_found_loc loc id
@@ -356,7 +356,9 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 		   uj_type = it_mkProd_or_LetIn j.uj_type ctxt })
             ctxtv vdef in
 	evar_type_fixpoint loc env evdref names ftys vdefj;
-	let fixj = match fixkind with
+	let ftys = Array.map (nf_evar (evars_of !evdref)) ftys in
+	let fdefs = Array.map (fun x -> nf_evar (evars_of !evdref) (j_val x)) vdefj in
+ 	let fixj = match fixkind with
 	  | RFix (vn,i) ->
 	      (* First, let's find the guard indexes. *)
 	      (* If recursive argument was not given by user, we try all args.
@@ -370,11 +372,11 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 		   | None -> list_map_i (fun i _ -> i) 0 ctxtv.(i))
 		vn)
 	      in 
-	      let fixdecls = (names,ftys,Array.map j_val vdefj) in 
+	      let fixdecls = (names,ftys,fdefs) in 
 	      let indexes = search_guard loc env possible_indexes fixdecls in 
 	      make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i)
 	  | RCoFix i ->
-	      let cofix = (i,(names,ftys,Array.map j_val vdefj)) in
+	      let cofix = (i,(names,ftys,fdefs)) in
 	      (try check_cofix env cofix with e -> Stdpp.raise_with_loc loc e);
 	      make_judge (mkCoFix cofix) ftys.(i) in
 	inh_conv_coerce_to_tycon loc env evdref fixj tycon
@@ -459,10 +461,10 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	in
 	let cstrs = get_constructors env indf in
 	  if Array.length cstrs <> 1 then
-            user_err_loc (loc,"",str "Destructing let is only for inductive types with one constructor");
+            user_err_loc (loc,"",str "Destructing let is only for inductive types with one constructor.");
 	  let cs = cstrs.(0) in
 	    if List.length nal <> cs.cs_nargs then
-              user_err_loc (loc,"", str "Destructing let on this type expects " ++ int cs.cs_nargs ++ str " variables");
+              user_err_loc (loc,"", str "Destructing let on this type expects " ++ int cs.cs_nargs ++ str " variables.");
 	    let fsign = List.map2 (fun na (_,c,t) -> (na,c,t))
               (List.rev nal) cs.cs_args in
 	    let env_f = push_rels fsign env in
@@ -525,7 +527,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	let cstrs = get_constructors env indf in 
 	  if Array.length cstrs <> 2 then
             user_err_loc (loc,"",
-			  str "If is only for inductive types with two constructors");
+			  str "If is only for inductive types with two constructors.");
 
 	  let arsgn = 
 	    let arsgn,_ = get_arity env indf in
@@ -613,7 +615,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	    j
 	      (*inh_conv_coerce_to_tycon loc env evdref j tycon*)
 	else
-	  user_err_loc (loc,"pretype",(str "Not a constr tagged Dynamic"))
+	  user_err_loc (loc,"pretype",(str "Not a constr tagged Dynamic."))
 
   (* [pretype_type valcon env evdref lvar c] coerces [c] into a type *)
   and pretype_type valcon env evdref lvar = function
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index 62798a45..3726b8df 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: rawterm.ml 11094 2008-06-10 19:35:23Z herbelin $ *)
+(* $Id: rawterm.ml 11282 2008-07-28 11:51:53Z msozeau $ *)
 
 (*i*)
 open Util
@@ -36,7 +36,7 @@ type rawsort = RProp of Term.contents | RType of Univ.universe option
 
 type binder_kind = BProd | BLambda | BLetIn
 
-type binding_kind = Explicit | Implicit
+type binding_kind = Lib.binding_kind = Explicit | Implicit
 
 type quantified_hypothesis = AnonHyp of int | NamedHyp of identifier
 
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 2ba8022f..eecee8b0 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 11094 2008-06-10 19:35:23Z herbelin $ i*)
+(*i $Id: rawterm.mli 11282 2008-07-28 11:51:53Z msozeau $ i*)
 
 (*i*)
 open Util
@@ -40,7 +40,7 @@ type rawsort = RProp of Term.contents | RType of Univ.universe option
 
 type binder_kind = BProd | BLambda | BLetIn
 
-type binding_kind = Explicit | Implicit
+type binding_kind = Lib.binding_kind = Explicit | Implicit
 
 type quantified_hypothesis = AnonHyp of int | NamedHyp of identifier
 
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index bd73740f..06289434 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: recordops.ml 10577 2008-02-19 10:18:19Z corbinea $ *)
+(* $Id: recordops.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
 
 open Util
 open Pp
@@ -109,6 +109,7 @@ that maps the pair (Li,ci) to the following data
     o_DEF = c
     o_TABS = B1...Bk
     o_PARAMS = a1...am
+    o_NARAMS = m
     o_TCOMP = ui1...uir
 
 *)
@@ -118,6 +119,7 @@ type obj_typ = {
   o_INJ : int;      (* position of trivial argument (negative= none) *)
   o_TABS : constr list;    (* ordered *)
   o_TPARAMS : constr list; (* ordered *)
+  o_NPARAMS : int;
   o_TCOMPS : constr list } (* ordered *)
 
 type cs_pattern =
@@ -126,10 +128,11 @@ type cs_pattern =
   | Sort_cs of sorts_family
   | Default_cs
 
-let object_table =
-  (ref [] : ((global_reference * cs_pattern) * obj_typ) list ref)
+let object_table = ref (Refmap.empty : (cs_pattern * obj_typ) list Refmap.t)
 
-let canonical_projections () = !object_table
+let canonical_projections () = 
+  Refmap.fold (fun x -> List.fold_right (fun (y,c) acc -> ((x,y),c)::acc))
+    !object_table []
 
 let keep_true_projections projs kinds =
   map_succeed (function (p,true) -> p | _ -> failwith "")
@@ -177,15 +180,18 @@ let compute_canonical_projections (con,ind) =
 	   | _ -> l)
       [] lps in
   List.map (fun (refi,c,inj,argj) ->
-    (refi,c),{o_DEF=v; o_INJ=inj; o_TABS=lt; o_TPARAMS=params; o_TCOMPS=argj})
+    (refi,c),
+    {o_DEF=v; o_INJ=inj; o_TABS=lt; 
+     o_TPARAMS=params; o_NPARAMS=List.length params; o_TCOMPS=argj})
     comp
 
 let open_canonical_structure i (_,o) =
   if i=1 then
     let lo = compute_canonical_projections o in
-    List.iter (fun (o,_ as x) ->
-      if not (List.mem_assoc o !object_table) then
-	object_table := x :: (!object_table)) lo
+    List.iter (fun ((proj,cs_pat),s) ->
+      let l = try Refmap.find proj !object_table with Not_found -> [] in
+      if not (List.mem_assoc cs_pat l) then
+        object_table := Refmap.add proj ((cs_pat,s)::l) !object_table) lo
 
 let cache_canonical_structure o =
   open_canonical_structure 1 o
@@ -215,7 +221,7 @@ let add_canonical_structure x = Lib.add_anonymous_leaf (inCanonStruc x)
 
 let error_not_structure ref =
   errorlabstrm "object_declare"
-    (Nameops.pr_id (id_of_global ref) ++ str" is not a structure object")
+    (Nameops.pr_id (id_of_global ref) ++ str" is not a structure object.")
 
 let check_and_decompose_canonical_structure ref =
   let sp = match ref with ConstRef sp -> sp | _ -> error_not_structure ref in
@@ -241,7 +247,15 @@ let declare_canonical_structure ref =
 
 let outCanonicalStructure x = fst (outCanonStruct x)
 
-let lookup_canonical_conversion o = List.assoc o !object_table
+let lookup_canonical_conversion (proj,pat) =
+  List.assoc pat (Refmap.find proj !object_table)
+
+let is_open_canonical_projection sigma (c,args) =
+  try 
+    let l = Refmap.find (global_of_constr c) !object_table in
+    let n = (snd (List.hd l)).o_NPARAMS in
+    try isEvar (whd_evar sigma (List.nth args n)) with Failure _ -> false
+  with Not_found -> false
 
 let freeze () =
   !structure_table, !projection_table, !object_table
@@ -251,7 +265,7 @@ let unfreeze (s,p,o) =
 
 let init () =
   structure_table := Indmap.empty; projection_table := Cmap.empty;
-  object_table:=[]
+  object_table := Refmap.empty
 
 let _ = init()
 
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 7a7d941d..74f6a9ce 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 10577 2008-02-19 10:18:19Z corbinea $ i*)
+(*i $Id: recordops.mli 11309 2008-08-06 10:30:35Z herbelin $ i*)
 
 (*i*)
 open Names
@@ -47,11 +47,14 @@ type obj_typ = {
   o_INJ : int;      (* position of trivial argument *)
   o_TABS : constr list;    (* ordered *)
   o_TPARAMS : constr list; (* ordered *)
+  o_NPARAMS : int;
   o_TCOMPS : constr list } (* ordered *)
 
 val cs_pattern_of_constr : constr -> cs_pattern * int * constr list
  
 val lookup_canonical_conversion : (global_reference * cs_pattern) -> obj_typ
 val declare_canonical_structure : global_reference -> unit
+val is_open_canonical_projection :
+  Evd.evar_map -> (constr * constr list) -> bool
 val canonical_projections : unit -> 
   ((global_reference * cs_pattern) * obj_typ) list
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 6fc30aae..2f507318 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: reductionops.ml 11010 2008-05-28 15:25:19Z barras $ *)
+(* $Id: reductionops.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
 
 open Pp
 open Util
@@ -518,9 +518,11 @@ let whd_eta c = app_stack (local_whd_state_gen eta (c,empty_stack))
 (* Replacing defined evars for error messages *)
 let rec whd_evar sigma c =
   match kind_of_term c with
-    | Evar (ev,args)
-        when Evd.mem sigma ev & Evd.is_defined sigma ev ->
-	whd_evar sigma (Evd.existential_value sigma (ev,args))
+    | Evar ev ->
+	let d = 
+	  try Some (Evd.existential_value sigma ev)
+	  with NotInstantiatedEvar | Not_found -> None in
+	(match d with Some c -> whd_evar sigma c | None -> c)
     | Sort s when is_sort_variable sigma s -> whd_sort_variable sigma c
     | _ -> collapse_appl c
 
@@ -773,7 +775,7 @@ let splay_arity env sigma c =
   let l, c = splay_prod env sigma c in
   match kind_of_term c with
     | Sort s -> l,s
-    | _ -> error "not an arity"
+    | _ -> invalid_arg "splay_arity"
 
 let sort_of_arity env c = snd (splay_arity env Evd.empty c)
 
@@ -783,7 +785,7 @@ let decomp_n_prod env sigma n =
       | Prod (n,a,c0) ->
 	  decrec (push_rel (n,None,a) env)
 	    (m-1) (Sign.add_rel_decl (n,None,a) ln) c0
-      | _                      -> error "decomp_n_prod: Not enough products"
+      | _                      -> invalid_arg "decomp_n_prod"
   in 
   decrec env n Sign.empty_rel_context
 
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index d48055cf..1ac36b2a 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: reductionops.mli 11010 2008-05-28 15:25:19Z barras $ i*)
+(*i $Id: reductionops.mli 11309 2008-08-06 10:30:35Z herbelin $ i*)
 
 (*i*)
 open Names
@@ -111,7 +111,6 @@ val whd_betadeltaiota_nolet_stack :  contextual_stack_reduction_function
 val whd_betaetalet_stack : local_stack_reduction_function
 val whd_betalet_stack : local_stack_reduction_function
 
-val whd_state : local_state_reduction_function
 val whd_beta_state : local_state_reduction_function
 val whd_betaiota_state : local_state_reduction_function
 val whd_betaiotazeta_state : local_state_reduction_function
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 50401502..57fdbb09 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: tacred.ml 11094 2008-06-10 19:35:23Z herbelin $ *)
+(* $Id: tacred.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
 
 open Pp
 open Util
@@ -543,7 +543,7 @@ let try_red_product env sigma c =
 
 let red_product env sigma c = 
   try try_red_product env sigma c
-  with Redelimination -> error "Not reducible"
+  with Redelimination -> error "Not reducible."
 
 (*
 (* This old version of hnf uses betadeltaiota instead of itself (resp 
@@ -698,7 +698,7 @@ let unfold env sigma name =
   if is_evaluable env name then
     clos_norm_flags (unfold_red name) env sigma
   else
-    error (string_of_evaluable_ref env name^" is opaque")
+    error (string_of_evaluable_ref env name^" is opaque.")
 
 (* [unfoldoccs : (readable_constraints -> (int list * section_path) -> constr -> constr)]
  * Unfolds the constant name in a term c following a list of occurrences occl.
@@ -709,7 +709,7 @@ let unfoldoccs env sigma ((nowhere_except_in,locs as plocs),name) c =
   else
     let (nbocc,uc) = substlin env name 1 plocs c in
     if nbocc = 1 then 
-      error ((string_of_evaluable_ref env name)^" does not occur");
+      error ((string_of_evaluable_ref env name)^" does not occur.");
     let rest = List.filter (fun o -> o >= nbocc) locs in
     if rest <> [] then error_invalid_occurrence rest;
     nf_betaiota uc
@@ -722,7 +722,7 @@ let unfoldn loccname env sigma c =
 let fold_one_com com env sigma c =
   let rcom =
     try red_product env sigma com
-    with Redelimination -> error "Not reducible" in
+    with Redelimination -> error "Not reducible." in
   (* Reason first on the beta-iota-zeta normal form of the constant as
      unfold produces it, so that the "unfold f; fold f" configuration works
      to refold fix expressions *)
@@ -757,7 +757,7 @@ let compute = cbv_betadeltaiota
 let abstract_scheme env sigma (locc,a) c =
   let ta = Retyping.get_type_of env sigma a in
   let na = named_hd env ta Anonymous in
-  if occur_meta ta then error "cannot find a type for the generalisation";
+  if occur_meta ta then error "Cannot find a type for the generalisation.";
   if occur_meta a then 
     mkLambda (na,ta,c)
   else 
@@ -785,14 +785,14 @@ let reduce_to_ind_gen allow_product env sigma t =
 	  if allow_product then
 	    elimrec (push_rel (n,None,ty) env) t' ((n,None,ty)::l)
 	  else
-	    errorlabstrm "" (str"Not an inductive definition")
+	    errorlabstrm "" (str"Not an inductive definition.")
       | _ ->
 	  (* Last chance: we allow to bypass the Opaque flag (as it
 	     was partially the case between V5.10 and V8.1 *)
 	  let t' = whd_betadeltaiota env sigma t in
 	  match kind_of_term (fst (decompose_app t')) with
 	    | Ind ind-> (ind, it_mkProd_or_LetIn t' l)
-	    | _ -> errorlabstrm "" (str"Not an inductive product")
+	    | _ -> errorlabstrm "" (str"Not an inductive product.")
   in
   elimrec env t []
 
@@ -843,7 +843,7 @@ let reduce_to_ref_gen allow_product env sigma ref t =
     let (mind,t) = reduce_to_ind_gen allow_product env sigma t in
     if IndRef mind <> ref then
       errorlabstrm "" (str "Cannot recognize a statement based on " ++ 
-        Nametab.pr_global_env Idset.empty ref)
+        Nametab.pr_global_env Idset.empty ref ++ str".")
     else
       t
   else
@@ -857,7 +857,7 @@ let reduce_to_ref_gen allow_product env sigma ref t =
 	  else 
 	     errorlabstrm "" 
 	       (str "Cannot recognize an atomic statement based on " ++ 
-	        Nametab.pr_global_env Idset.empty ref)
+	        Nametab.pr_global_env Idset.empty ref ++ str".")
       | _ ->
 	  try 
 	    if global_of_constr c = ref 
@@ -870,7 +870,7 @@ let reduce_to_ref_gen allow_product env sigma ref t =
           with NotStepReducible ->
 	    errorlabstrm ""
 	      (str "Cannot recognize a statement based on " ++ 
-	       Nametab.pr_global_env Idset.empty ref)
+	       Nametab.pr_global_env Idset.empty ref ++ str".")
   in
   elimrec env t []
 
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index e31024bb..1ce53e88 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: termops.ml 11166 2008-06-22 13:23:35Z herbelin $ *)
+(* $Id: termops.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
 
 open Pp
 open Util
@@ -639,7 +639,7 @@ let error_invalid_occurrence l =
   let l = list_uniquize (List.sort Pervasives.compare l) in
   errorlabstrm ""
     (str ("Invalid occurrence " ^ plural (List.length l) "number" ^": ") ++ 
-     prlist_with_sep spc int l)
+     prlist_with_sep spc int l ++ str ".")
 
 let subst_term_occ_gen (nowhere_except_in,locs) occ c t =
   let maxocc = List.fold_right max locs 0 in
@@ -817,21 +817,15 @@ let names_of_rel_context env =
 
 (**** Globality of identifiers *)
 
-(* TODO temporary hack!!! *)
 let rec is_imported_modpath = function
-  | MPfile dp -> dp <> (Lib.library_dp ())
-(*  | MPdot (mp,_) -> is_imported_modpath mp *)
-  | _ -> false
+  | MPfile dp -> true
+  | p -> false
 
 let is_imported_ref = function
   | VarRef _ -> false
   | IndRef (kn,_)
-  | ConstructRef ((kn,_),_) 
-(*  | ModTypeRef ln  *) -> 
+  | ConstructRef ((kn,_),_) ->
       let (mp,_,_) = repr_kn kn in is_imported_modpath mp
-(*  | ModRef mp ->
-      is_imported_modpath mp
-*)
   | ConstRef kn ->
       let (mp,_,_) = repr_con kn in is_imported_modpath mp
 
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 94aff66f..645b7d72 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 11166 2008-06-22 13:23:35Z herbelin $ i*)
+(*i $Id: termops.mli 11282 2008-07-28 11:51:53Z msozeau $ i*)
 
 open Util
 open Pp
@@ -185,7 +185,7 @@ val mkLambda_or_LetIn_name : env -> constr -> rel_declaration -> constr
 val it_mkProd_or_LetIn_name   : env -> types -> rel_context -> types
 val it_mkLambda_or_LetIn_name : env -> constr -> rel_context -> constr
 
-(* Get the last arg of a constr intended to be nn application *)
+(* Get the last arg of a constr intended to be an application *)
 val last_arg : constr -> constr
 
 (* name contexts *)
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index a2392033..86168a1f 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 11143 2008-06-18 15:52:42Z msozeau $ i*)
+(*i $Id: typeclasses.ml 11282 2008-07-28 11:51:53Z msozeau $ i*)
 
 (*i*)
 open Names
@@ -35,12 +35,10 @@ type typeclass = {
   cl_impl : global_reference; 
 
   (* Context in which the definitions are typed. Includes both typeclass parameters and superclasses. *)
-  cl_context : ((global_reference * bool) option * named_declaration) list; 
-
-  cl_params: int;
+  cl_context : ((global_reference * bool) option * rel_declaration) list; 
 
   (* Context of definitions and properties on defs, will not be shared *)
-  cl_props : named_context;
+  cl_props : rel_context;
   
   (* The method implementaions as projections. *)
   cl_projs : (identifier * constant) list;
@@ -111,13 +109,13 @@ let gmap_cmap_merge old ne =
     Gmap.fold (fun cl insts acc -> 
       let oldinsts = try Gmap.find cl old with Not_found -> Cmap.empty in
 	Gmap.add cl (cmap_union oldinsts insts) acc)
-      Gmap.empty ne
+      ne Gmap.empty
   in
     Gmap.fold (fun cl insts acc -> 
       if Gmap.mem cl ne' then acc
       else Gmap.add cl insts acc)
-      ne' old
-      
+      old ne'
+
 let add_instance_hint_ref = ref (fun id pri -> assert false)
 let register_add_instance_hint =
   (:=) add_instance_hint_ref
@@ -154,7 +152,7 @@ let subst (_,subst,(cl,m,inst)) =
   let do_subst_projs projs = list_smartmap (fun (x, y) -> (x, do_subst_con y)) projs in
   let subst_class k cl classes = 
     let k = do_subst_gr k in
-    let cl' = { cl with cl_impl = k;
+    let cl' = { cl_impl = k;
 		cl_context = do_subst_ctx cl.cl_context;
 		cl_props = do_subst_named cl.cl_props;
 		cl_projs = do_subst_projs cl.cl_projs; }
@@ -176,8 +174,14 @@ let subst (_,subst,(cl,m,inst)) =
     (classes, m, instances)
 
 let discharge (_,(cl,m,inst)) =
-  let discharge_named (cl, r) =
-    Option.smartmap (fun (gr, b) -> Lib.discharge_global gr, b) cl, r
+  let discharge_context subst rel =
+    let ctx, _ =
+      List.fold_right
+	(fun (gr, (id, b, t)) (ctx, k) -> 
+	  let gr' = Option.map (fun (gr, b) -> Lib.discharge_global gr, b) gr in
+	    ((gr', (id, Option.map (substn_vars k subst) b, substn_vars k subst t)) :: ctx), succ k)
+	rel ([], 0)
+    in ctx
   in
   let abs_context cl =
     match cl.cl_impl with
@@ -190,10 +194,11 @@ let discharge (_,(cl,m,inst)) =
     let cl' =
       if cl_impl' == cl.cl_impl then cl
       else
+	let ctx = abs_context cl in
 	{ cl with cl_impl = cl_impl';
 	  cl_context = 
-	    List.map (fun x -> None, x) (abs_context cl) @	
-	      (list_smartmap discharge_named cl.cl_context);
+	    List.map (fun (na,impl,b,t) -> None, (Name na,b,t)) ctx @
+	      (discharge_context (List.map (fun (na, _, _, _) -> na) ctx) cl.cl_context);
 	  cl_projs = list_smartmap (fun (x, y) -> x, Lib.discharge_con y) cl.cl_projs }
     in Gmap.add cl_impl' cl' acc
   in
@@ -211,7 +216,7 @@ let discharge (_,(cl,m,inst)) =
   let instances = Gmap.fold subst_inst inst Gmap.empty in
     Some (classes, m, instances)
       
-let rebuild (_,(cl,m,inst)) =
+let rebuild (cl,m,inst) =
   let inst = 
     Gmap.map (fun insts -> 
       Cmap.fold (fun k is insts -> 
@@ -277,49 +282,14 @@ let add_instance i =
   add_instance_hint i.is_impl i.is_pri;
   update ()
 
+let all_instances () = 
+  Gmap.fold (fun k v acc -> 
+    Cmap.fold (fun k v acc -> v :: acc) v acc)
+    !instances []
+
 let instances r = 
   let cl = class_info r in instances_of cl
-
-let solve_instanciation_problem = ref (fun _ _ _ _ -> assert false)
-let solve_instanciations_problem = ref (fun _ _ _ _ _ -> assert false)
-
-let resolve_typeclass env ev evi (evd, defined as acc) =
-  try
-    assert(evi.evar_body = Evar_empty);
-    !solve_instanciation_problem env evd ev evi
-  with Exit -> acc
-
-let resolve_one_typeclass env types =
-  try
-    let evi = Evd.make_evar (Environ.named_context_val env) types in
-    let ev = 1 in
-    let evm = Evd.add Evd.empty ev evi in
-    let evd = Evd.create_evar_defs evm in
-    let evd', b = !solve_instanciation_problem env evd ev evi in
-      if b then 
-	let evm' = Evd.evars_of evd' in
-	  match Evd.evar_body (Evd.find evm' ev) with
-	      Evar_empty -> raise Not_found
-	    | Evar_defined c -> c
-      else raise Not_found
-  with Exit -> raise Not_found
-
-let resolve_one_typeclass_evd env evd types =
-  try
-    let ev = Evarutil.e_new_evar evd env types in
-    let (ev,_) = destEvar ev in
-    let evd', b =
-	!solve_instanciation_problem env !evd ev (Evd.find (Evd.evars_of !evd) ev)
-    in
-      evd := evd';
-      if b then 
-	let evm' = Evd.evars_of evd' in
-	  match Evd.evar_body (Evd.find evm' ev) with
-	      Evar_empty -> raise Not_found
-	    | Evar_defined c -> Evarutil.nf_evar evm' c
-      else raise Not_found
-  with Exit -> raise Not_found
-
+    
 let method_typeclass ref = 
   match ref with 
     | ConstRef c -> 
@@ -349,51 +319,6 @@ let is_implicit_arg k =
     | InternalHole -> true
     | _ -> false
 
-let destClassApp c = 
-  match kind_of_term c with
-    | App (ki, args) when isInd ki -> 
-	Some (destInd ki, args)
-    | _ when isInd c -> Some (destInd c, [||])
-    | _ -> None
-
-let is_independent evm ev = 
-  Evd.fold (fun ev' evi indep -> indep && 
-    (ev = ev' || 
-	evi.evar_body <> Evar_empty ||
-	not (Termops.occur_evar ev evi.evar_concl)))
-    evm true
-    
-
-(*   try !solve_instanciations_problem env (Evarutil.nf_evar_defs evd) *)
-(*   with _ -> *)
-(*   let evm = Evd.evars_of evd in *)
-(*   let tc_evars =  *)
-(*     let f ev evi acc = *)
-(*       let (l, k) = Evd.evar_source ev evd in *)
-(* 	if not check || is_implicit_arg k then *)
-(* 	  match destClassApp evi.evar_concl with *)
-(* 	    | Some (i, args) when is_class i ->  *)
-(* 		Evd.add acc ev evi *)
-(* 	    | _ -> acc *)
-(* 	else acc *)
-(*     in Evd.fold f evm Evd.empty *)
-(*   in *)
-(*   let rec sat evars = *)
-(*     let evm = Evd.evars_of evars in *)
-(*     let (evars', progress) =  *)
-(*       Evd.fold  *)
-(* 	(fun ev evi acc ->  *)
-(* 	  if (Evd.mem tc_evars ev || not (Evd.mem evm ev))  *)
-(* 	    && evi.evar_body = Evar_empty then *)
-(* 	    resolve_typeclass env ev evi acc  *)
-(* 	  else acc) *)
-(* 	evm (evars, false)  *)
-(*     in *)
-(*       if not progress then evars' *)
-(*       else *)
-(* 	sat (Evarutil.nf_evar_defs evars') *)
-(*   in sat (Evarutil.nf_evar_defs evd) *)
-  
 let class_of_constr c = 
   let extract_cl c =
     try Some (class_info (global_of_constr c)) with _ -> None
@@ -432,26 +357,26 @@ let mark_unresolvables sigma =
     Evd.add evs ev (mark_unresolvable evi))
     sigma Evd.empty
     
+let rec is_class_type c =
+  match kind_of_term c with
+  | Prod (_, _, t) -> is_class_type t
+  | _ -> class_of_constr c <> None
+
+let is_class_evar evi = 
+  is_class_type evi.Evd.evar_concl
+    
 let has_typeclasses evd =
   Evd.fold (fun ev evi has -> has || 
-    (evi.evar_body = Evar_empty && class_of_constr evi.evar_concl <> None 
-	&& is_resolvable evi))
+    (evi.evar_body = Evar_empty && is_class_evar evi && is_resolvable evi))
     evd false
 
+let solve_instanciations_problem = ref (fun _ _ _ _ _ -> assert false)
+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
 
-type substitution = (identifier * constr) list
-
-let substitution_of_named_context isevars env id n subst l = 
-  List.fold_right
-    (fun (na, _, t) subst -> 
-      let t' = replace_vars subst t in
-      let b = Evarutil.e_new_evar isevars env ~src:(dummy_loc, ImplicitArg (VarRef id, (n, Some na))) t' in
-	(na, b) :: subst)
-    l subst
-
-let nf_substitution sigma subst = 
-  List.map (function (na, c) -> na, Reductionops.nf_evar sigma c) subst
+let resolve_one_typeclass env evm t =
+  !solve_instanciation_problem env evm t
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index a3118053..fdbb78a9 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: typeclasses.mli 11161 2008-06-21 14:32:47Z msozeau $ i*)
+(*i $Id: typeclasses.mli 11282 2008-07-28 11:51:53Z msozeau $ i*)
 
 (*i*)
 open Names
@@ -30,12 +30,10 @@ type typeclass = {
 
   (* Context in which the definitions are typed. Includes both typeclass parameters and superclasses. 
      The boolean indicates if the typeclass argument is a direct superclass. *)
-  cl_context : ((global_reference * bool) option * named_declaration) list; 
-
-  cl_params : int; (* This is the length of the suffix of the context which should be considered explicit parameters. *)
+  cl_context : ((global_reference * bool) option * rel_declaration) list; 
 
   (* Context of definitions and properties on defs, will not be shared *)
-  cl_props : named_context;
+  cl_props : rel_context;
 
   (* The methods implementations of the typeclass as projections. *)
   cl_projs : (identifier * constant) list;
@@ -43,33 +41,32 @@ type typeclass = {
 
 type instance
 
-val instance_impl : instance -> constant
-
-val new_instance : typeclass -> int option -> bool -> constant -> instance
-  
 val instances : global_reference -> instance list
 val typeclasses : unit -> typeclass list
+val all_instances : unit -> instance list
+
 val add_class : typeclass -> unit
-val add_instance : instance -> unit
 
-val register_add_instance_hint : (constant -> int option -> unit) -> unit
-val add_instance_hint : constant -> int option -> unit
+val new_instance : typeclass -> int option -> bool -> constant -> instance
+val add_instance : instance -> unit
 
 val class_info : global_reference -> typeclass (* raises a UserError if not a class *)
-val is_class : global_reference -> bool
+
 val class_of_constr : constr -> typeclass option
 val dest_class_app : constr -> typeclass * constr array (* raises a UserError if not a class *)
 
+val instance_impl : instance -> constant
+
+val is_class : global_reference -> bool
 val is_instance : global_reference -> bool
 val is_method : constant -> bool
 
+val is_implicit_arg : hole_kind -> bool
+
 (* Returns the term and type for the given instance of the parameters and fields
    of the type class. *)
-val instance_constructor : typeclass -> constr list -> constr * types
 
-val resolve_one_typeclass : env -> types -> types (* Raises Not_found *)
-val resolve_one_typeclass_evd : env -> evar_defs ref -> types -> types (* Raises Not_found *)
-val resolve_typeclass : env -> evar -> evar_info -> evar_defs * bool -> evar_defs * bool
+val instance_constructor : typeclass -> constr list -> constr * types
 
 (* Use evar_extra for marking resolvable evars. *)
 val bool_in : bool -> Dyn.t
@@ -78,28 +75,15 @@ val bool_out : Dyn.t -> bool
 val is_resolvable : evar_info -> bool
 val mark_unresolvable : evar_info -> evar_info
 val mark_unresolvables : evar_map -> evar_map
+val is_class_evar : evar_info -> bool
 
-val resolve_typeclasses : ?onlyargs:bool -> ?split:bool -> ?fail:bool -> env -> evar_defs -> evar_defs
-
-val solve_instanciation_problem : (env -> evar_defs -> existential_key -> evar_info -> evar_defs * bool) ref
-val solve_instanciations_problem : (env -> evar_defs -> bool -> bool -> bool -> evar_defs) ref
-
-type substitution = (identifier * constr) list
+val resolve_typeclasses : ?onlyargs:bool -> ?split:bool -> ?fail:bool -> 
+  env -> evar_defs -> evar_defs
+val resolve_one_typeclass : env -> evar_map -> types -> constr
 
-val substitution_of_named_context : 
-  evar_defs ref -> env -> identifier -> int ->
-  substitution -> named_context -> substitution
-
-val nf_substitution : evar_map -> substitution -> substitution
-
-val is_implicit_arg : hole_kind -> bool
-
-(* debug *)
+val register_add_instance_hint : (constant -> int option -> unit) -> unit
+val add_instance_hint : constant -> int option -> unit
 
-(* val subst :  *)
-(*     'a * Mod_subst.substitution * *)
-(*     ((Libnames.global_reference, typeclass) Gmap.t * 'b * *)
-(*      ('c, instance list) Gmap.t) -> *)
-(*     (Libnames.global_reference, typeclass) Gmap.t * 'b * *)
-(*     ('c, instance list) Gmap.t *)
+val solve_instanciations_problem : (env -> evar_defs -> bool -> bool -> bool -> evar_defs) ref
+val solve_instanciation_problem : (env -> evar_map -> types -> constr) ref
 
diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index 9faac94d..8844baab 100644
--- a/pretyping/typeclasses_errors.ml
+++ b/pretyping/typeclasses_errors.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: typeclasses_errors.ml 11150 2008-06-19 11:38:27Z msozeau $ i*)
+(*i $Id: typeclasses_errors.ml 11282 2008-07-28 11:51:53Z msozeau $ i*)
 
 (*i*)
 open Names
@@ -29,7 +29,7 @@ type typeclass_error =
     | UnboundMethod of global_reference * identifier located (* Class name, method *)
     | NoInstance of identifier located * constr list
     | UnsatisfiableConstraints of evar_defs * (evar_info * hole_kind) option
-    | MismatchedContextInstance of contexts * constr_expr list * named_context (* found, expected *)
+    | MismatchedContextInstance of contexts * constr_expr list * rel_context (* found, expected *)
 
 exception TypeClassError of env * typeclass_error
 
diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli
index 6491372f..a79307d0 100644
--- a/pretyping/typeclasses_errors.mli
+++ b/pretyping/typeclasses_errors.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: typeclasses_errors.mli 11105 2008-06-11 13:47:21Z msozeau $ i*)
+(*i $Id: typeclasses_errors.mli 11282 2008-07-28 11:51:53Z msozeau $ i*)
 
 (*i*)
 open Names
@@ -29,7 +29,7 @@ type typeclass_error =
     | UnboundMethod of global_reference * identifier located (* Class name, method *)
     | NoInstance of identifier located * constr list
     | UnsatisfiableConstraints of evar_defs * (evar_info * hole_kind) option
-    | MismatchedContextInstance of contexts * constr_expr list * named_context (* found, expected *)
+    | MismatchedContextInstance of contexts * constr_expr list * rel_context (* found, expected *)
 
 exception TypeClassError of env * typeclass_error
 
@@ -41,4 +41,4 @@ val no_instance : env -> identifier located -> constr list -> 'a
 
 val unsatisfiable_constraints : env -> evar_defs -> evar option -> 'a
 
-val mismatched_ctx_inst : env -> contexts -> constr_expr list -> named_context -> 'a
+val mismatched_ctx_inst : env -> contexts -> constr_expr list -> rel_context -> 'a
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index fc812594..b3c920a2 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: unification.ml 11157 2008-06-21 10:45:51Z herbelin $ *)
+(* $Id: unification.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
 
 open Pp
 open Util
@@ -239,9 +239,9 @@ let unify_0_with_initial_metas subst conv_at_top env sigma cv_pb flags m n =
       | Some c ->
 	  unirec_rec curenv pb b substn cM (whd_betaiotazeta (mkApp(c,l2)))
       | None ->
-      error_cannot_unify env sigma (cM,cN)
+      error_cannot_unify curenv sigma (cM,cN)
     else
-      error_cannot_unify env sigma (cM,cN)
+      error_cannot_unify curenv sigma (cM,cN)
 
   in
     if (not(occur_meta m)) &&