diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-06-20 13:46:30 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-06-20 13:46:30 -0400 |
| commit | 4bb42c36190c360f8d2fecc865ed9e822deddf26 (patch) | |
| tree | 24d9f6c03d7685b0876b7b80acac6180e420d6d3 /src/Tactics | |
| parent | d68ece243924a969bd8b4ce6a5a4e7fb2cf23df1 (diff) | |
Fix nsatz_compute for 8.4
Diffstat (limited to 'src/Tactics')
| -rw-r--r-- | src/Tactics/Nsatz.v | 4 |
1 files changed, 2 insertions, 2 deletions
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). |