| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Ensuring all .v files end with a newline to make "sed -i" work better on them. |  Hugo Herbelin | 2017-08-21 |
| | | |||
| * | test-suite: more use of the new command Extraction TestCompile |  Pierre Letouzey | 2017-07-27 |
| | | |||
| * | Prelude : no more autoload of plugins extraction and recdef | Pierre Letouzey | 2017-06-14 |
| | | | | | | | | | | | | | | | | | | The user now has to manually load them, respectively via: Require Extraction Require Import FunInd The "Import" in the case of FunInd is to ensure that the tactics functional induction and functional inversion are indeed in scope. Note that the Recdef.v file is still there as well (it contains complements used when doing Function with measures), and it also triggers a load of FunInd.v. This change is correctly documented in the refman, and the test-suite has been adapted. | ||
| * | Get rid of "shouldsucceed" subdirectory by moving tests to parent directory. |  xclerc | 2013-09-20 |
| git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16797 85f007b7-540e-0410-9357-904b9bb8a0f7 | |||
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |