From 1a5130702303e2843ab458e2566bef293c6947cd Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Mon, 20 Jun 2016 14:28:02 -0400 Subject: parenthesize Ltac [constr:] arguments --- src/Tactics/Nsatz.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src/Tactics') diff --git a/src/Tactics/Nsatz.v b/src/Tactics/Nsatz.v index 3eb3647a1..8fa8c4a86 100644 --- a/src/Tactics/Nsatz.v +++ b/src/Tactics/Nsatz.v @@ -25,7 +25,7 @@ Ltac nsatz_reify_equations eq zero := lazymatch (eval red in (Ncring_tac.list_reifyl (lterm:=lb))) with (?variables, ?le) => lazymatch (eval compute in (List.rev le)) with - | ?reified_goal::?reified_givens => constr:(variables, reified_givens, reified_goal) + | ?reified_goal::?reified_givens => constr:((variables, reified_givens, reified_goal)) end end. @@ -56,7 +56,7 @@ Ltac nsatz_compute_get_leading_coefficient := Ltac nsatz_compute_get_certificate := lazymatch goal with - |- Logic.eq ((?a :: _ :: ?b) :: ?c) _ -> _ => constr:(c,b) + |- Logic.eq ((?a :: _ :: ?b) :: ?c) _ -> _ => constr:((c,b)) end. Ltac nsatz_rewrite_and_revert domain := -- cgit v1.2.3