Fixing incompatibility introduced with simpl in commit 364decf59c1 (or

maybe ca71714).

Goal 2=2+2.
match goal with |- (_ = ?c) => simpl c end.

was working in 8.4 but was failing in 8.5beta2.

Note: Changes in tacintern.ml are otherwise purely cosmetic.

3 files changed, 26 insertions, 7 deletions

diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index d4c67b90fb..fb22da83aa 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -341,7 +341,7 @@ let intern_typed_pattern ist p =
 
 let rec intern_typed_pattern_or_ref_with_occurrences ist (l,p) =
   let interp_ref r =
-    try l, Inl (intern_evaluable ist r)
+    try Inl (intern_evaluable ist r)
     with e when Logic.catchable_exception e ->
       (* Compatibility. In practice, this means that the code above
          is useless. Still the idea of having either an evaluable
@@ -356,19 +356,19 @@ let rec intern_typed_pattern_or_ref_with_occurrences ist (l,p) =
       let c = Constrintern.interp_reference sign r in
       match c with
       | GRef (_,r,None) ->
-          l, Inl (ArgArg (evaluable_of_global_reference ist.genv r,None))
+          Inl (ArgArg (evaluable_of_global_reference ist.genv r,None))
       | GVar (_,id) ->
           let r = evaluable_of_global_reference ist.genv (VarRef id) in
-          l, Inl (ArgArg (r,None))
+          Inl (ArgArg (r,None))
       | _ ->
-          l, Inr ((c,None),dummy_pat) in
-  match p with
+          Inr ((c,None),dummy_pat) in
+  (l, match p with
   | Inl r -> interp_ref r
   | Inr (CAppExpl(_,(None,r,None),[])) ->
       (* We interpret similarly @ref and ref *)
       interp_ref (AN r)
   | Inr c ->
-      l, Inr (intern_typed_pattern ist c)
+      Inr (intern_typed_pattern ist c))
 
 (* This seems fairly hacky, but it's the first way I've found to get proper
    globalization of [unfold].  --adamc *)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 374c7c7364..593e46b05c 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -678,7 +678,19 @@ let interp_constr_with_occurrences ist env sigma (occs,c) =
 
 let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, a) =
   let p = match a with
-  | Inl b -> Inl (interp_evaluable ist env sigma b)
+  | Inl (ArgVar (loc,id)) ->
+      (* This is the encoding of an ltac var supposed to be bound
+         prioritary to an evaluable reference and otherwise to a constr
+         (it is an encoding to satisfy the "union" type given to Simpl) *)
+    let coerce_eval_ref_or_constr x =
+      try Inl (coerce_to_evaluable_ref env x)
+      with CannotCoerceTo _ ->
+        let c = coerce_to_closed_constr env x in
+        Inr (pi3 (pattern_of_constr env sigma c)) in
+    (try try_interp_ltac_var coerce_eval_ref_or_constr ist (Some (env,sigma)) (loc,id)
+     with Not_found ->
+       error_global_not_found_loc loc (qualid_of_ident id))
+  | Inl (ArgArg _ as b) -> Inl (interp_evaluable ist env sigma b)
   | Inr c -> Inr (pi3 (interp_typed_pattern ist env sigma c)) in
   interp_occurrences ist occs, p
 
diff --git a/test-suite/success/simpl.v b/test-suite/success/simpl.v
index e540ae5f30..5b87e877bf 100644
--- a/test-suite/success/simpl.v
+++ b/test-suite/success/simpl.v
@@ -98,3 +98,10 @@ Fail simpl (unbox _ (unbox _ _)) at 3 4. (* Nested and even overlapping *)
 simpl (unbox _ (unbox _ _)) at 2 4.
 match goal with |- unbox _ (Box _ True) = unbox _ (Box _ True) => idtac end.
 Abort.
+
+(* Check interpretation of ltac variables (was broken in 8.5 beta 1 and 2 *)
+
+Goal 2=1+1.
+match goal with |- (_ = ?c) => simpl c end.
+match goal with |- 2 = 2 => idtac end. (* Check that it reduced *)
+Abort.