aboutsummaryrefslogtreecommitdiff
path: root/src/Tactics
Commit message (Collapse)AuthorAge
* nsatz_contradict can now handle invalid _ <> _ hypothesesGravatar Jason Gross2016-06-23
|
* Make [nsatz_contradict] better at inequalitiesGravatar Jason Gross2016-06-23
|
* Work around bug #4851 in nsatzGravatar Jason Gross2016-06-23
| | | | | Now our [nsatz] does not barf when you have duplicate equations in the context.
* parenthesize Ltac [constr:] argumentsGravatar Andres Erbsen2016-06-20
|
* Fix nsatz_compute for 8.4Gravatar Jason Gross2016-06-20
|
* More 8.5 fixesGravatar Jason Gross2016-06-20
| | | | Changing scopes?
* move nsatz into tactics directoryGravatar Andres Erbsen2016-06-20
|
* import VerdiTacticsGravatar Andres Erbsen2015-09-17