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.

2 files changed, 28 insertions, 1 deletions

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.
+*)