aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/Hints.v
Commit message (Expand)AuthorAge
* hints: add Hint Variables/Constants Opaque/Transparent commandsGravatar Matthieu Sozeau2018-07-02
* Do not allow spliting in res_pf, this is reserved for pretypingGravatar Matthieu Sozeau2018-06-15
* Fix core hint database issue #6521Gravatar Anton Trunov2018-01-03
* Remove non-terminating Timeout tests from Hints.v.Gravatar Maxime Dénès2017-07-20
* Test new syntax for hints and typeclass optionsGravatar Matthieu Sozeau2016-11-03
* Lets Hints/Instances take an optional patternGravatar Matthieu Sozeau2016-11-03
* Revise syntax of Hint CutGravatar Matthieu Sozeau2016-06-16
* Hint Cut documentation and cleanup of printing (was duplicated andGravatar Matthieu Sozeau2015-11-04
* ZArith + other : favor the use of modern names instead of compat notationsGravatar letouzey2012-07-05
* Repair two testsGravatar letouzey2012-04-12
* Try to fix the behavior of clenv_missing used when declaring hintsGravatar letouzey2011-02-22
* Some fixes of the test-suite scriptsGravatar letouzey2011-02-21
* Mainly made that evarconv is able to solve "?n = (fun x => x) ?n" (sic).Gravatar herbelin2010-06-11
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* - Addition of "Hint Resolve ->" and "Hint Resolve <-" continued: itGravatar herbelin2009-05-10
* Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8Gravatar herbelin2005-12-21
* Fusion entre la nouvelle et l'ancienne syntaxe de HintDestructGravatar herbelin2002-06-05
* Syntaxe des HintsGravatar herbelin2001-09-13
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-17 02:58:14 +0000