From 4bb42c36190c360f8d2fecc865ed9e822deddf26 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 20 Jun 2016 13:46:30 -0400 Subject: Fix nsatz_compute for 8.4 --- 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 729017590..3eb3647a1 100644 --- a/src/Tactics/Nsatz.v +++ b/src/Tactics/Nsatz.v @@ -42,9 +42,9 @@ Require Import Coq.setoid_ring.Ring_polynom. (* Kludge for 8.4/8.5 compatibility *) Module Import mynsatz_compute. Import Nsatz. - Global Ltac mynsatz_compute := nsatz_compute. + Global Ltac mynsatz_compute x := nsatz_compute x. End mynsatz_compute. -Ltac nsatz_compute := mynsatz_compute. +Ltac nsatz_compute x := mynsatz_compute x. Ltac nsatz_compute_to_goal sugar nparams reified_goal power reified_givens := nsatz_compute (PEc sugar :: PEc nparams :: PEpow reified_goal power :: reified_givens). -- cgit v1.2.3