diff options
| author | Pierre-Marie Pédrot | 2017-09-05 16:27:44 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-09-05 16:27:44 +0200 |
| commit | 68e803063818235acdc6ade35767ee618f88fe89 (patch) | |
| tree | a00ddfd115a11110bf14a8ad883467a3447cff7e | |
| parent | c38e196fc175aaca2268f73107c9658c7af7d9fc (diff) | |
The absurd tactic now parses a constr.
| -rw-r--r-- | theories/Notations.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Notations.v b/theories/Notations.v index 9ecca018af..743210ae8d 100644 --- a/theories/Notations.v +++ b/theories/Notations.v @@ -435,7 +435,7 @@ Ltac2 Notation refine := Control.refine. Ltac2 absurd0 c := Control.enter (fun _ => Std.absurd (c ())). -Ltac2 Notation absurd := absurd0. +Ltac2 Notation "absurd" c(thunk(open_constr)) := absurd0 c. Ltac2 subst0 ids := match ids with | [] => Std.subst_all () |