From 86116b181bb866c7f63a37796e1388f731ce7204 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 26 Jan 2017 11:38:19 +0100
Subject: [native comp] Improve error message on linking error.

The native compiler doesn't support `Require` inside `Module` sections
in some cases, we improve the error message. See:

https://coq.inria.fr/bugs/show_bug.cgi?id=4335

This patch improves the error message and gives the user some
feedback.
---
 kernel/safe_typing.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 8b28cd87bd..7e28b1c567 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -795,7 +795,10 @@ type compiled_library = {
 type native_library = Nativecode.global list
 
 let get_library_native_symbols senv dir =
-  DPMap.find dir senv.native_symbols
+  try DPMap.find dir senv.native_symbols
+  with Not_found -> Errors.errorlabstrm "get_library_native_symbols"
+                      Pp.((str "Linker error in the native compiler. Are you using Require inside a nested Module declaration?") ++ fnl () ++
+                          (str "This use case is not supported, but disabling the native compiler may help."))
 
 (** FIXME: MS: remove?*)
 let current_modpath senv = senv.modpath
-- 
cgit v1.2.3


From f5923c2174fbb419397f127af31ab1cd0b223e0a Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 31 Jan 2017 06:36:25 +0100
Subject: Fixing #5311 (anomaly on unexpected intro pattern).

This was introduced in 8.5 while reorganizing the structure of
intro-patterns.
---
 tactics/tacinterp.ml          |  2 +-
 test-suite/bugs/closed/5331.v | 11 +++++++++++
 2 files changed, 12 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/bugs/closed/5331.v

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 23d188aa73..2cfd2d6b12 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -894,7 +894,7 @@ let interp_or_and_intro_pattern_option ist env sigma = function
       (match coerce_to_intro_pattern env (Id.Map.find id ist.lfun) with
       | IntroAction (IntroOrAndPattern l) -> sigma, Some (loc,l)
       | _ ->
-        raise (CannotCoerceTo "a disjunctive/conjunctive introduction pattern"))
+        user_err_loc (loc,"", str "Cannot coerce to a disjunctive/conjunctive pattern."))
   | Some (ArgArg (loc,l)) ->
       let sigma,l = interp_or_and_intro_pattern ist env sigma l in
       sigma, Some (loc,l)
diff --git a/test-suite/bugs/closed/5331.v b/test-suite/bugs/closed/5331.v
new file mode 100644
index 0000000000..0d72fcb5df
--- /dev/null
+++ b/test-suite/bugs/closed/5331.v
@@ -0,0 +1,11 @@
+(* Checking no anomaly on some unexpected intropattern *)
+
+Ltac ih H := induction H as H.
+Ltac ih' H H' := induction H as H'.
+
+Goal True -> True.
+Fail intro H; ih H.
+intro H; ih' H ipattern:[].
+exact I.
+Qed.
+
-- 
cgit v1.2.3