diff options
| -rw-r--r-- | tactics/tacinterp.ml | 4 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4034.v | 25 |
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. +*) |