Basics/Tactics: restore "notypeclasses" to *hs* tacticals

HoTT · Sep 30, 2023 · e68da51 · e68da51
1 parent 8ddce30
commit e68da51
Showing 1 changed file with 4 additions and 4 deletions.
diff --git a/theories/Basics/Tactics.v b/theories/Basics/Tactics.v
@@ -485,10 +485,10 @@ Tactic Notation "snrapply_rhs_V" uconstr(term)
 
 (** The hope is that these can replace the above 32 definitions, but currently there are some issues. *)
 
-Tactic Notation "lhs" tactic3(tac) := refine (_ @ _); [ tac | ].
-Tactic Notation "lhs_V" tactic3(tac) := refine (_^ @ _); [ tac | ].
-Tactic Notation "rhs" tactic3(tac) := refine (_ @ _^); [ | tac ].
-Tactic Notation "rhs_V" tactic3(tac) := refine (_ @ _); [ | tac ].
+Tactic Notation "lhs" tactic3(tac) := nrefine (_ @ _); [ tac | ].
+Tactic Notation "lhs_V" tactic3(tac) := nrefine (_^ @ _); [ tac | ].
+Tactic Notation "rhs" tactic3(tac) := nrefine (_ @ _^); [ | tac ].
+Tactic Notation "rhs_V" tactic3(tac) := nrefine (_ @ _); [ | tac ].
 
 (** Ssreflect tactics, adapted by Robbert Krebbers *)
 Ltac done :=