From 3df7e2a89ae931207781c6f5cbc9e196235b1dc3 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 24 Oct 2015 09:57:50 +0200
Subject: Backtracking on interpreting toplevel calls to exact in scope
 determined by the type to prove (was introduced in 35846ec22, r15978, Nov
 2012).

Not only it does not work when exact is called via a Ltac definition,
but, also, it does not scale easily to refine which is a TACTIC
EXTEND.

Ideally, one may then want to propagate scope interpretations through
ltac variables, as well as supporting refine...

See #4034 for a discussion.
---
 tactics/tacinterp.ml          |  4 +++-
 test-suite/bugs/closed/4034.v | 25 +++++++++++++++++++++++++
 2 files changed, 28 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/bugs/closed/4034.v

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 5a0d26a1cb..6c125ed2d9 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -557,7 +557,9 @@ let interp_gen kind ist allow_patvar flags env sigma (c,ce) =
         ltac_vars = constr_context;
         ltac_bound = Id.Map.domain ist.lfun;
       } in
-      intern_gen kind ~allow_patvar ~ltacvars env c
+      let kind_for_intern =
+        match kind with OfType _ -> WithoutTypeConstraint | _ -> kind in
+      intern_gen kind_for_intern ~allow_patvar ~ltacvars env c
   in
   let trace =
     push_trace (loc_of_glob_constr c,LtacConstrInterp (c,vars)) ist in
diff --git a/test-suite/bugs/closed/4034.v b/test-suite/bugs/closed/4034.v
new file mode 100644
index 0000000000..3f7be4d1c7
--- /dev/null
+++ b/test-suite/bugs/closed/4034.v
@@ -0,0 +1,25 @@
+(* This checks compatibility of interpretation scope used for exact
+   between 8.4 and 8.5. See discussion at
+   https://coq.inria.fr/bugs/show_bug.cgi?id=4034. It is not clear
+   what we would like exactly, but certainly, if exact is interpreted
+   in a special scope, it should be interpreted consistently so also
+   in ltac code. *)
+
+Record Foo := {}.
+Bind Scope foo_scope with Foo.
+Notation "!" := Build_Foo : foo_scope.
+Notation "!" := 1 : core_scope.
+Open Scope foo_scope.
+Open Scope core_scope.
+
+Goal Foo.
+  Fail exact !.
+(* ... but maybe will we want it to succeed eventually if we ever
+   would be able to make it working the same in
+
+Ltac myexact e := exact e.
+
+Goal Foo.
+  myexact !.
+Defined.
+*)
-- 
cgit v1.2.3