Imported Upstream version 8.5upstream/8.5

35 files changed, 73 insertions, 65 deletions

diff --git a/interp/constrarg.ml b/interp/constrarg.ml
index a7241399..d9c60a18 100644
--- a/interp/constrarg.ml
+++ b/interp/constrarg.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/interp/constrarg.mli b/interp/constrarg.mli
index fdeddd66..ebef1ada 100644
--- a/interp/constrarg.mli
+++ b/interp/constrarg.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 2d48ea4d..16447002 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli
index 10c84b8d..3f5be485 100644
--- a/interp/constrexpr_ops.mli
+++ b/interp/constrexpr_ops.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index f57772ec..9df8f9c2 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -147,8 +147,17 @@ let extern_evar loc n l = CEvar (loc,n,l)
     For instance, in the debugger the tables of global references
     may be inaccurate *)
 
+let safe_shortest_qualid_of_global vars r =
+  try shortest_qualid_of_global vars r
+  with Not_found ->
+    match r with
+    | VarRef v -> make_qualid DirPath.empty v
+    | ConstRef c -> make_qualid DirPath.empty Names.(Label.to_id (con_label c))
+    | IndRef (i,_) | ConstructRef ((i,_),_) ->
+        make_qualid DirPath.empty Names.(Label.to_id (mind_label i))
+
 let default_extern_reference loc vars r =
-  Qualid (loc,shortest_qualid_of_global vars r)
+  Qualid (loc,safe_shortest_qualid_of_global vars r)
 
 let my_extern_reference = ref default_extern_reference
 
@@ -438,8 +447,8 @@ let is_projection nargs = function
   | Some r when not !Flags.in_debugger && not !Flags.raw_print && !print_projections ->
     (try
        let n = Recordops.find_projection_nparams r + 1 in
-	 if n <= nargs then None
-	 else Some n
+	 if n <= nargs then Some n
+	 else None
      with Not_found -> None)
   | _ -> None
 	
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index b797e455..bf1f529c 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index c754f191..a7b1bb41 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -317,7 +317,7 @@ let rec it_mkGLambda loc2 env body =
 let build_impls = function
   |Implicit -> (function
 		  |Name id ->  Some (id, Impargs.Manual, (true,true))
-		  |Anonymous -> anomaly (Pp.str "Anonymous implicit argument"))
+		  |Anonymous -> Some (Id.of_string "_", Impargs.Manual, (true,true)))
   |Explicit -> fun _ -> None
 
 let impls_type_list ?(args = []) =
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index b671c988..22cf910b 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index 5ac718e3..9e517381 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/interp/coqlib.mli b/interp/coqlib.mli
index 41204a71..5ba26d82 100644
--- a/interp/coqlib.mli
+++ b/interp/coqlib.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index c18ceeca..0d9d021c 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -139,12 +139,15 @@ let interval loc =
   loc1, loc2-1
 
 let dump_ref loc filepath modpath ident ty =
-  if !glob_output = Feedback then
+  match !glob_output with
+  | Feedback ->
     Pp.feedback (Feedback.GlobRef (loc, filepath, modpath, ident, ty))
-  else
+  | NoGlob -> ()
+  | _ when not (Loc.is_ghost loc) ->
     let bl,el = interval loc in
     dump_string (Printf.sprintf "R%d:%d %s %s %s %s\n"
 		  bl el filepath modpath ident ty)
+  | _ -> ()
 
 let dump_reference loc modpath ident ty =
   let filepath = Names.DirPath.to_string (Lib.library_dp ()) in
diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli
index 428189be..a7c79911 100644
--- a/interp/dumpglob.mli
+++ b/interp/dumpglob.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/interp/genintern.ml b/interp/genintern.ml
index 7795946d..47b71735 100644
--- a/interp/genintern.ml
+++ b/interp/genintern.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/interp/genintern.mli b/interp/genintern.mli
index 28f4f530..4b244b38 100644
--- a/interp/genintern.mli
+++ b/interp/genintern.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 87f7a6d6..391c600e 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index eee92898..b226bfa0 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/interp/interp.mllib b/interp/interp.mllib
index c9a03152..96b52959 100644
--- a/interp/interp.mllib
+++ b/interp/interp.mllib
@@ -3,12 +3,12 @@ Constrarg
 Genintern
 Constrexpr_ops
 Notation_ops
-Topconstr
 Ppextend
 Notation
 Dumpglob
 Syntax_def
 Smartlocate
+Topconstr
 Reserve
 Impargs
 Implicit_quantifiers
diff --git a/interp/modintern.ml b/interp/modintern.ml
index 35e73113..e5dce5cc 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/interp/modintern.mli b/interp/modintern.mli
index 8b6d002e..1e04ada1 100644
--- a/interp/modintern.mli
+++ b/interp/modintern.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/interp/notation.ml b/interp/notation.ml
index d18b804b..5c10e0af 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/interp/notation.mli b/interp/notation.mli
index 38bd5fc7..7885814c 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 2762dc0b..51dfadac 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli
index c6770dee..280ccfd2 100644
--- a/interp/notation_ops.mli
+++ b/interp/notation_ops.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/interp/ppextend.ml b/interp/ppextend.ml
index cb12b98a..37bbe0ce 100644
--- a/interp/ppextend.ml
+++ b/interp/ppextend.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/interp/ppextend.mli b/interp/ppextend.mli
index 0385eea2..de7a42ee 100644
--- a/interp/ppextend.mli
+++ b/interp/ppextend.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 3100298e..7e42c1a2 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/interp/reserve.mli b/interp/reserve.mli
index 6cae2b02..9c77400d 100644
--- a/interp/reserve.mli
+++ b/interp/reserve.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml
index ce3c9b8f..1f28ba65 100644
--- a/interp/smartlocate.ml
+++ b/interp/smartlocate.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/interp/smartlocate.mli b/interp/smartlocate.mli
index 68ef6594..0749ca57 100644
--- a/interp/smartlocate.mli
+++ b/interp/smartlocate.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/interp/stdarg.ml b/interp/stdarg.ml
index e155a521..9c3ed941 100644
--- a/interp/stdarg.ml
+++ b/interp/stdarg.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/interp/stdarg.mli b/interp/stdarg.mli
index 5a44b1ca..d8904dab 100644
--- a/interp/stdarg.mli
+++ b/interp/stdarg.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index d2709d5e..db548ec3 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli
index e5a3f4ce..7a1c9c5c 100644
--- a/interp/syntax_def.mli
+++ b/interp/syntax_def.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 1231f115..cc8e697e 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -38,27 +38,11 @@ let error_invalid_pattern_notation loc =
 (**********************************************************************)
 (* Functions on constr_expr *)
 
-let ids_of_cases_indtype =
-  let rec vars_of ids = function
-    (* We deal only with the regular cases *)
-    | (CPatCstr (_,_,l1,l2)|CPatNotation (_,_,(l1,[]),l2)) ->
-      List.fold_left vars_of (List.fold_left vars_of [] l2) l1
-    (* assume the ntn is applicative and does not instantiate the head !! *)
-    | CPatDelimiters(_,_,c) -> vars_of ids c
-    | CPatAtom (_, Some (Libnames.Ident (_, x))) -> x::ids
-    | _ -> ids in
-  vars_of []
-
-let ids_of_cases_tomatch tms =
-  List.fold_right
-    (fun (_,(ona,indnal)) l ->
-      Option.fold_right (fun t -> (@) (ids_of_cases_indtype t))
-      indnal (Option.fold_right (Loc.down_located name_cons) ona l))
-    tms []
-
 let is_constructor id =
-  try ignore (Nametab.locate_extended (qualid_of_ident id)); true
-  with Not_found -> true
+  try Globnames.isConstructRef
+        (Smartlocate.global_of_extended_global
+           (Nametab.locate_extended (qualid_of_ident id)))
+  with Not_found -> false
 
 let rec cases_pattern_fold_names f a = function
   | CPatRecord (_, l) ->
@@ -82,6 +66,17 @@ let ids_of_pattern_list =
       (List.fold_left (cases_pattern_fold_names Id.Set.add)))
     Id.Set.empty
 
+let ids_of_cases_indtype p =
+  Id.Set.elements (cases_pattern_fold_names Id.Set.add Id.Set.empty p)
+
+let ids_of_cases_tomatch tms =
+  List.fold_right
+    (fun (_,(ona,indnal)) l ->
+      Option.fold_right (fun t ids -> cases_pattern_fold_names Id.Set.add ids t)
+      indnal
+        (Option.fold_right (Loc.down_located (name_fold Id.Set.add)) ona l))
+    tms Id.Set.empty
+
 let rec fold_constr_expr_binders g f n acc b = function
   | (nal,bk,t)::l ->
       let nal = snd (List.split nal) in
@@ -119,7 +114,7 @@ let fold_constr_expr_with_binders g f n acc = function
   | CRecord (loc,_,l) -> List.fold_left (fun acc (id, c) -> f n acc c) acc l
   | CCases (loc,sty,rtnpo,al,bl) ->
       let ids = ids_of_cases_tomatch al in
-      let acc = Option.fold_left (f (List.fold_right g ids n)) acc rtnpo in
+      let acc = Option.fold_left (f (Id.Set.fold g ids n)) acc rtnpo in
       let acc = List.fold_left (f n) acc (List.map fst al) in
       List.fold_right (fun (loc,patl,rhs) acc ->
 	let ids = ids_of_pattern_list patl in
@@ -220,10 +215,11 @@ let map_constr_expr_with_binders g f e = function
   | CPrim _ | CRef _ as x -> x
   | CRecord (loc,p,l) -> CRecord (loc,p,List.map (fun (id, c) -> (id, f e c)) l)
   | CCases (loc,sty,rtnpo,a,bl) ->
-      (* TODO: apply g on the binding variables in pat... *)
-      let bl = List.map (fun (loc,pat,rhs) -> (loc,pat,f e rhs)) bl in
+      let bl = List.map (fun (loc,patl,rhs) ->
+        let ids = ids_of_pattern_list patl in
+        (loc,patl,f (Id.Set.fold g ids e) rhs)) bl in
       let ids = ids_of_cases_tomatch a in
-      let po = Option.map (f (List.fold_right g ids e)) rtnpo in
+      let po = Option.map (f (Id.Set.fold g ids e)) rtnpo in
       CCases (loc, sty, po, List.map (fun (tm,x) -> (f e tm,x)) a,bl)
   | CLetTuple (loc,nal,(ona,po),b,c) ->
       let e' = List.fold_right (Loc.down_located (name_fold g)) nal e in
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index b25d7082..1e867c19 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)