Imported Upstream version 8.4pl4dfsgupstream/8.4pl4dfsg

56 files changed, 151 insertions, 126 deletions

diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml
index 92378837..78290e03 100644
--- a/pretyping/arguments_renaming.ml
+++ b/pretyping/arguments_renaming.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/pretyping/arguments_renaming.mli b/pretyping/arguments_renaming.mli
index a4121623..74c4cdc3 100644
--- a/pretyping/arguments_renaming.mli
+++ b/pretyping/arguments_renaming.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 38355cf1..57857351 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -391,7 +391,7 @@ let adjust_tomatch_to_pattern pb ((current,typ),deps,dep) =
 		let _ = e_cumul pb.env pb.evdref indt typ in
 		current
 	      else
-		(evd_comb2 (Coercion.inh_conv_coerce_to dummy_loc pb.env)
+		(evd_comb2 (Coercion.inh_conv_coerce_to true dummy_loc pb.env)
 		  pb.evdref (make_judge current typ) (mk_tycon_type indt)).uj_val in
 	    let sigma =  !(pb.evdref) in
 	    (current,try_find_ind pb.env sigma indt names))
@@ -1680,7 +1680,7 @@ let extract_arity_signature env0 tomatchl tmsign =
 let inh_conv_coerce_to_tycon loc env evdref j tycon =
   match tycon with
     | Some p ->
-	let (evd',j) = Coercion.inh_conv_coerce_to loc env !evdref j p in
+	let (evd',j) = Coercion.inh_conv_coerce_to true loc env !evdref j p in
           evdref := evd';
           j
     | None -> j
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index 566c172d..826d68a4 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index 9429086c..08ec25be 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli
index 08e52ff7..eb0abe97 100644
--- a/pretyping/cbv.mli
+++ b/pretyping/cbv.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index ddc99e0e..59f3c740 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index 675ccbbc..0136b90c 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 86f96c7c..917856a2 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -36,7 +36,7 @@ module type S = sig
      inserts a coercion into [j], if needed, in such a way it gets as
      type a product; it returns [j] if no coercion is applicable *)
   val inh_app_fun :
-    env -> evar_map -> unsafe_judgment -> evar_map * unsafe_judgment
+    bool -> env -> evar_map -> unsafe_judgment -> evar_map * unsafe_judgment
 
   (* [inh_coerce_to_sort env evd j] coerces [j] to a type; i.e. it
      inserts a coercion into [j], if needed, in such a way it gets as
@@ -57,10 +57,10 @@ module type S = sig
   (* [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 *)
-  val inh_conv_coerce_to : loc ->
+  val inh_conv_coerce_to : bool -> loc ->
     env -> evar_map -> unsafe_judgment -> type_constraint_type -> evar_map * unsafe_judgment
 
-  val inh_conv_coerce_rigid_to : loc ->
+  val inh_conv_coerce_rigid_to : bool -> loc ->
     env -> evar_map -> unsafe_judgment -> type_constraint_type -> evar_map * unsafe_judgment
 
   (* [inh_conv_coerces_to loc env evd t t'] checks if an object of type [t]
@@ -140,9 +140,11 @@ module Default = struct
 	      lookup_path_to_fun_from env evd j.uj_type in
 	      (evd,apply_coercion env evd p j t)
 
-  let inh_app_fun env evd j =
+  let inh_app_fun resolve_tc env evd j =
     try inh_app_fun env evd j
-    with Not_found ->
+    with
+    | Not_found when not resolve_tc -> (evd, j)
+    | Not_found ->
       try inh_app_fun env (saturate_evd env evd) j
       with Not_found -> (evd, j)
 
@@ -221,13 +223,15 @@ module Default = struct
     | _ -> raise NoCoercion
 
   (* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *)
-  let inh_conv_coerce_to_gen rigidonly loc env evd cj (n, t) =
+  let inh_conv_coerce_to_gen resolve_tc rigidonly loc env evd cj (n, t) =
     match n with
 	None ->
 	  let (evd', val') =
 	    try
 	      inh_conv_coerce_to_fail loc env evd rigidonly (Some cj.uj_val) cj.uj_type t
-	    with NoCoercion ->
+	    with
+            | NoCoercion when not resolve_tc -> error_actual_type_loc loc env evd cj t
+            | NoCoercion ->
 	      let evd = saturate_evd env evd in
 		try
 		  inh_conv_coerce_to_fail loc env evd rigidonly (Some cj.uj_val) cj.uj_type t
@@ -238,8 +242,8 @@ module Default = struct
 	    (evd',{ uj_val = val'; uj_type = t })
       | Some (init, cur) -> (evd, cj)
 
-  let inh_conv_coerce_to = inh_conv_coerce_to_gen false
-  let inh_conv_coerce_rigid_to = inh_conv_coerce_to_gen true
+  let inh_conv_coerce_to resolve_tc = inh_conv_coerce_to_gen resolve_tc false
+  let inh_conv_coerce_rigid_to resolve_tc = inh_conv_coerce_to_gen resolve_tc true
 
 
     let inh_conv_coerces_to loc env (evd : evar_map) t (abs, t') =
diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli
index 4c4725b3..f06f58f4 100644
--- a/pretyping/coercion.mli
+++ b/pretyping/coercion.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -18,11 +18,13 @@ open Glob_term
 module type S = sig
   (** {6 Coercions. } *)
 
-  (** [inh_app_fun env isevars j] coerces [j] to a function; i.e. it
+  (** [inh_app_fun resolve_tc env isevars j] coerces [j] to a function; i.e. it
      inserts a coercion into [j], if needed, in such a way it gets as
-     type a product; it returns [j] if no coercion is applicable *)
+     type a product; it returns [j] if no coercion is applicable.
+     resolve_tc=false disables resolving type classes (as the last
+     resort before failing) *)
   val inh_app_fun :
-    env -> evar_map -> unsafe_judgment -> evar_map * unsafe_judgment
+    bool -> env -> evar_map -> unsafe_judgment -> evar_map * unsafe_judgment
 
   (** [inh_coerce_to_sort env isevars j] coerces [j] to a type; i.e. it
      inserts a coercion into [j], if needed, in such a way it gets as
@@ -40,13 +42,15 @@ module type S = sig
   val inh_coerce_to_prod : loc ->
     env -> evar_map -> type_constraint_type -> evar_map * type_constraint_type
 
-  (** [inh_conv_coerce_to loc env isevars j t] coerces [j] to an object of type
+  (** [inh_conv_coerce_to resolve_tc 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
-     [j.uj_type] are convertible; it fails if no coercion is applicable *)
-  val inh_conv_coerce_to : loc ->
+     [j.uj_type] are convertible; it fails if no coercion is applicable.
+     resolve_tc=false disables resolving type classes (as the last
+     resort before failing) *)
+  val inh_conv_coerce_to : bool -> loc ->
     env -> evar_map -> unsafe_judgment -> type_constraint_type -> evar_map * unsafe_judgment
 
-  val inh_conv_coerce_rigid_to : loc ->
+  val inh_conv_coerce_rigid_to : bool -> loc ->
     env -> evar_map -> unsafe_judgment -> type_constraint_type -> evar_map * unsafe_judgment
 
   (** [inh_conv_coerces_to loc env isevars t t'] checks if an object of type [t]
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 1065aec9..9e808dd4 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index cd017ba7..bbd94cfe 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index f0019448..8b421ea3 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -20,6 +20,17 @@ open Evarutil
 open Libnames
 open Evd
 
+let debug_unification = ref (false)
+let _ = Goptions.declare_bool_option {
+  Goptions.optsync = true; Goptions.optdepr = false;
+  Goptions.optname =
+    "Print states sended to Evarconv unification";
+  Goptions.optkey = ["Debug";"Unification"];
+  Goptions.optread = (fun () -> !debug_unification);
+  Goptions.optwrite = (fun a -> debug_unification:=a);
+}
+
+
 type flex_kind_of_term =
   | Rigid of constr
   | PseudoRigid of constr (* approximated as rigid but not necessarily so *)
@@ -210,6 +221,13 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false)
   in
 
   (* Evar must be undefined since we have flushed evars *)
+  let () = if !debug_unification then
+	     let open Pp in
+	     let pr_state (tm,l) =
+	       h 0 (Termops.print_constr tm ++ str "|" ++ cut ()
+		    ++ prlist_with_sep pr_semicolon
+				       (fun x -> hov 1 (Termops.print_constr x)) l) in
+	     pp (v 0 (pr_state appr1 ++ cut () ++ pr_state appr2 ++ cut ()) ++ fnl ()) in
   match (flex_kind_of_term term1 l1, flex_kind_of_term term2 l2) with
     | Flexible (sp1,al1 as ev1), Flexible (sp2,al2 as ev2) ->
 	let f1 i =
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index dd68f16f..3a352d13 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index fc29ba6c..05b7e443 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -1180,17 +1180,28 @@ let invert_invertible_arg fullenv evd aliases k (evk,argsv) args' =
  * such that "hyps' |- ?e : T"
  *)
 
-let filter_candidates evd evk filter candidates =
+let filter_effective_candidates evi filter candidates =
+  match filter with
+  | None -> candidates
+  | Some filter ->
+      let ids = List.map pi1 (list_filter_with filter (evar_context evi)) in
+      List.filter (fun a -> list_subset (Idset.elements (collect_vars a)) ids)
+        candidates
+
+let filter_candidates evd evk filter candidates_update =
   let evi = Evd.find_undefined evd evk in
-  let candidates = match candidates with
+  let candidates = match candidates_update with
   | None -> evi.evar_candidates
-  | Some _ -> candidates in
-  match candidates,filter with
-  | None,_ | _, None -> candidates
-  | Some l, Some filter ->
-      let ids = List.map pi1 (list_filter_with filter (evar_context evi)) in
-      Some (List.filter (fun a ->
-        list_subset (Idset.elements (collect_vars a)) ids) l)
+  | Some _ -> candidates_update
+  in
+  match candidates with
+  | None -> None
+  | Some l ->
+      let l' = filter_effective_candidates evi filter l in
+      if List.length l = List.length l' && candidates_update = None then
+        None
+      else
+        Some l'
 
 let closure_of_filter evd evk filter =
   let evi = Evd.find_undefined evd evk in
@@ -1530,6 +1541,7 @@ let solve_candidates conv_algo env evd (evk,argsv as ev) rhs =
 
 exception NotInvertibleUsingOurAlgorithm of constr
 exception NotEnoughInformationToProgress of (identifier * evar_projection) list
+exception NotEnoughInformationEvarEvar of constr
 exception OccurCheckIn of evar_map * constr
 
 let rec invert_definition conv_algo choose env evd (evk,argsv as ev) rhs =
@@ -1608,7 +1620,8 @@ let rec invert_definition conv_algo choose env evd (evk,argsv as ev) rhs =
         with
         | EvarSolvedOnTheFly (evd,t) -> evdref:=evd; imitate envk t
         | CannotProject filter' ->
-	  assert !progress;
+          if not !progress then
+            raise (NotEnoughInformationEvarEvar t);
 	  (* Make the virtual left evar real *)
 	  let ty = get_type_of env' !evdref t in
 	  let (evd,evar'',ev'') =
@@ -1714,6 +1727,8 @@ and evar_define conv_algo ?(choose=false) env evd (evk,argsv as ev) rhs =
   with
     | NotEnoughInformationToProgress sols ->
 	postpone_non_unique_projection env evd ev sols rhs
+    | NotEnoughInformationEvarEvar t ->
+        add_conv_pb (Reduction.CONV,env,mkEvar ev,t) evd
     | NotInvertibleUsingOurAlgorithm t ->
 	error_not_clean env evd evk t (evar_source evk evd)
     | OccurCheckIn (evd,rhs) ->
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 591a008c..9269f138 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 4d9eb897..72dc27e6 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index dbaf803b..d5bf2f68 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml
index 8e4b211f..b7023db0 100644
--- a/pretyping/glob_term.ml
+++ b/pretyping/glob_term.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -359,27 +359,6 @@ let rec cases_pattern_of_glob_constr na = function
       PatCstr (loc,cstr,args,na)
   | _ -> raise Not_found
 
-let rec cases_pattern_of_glob_constr na = function
-  | GVar (loc,id) when na<>Anonymous ->
-      (* Unable to manage the presence of both an alias and a variable *)
-      raise Not_found
-  | GVar (loc,id) -> PatVar (loc,Name id)
-  | GHole (loc,_) -> PatVar (loc,na)
-  | GRef (loc,ConstructRef cstr) ->
-      PatCstr (loc,cstr,[],na)
-  | GApp (loc,GRef (_,ConstructRef (ind,_ as cstr)),args) ->
-      let mib,_ = Global.lookup_inductive ind in
-      let nparams = mib.Declarations.mind_nparams in
-      if nparams > List.length args then
-        user_err_loc (loc,"",Pp.str "Invalid notation for pattern.");
-      let params,args = list_chop nparams args in
-      List.iter (function GHole _ -> ()
-	| _ -> user_err_loc (loc,"",Pp.str"Invalid notation for pattern."))
-        params;
-      let args = List.map (cases_pattern_of_glob_constr Anonymous) args in
-      PatCstr (loc,cstr,args,na)
-  | _ -> raise Not_found
-
 (* Turn a closed cases pattern into a glob_constr *)
 let rec glob_constr_of_closed_cases_pattern_aux = function
   | PatCstr (loc,cstr,[],Anonymous) ->
diff --git a/pretyping/glob_term.mli b/pretyping/glob_term.mli
index 798a960f..09dd9203 100644
--- a/pretyping/glob_term.mli
+++ b/pretyping/glob_term.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 18d30bfd..c7cdb302 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli
index 1bf5fd90..19c70dc0 100644
--- a/pretyping/indrec.mli
+++ b/pretyping/indrec.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index bdccc57b..5bfc57bf 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 91662fd9..133d7013 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/pretyping/matching.ml b/pretyping/matching.ml
index d99b8c9f..b86f3e45 100644
--- a/pretyping/matching.ml
+++ b/pretyping/matching.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/pretyping/matching.mli b/pretyping/matching.mli
index 9b412692..1a47b714 100644
--- a/pretyping/matching.mli
+++ b/pretyping/matching.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml
index e5dd75c0..76b9bd8a 100644
--- a/pretyping/namegen.ml
+++ b/pretyping/namegen.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/pretyping/namegen.mli b/pretyping/namegen.mli
index e23c6dad..db078026 100644
--- a/pretyping/namegen.mli
+++ b/pretyping/namegen.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 7e486956..553615c2 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli
index f6d55bc6..7fb53133 100644
--- a/pretyping/pattern.mli
+++ b/pretyping/pattern.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 672debfa..52122974 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index 68ea67f7..75962d11 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 1dd71fab..08e8df05 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -200,11 +200,11 @@ sig
    * Unused outside, but useful for debugging
    *)
   val pretype :
-    type_constraint -> env -> evar_map ref ->
+    bool -> type_constraint -> env -> evar_map ref ->
     ltac_var_map -> glob_constr -> unsafe_judgment
 
   val pretype_type :
-    val_constraint -> env -> evar_map ref ->
+    bool -> val_constraint -> env -> evar_map ref ->
     ltac_var_map -> glob_constr -> unsafe_type_judgment
 
   val pretype_gen :
@@ -259,9 +259,9 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	done
 
   (* coerce to tycon if any *)
-  let inh_conv_coerce_to_tycon loc env evdref j = function
+  let inh_conv_coerce_to_tycon resolve_tc loc env evdref j = function
     | None -> j
-    | Some t -> evd_comb2 (Coercion.inh_conv_coerce_to loc env) evdref j t
+    | Some t -> evd_comb2 (Coercion.inh_conv_coerce_to resolve_tc loc env) evdref j t
 
   let push_rels vars env = List.fold_right push_rel vars env
 
@@ -297,18 +297,19 @@ module Pretyping_F (Coercion : Coercion.S) = struct
       let c = substl subst c in
       { uj_val = c; uj_type = protected_get_type_of env sigma c }
     with Not_found ->
-    (* Check if [id] is a section or goal variable *)
-    try
-      let (_,_,typ) = lookup_named id env in
-      { uj_val  = mkVar id; uj_type = typ }
-    with Not_found ->
-    (* [id] not found, build nice error message if [id] yet known from ltac *)
+    (* if [id] an ltac variable not bound to a term *)
+    (* build a nice error message *)
     try
       match List.assoc id unbndltacvars with
       | None -> user_err_loc (loc,"",
 	  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 ->
+    (* Check if [id] is a section or goal variable *)
+    try
+      let (_,_,typ) = lookup_named id env in
+      { uj_val  = mkVar id; uj_type = typ }
+    with Not_found ->
     (* [id] not found, standard error message *)
       error_var_not_found_loc loc id
 
@@ -346,7 +347,11 @@ module Pretyping_F (Coercion : Coercion.S) = struct
   (* [pretype tycon env evdref lvar lmeta cstr] attempts to type [cstr] *)
   (* in environment [env], with existential variables [evdref] and *)
   (* the type constraint tycon *)
-  let rec pretype (tycon : type_constraint) env evdref lvar = function
+  let rec pretype resolve_tc (tycon : type_constraint) env evdref lvar t =
+    let pretype = pretype resolve_tc in
+    let pretype_type = pretype_type resolve_tc in
+    let inh_conv_coerce_to_tycon = inh_conv_coerce_to_tycon resolve_tc in
+    match t with
     | GRef (loc,ref) ->
 	inh_conv_coerce_to_tycon loc env evdref
 	  (pretype_ref loc evdref env ref)
@@ -459,7 +464,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	  | [] -> resj
 	  | c::rest ->
 	      let argloc = loc_of_glob_constr c in
-	      let resj = evd_comb1 (Coercion.inh_app_fun env) evdref resj in
+	      let resj = evd_comb1 (Coercion.inh_app_fun resolve_tc env) evdref resj in
               let resty = whd_betadeltaiota env !evdref resj.uj_type in
       		match kind_of_term resty with
 		  | Prod (na,c1,c2) ->
@@ -696,7 +701,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	in inh_conv_coerce_to_tycon loc env evdref cj tycon
 
   (* [pretype_type valcon env evdref lvar c] coerces [c] into a type *)
-  and pretype_type valcon env evdref lvar = function
+  and pretype_type resolve_tc valcon env evdref lvar = function
     | GHole loc ->
 	(match valcon with
 	   | Some v ->
@@ -716,7 +721,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 		 { utj_val = e_new_evar evdref env ~src:loc (mkSort s);
 		   utj_type = s})
     | c ->
-	let j = pretype empty_tycon env evdref lvar c in
+	let j = pretype resolve_tc empty_tycon env evdref lvar c in
 	let loc = loc_of_glob_constr c in
 	let tj = evd_comb1 (Coercion.inh_coerce_to_sort loc env) evdref j in
 	  match valcon with
@@ -731,9 +736,9 @@ module Pretyping_F (Coercion : Coercion.S) = struct
     let c' = match kind with
       | OfType exptyp ->
 	  let tycon = match exptyp with None -> empty_tycon | Some t -> mk_tycon t in
-	  (pretype tycon env evdref lvar c).uj_val
+	  (pretype resolve_classes tycon env evdref lvar c).uj_val
       | IsType ->
-	  (pretype_type empty_valcon env evdref lvar c).utj_val 
+	  (pretype_type resolve_classes empty_valcon env evdref lvar c).utj_val 
     in
       resolve_evars env evdref fail_evar resolve_classes;
       let c = if expand_evar then nf_evar !evdref c' else c' in
@@ -747,14 +752,14 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 
   let understand_judgment sigma env c =
     let evdref = ref sigma in
-    let j = pretype empty_tycon env evdref ([],[]) c in
+    let j = pretype true empty_tycon env evdref ([],[]) c in
       resolve_evars env evdref true true;
       let j = j_nf_evar !evdref j in
 	check_evars env sigma !evdref (mkCast(j.uj_val,DEFAULTcast, j.uj_type));
 	j
 
   let understand_judgment_tcc evdref env c =
-    let j = pretype empty_tycon env evdref ([],[]) c in
+    let j = pretype true empty_tycon env evdref ([],[]) c in
       resolve_evars env evdref false true;
       j_nf_evar !evdref j
 
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 761e1641..a785b432 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -93,11 +93,11 @@ sig
   (**/**)
   (** Internal of Pretyping... *)
   val pretype :
-    type_constraint -> env -> evar_map ref ->
+    bool -> type_constraint -> env -> evar_map ref ->
     ltac_var_map -> glob_constr -> unsafe_judgment
 
   val pretype_type :
-    val_constraint -> env -> evar_map ref ->
+    bool -> val_constraint -> env -> evar_map ref ->
     ltac_var_map -> glob_constr -> unsafe_type_judgment
 
   val pretype_gen :
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 434fe80c..f9cd3501 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 1c19ef6c..442e51db 100644
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 993ad46b..7c348d97 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 6f7f9de3..f508ea6c 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 3f6acfcb..1e1960f5 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli
index 62bda6ef..4ef54c13 100644
--- a/pretyping/retyping.mli
+++ b/pretyping/retyping.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 78b239c0..b18314f7 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index f2a4c303..aec9da95 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/pretyping/term_dnet.ml b/pretyping/term_dnet.ml
index 3340dbe2..28a6c92c 100644
--- a/pretyping/term_dnet.ml
+++ b/pretyping/term_dnet.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/pretyping/term_dnet.mli b/pretyping/term_dnet.mli
index bf4557fc..9e629dcd 100644
--- a/pretyping/term_dnet.mli
+++ b/pretyping/term_dnet.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 0e31ee2d..02661a93 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 0e384829..81b23d7e 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 0344ebcc..2b5b7fe2 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index c458e5d5..91069b70 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index 19e18489..da5dc909 100644
--- a/pretyping/typeclasses_errors.ml
+++ b/pretyping/typeclasses_errors.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli
index cb67c73d..6e0fc6ad 100644
--- a/pretyping/typeclasses_errors.mli
+++ b/pretyping/typeclasses_errors.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 22aacb29..9fbfc197 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index 88dc895e..5aa0a2d4 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index fd045690..d6b1e2e4 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -794,7 +794,7 @@ let is_mimick_head ts f =
 
 let try_to_coerce env evd c cty tycon =
   let j = make_judge c cty in
-  let (evd',j') = inh_conv_coerce_rigid_to dummy_loc env evd j tycon in
+  let (evd',j') = inh_conv_coerce_rigid_to true dummy_loc env evd j tycon in
   let evd' = Evarconv.consider_remaining_unif_problems env evd' in
   let evd' = Evd.map_metas_fvalue (nf_evar evd') evd' in
     (evd',j'.uj_val)
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index 1ec5c1a2..75bddc1f 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 3966146d..047971d5 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/pretyping/vnorm.mli b/pretyping/vnorm.mli
index ca370b55..a0cf2372 100644
--- a/pretyping/vnorm.mli
+++ b/pretyping/vnorm.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)