diff options
| -rw-r--r-- | tactics/tacintern.ml | 12 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 14 | ||||
| -rw-r--r-- | test-suite/success/simpl.v | 7 |
3 files changed, 26 insertions, 7 deletions
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index d4c67b90f..fb22da83a 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 374c7c736..593e46b05 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 e540ae5f3..5b87e877b 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. |