aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Add an option to configure the modifier for Queries.Gravatar Cyprien Mangin2016-06-02
* Merge the user queries tab with the shortcut tab.Gravatar Cyprien Mangin2016-06-02
* Slightly better interface to edit queries.Gravatar Cyprien Mangin2016-06-02
* Add user-created queries to CoqIDE.Gravatar Cyprien Mangin2016-06-02
* Add a [Show Proof.] query to CoqIDE.Gravatar Cyprien Mangin2016-06-02
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-01
|\
* | Makefile.build : follow-up of previous commitGravatar Pierre Letouzey2016-06-01
* | Makefile.build : improved rules about .cm(x)aGravatar Pierre Letouzey2016-06-01
* | Makefile.build : update the otags ruleGravatar Pierre Letouzey2016-06-01
* | g_tactics : remove opt_bindings (2-line dead code)Gravatar Pierre Letouzey2016-06-01
* | Makefile.common : avoid warnings about files linked twiceGravatar Pierre Letouzey2016-06-01
* | Merge branch 'yet-another-makefile-bigbang' into trunkGravatar Pierre Letouzey2016-06-01
|\ \
| * | Yet another Makefile reform : a unique phase without nasty make tricksGravatar Pierre Letouzey2016-06-01
| * | Makefile: restore the use of coqdep_boot for creating .v.d filesGravatar Pierre Letouzey2016-06-01
| | * Fix potential race condition in vm_compute.Gravatar Guillaume Melquiond2016-05-31
* | | This patch splits pretty printing representation from IO operations.Gravatar Pierre-Marie Pédrot2016-05-31
|\ \ \ | |/ / |/| |
| | * Revert "Rename Lexer -> CLexer."Gravatar Pierre-Marie Pédrot2016-05-31
* | | Making the grammar/ folder independent from the other ones.Gravatar Pierre-Marie Pédrot2016-05-31
| * | Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
|/ /
* | Checker: avoid using obsolete names from NamesGravatar Pierre Letouzey2016-05-31
* | Checker: no more -I kernel via a few symlinks (for Names and Esubst)Gravatar Pierre Letouzey2016-05-31
| * Extraction : add a location in the error message about polypropGravatar Pierre Letouzey2016-05-30
* | Extraction : add a location in the error message about polypropGravatar Pierre Letouzey2016-05-30
| * Fix bug #4746: Anomaly: Evar ?X10 was not declared.Gravatar Pierre-Marie Pédrot2016-05-29
| * STM: fix argument filtering for slavesGravatar Enrico Tassi2016-05-27
| * Pfedit.get_current_context refinement (fix #4523)Gravatar Matthieu Sozeau2016-05-26
| * rewrite/Univs: Fix bug # 4498.Gravatar Matthieu Sozeau2016-05-26
* | Update required OCaml version in configure.Gravatar Maxime Dénès2016-05-26
| * Extraction/Projections: Fix bug #4710Gravatar Matthieu Sozeau2016-05-23
| * Hints/Univs: fix bug #4628 anomaliesGravatar Matthieu Sozeau2016-05-23
* | typosGravatar Enrico Tassi2016-05-23
| * Disable memoization rather than failing when files cannot be opened.Gravatar Guillaume Melquiond2016-05-20
* | Extraction: code cleanup in CommonGravatar Pierre Letouzey2016-05-20
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-20
|\|
| * native_compute: don't call Unicode.ascii_of_ident twice (not idempotent anymore)Gravatar Pierre Letouzey2016-05-19
| * Extraction: don't call Unicode.ascii_of_ident twice (not idempotent anymore)Gravatar Pierre Letouzey2016-05-19
* | native_compute: don't call Unicode.ascii_of_ident twice (not idempotent anymore)Gravatar Pierre Letouzey2016-05-19
* | Extraction: don't call Unicode.ascii_of_ident twice (not idempotent anymore)Gravatar Pierre Letouzey2016-05-19
| * adding "user-contrib" directory to ".gitignore"Gravatar Matej Kosik2016-05-19
| * Unicode.ascii_of_ident is now truly injectiveGravatar Pierre Letouzey2016-05-19
* | Unicode.ascii_of_ident is now truly injectiveGravatar Pierre Letouzey2016-05-19
* | Micromega: qualify Coq.micromega.Tauto (avoid coqdep warnings about new Init/...Gravatar Pierre Letouzey2016-05-19
* | Putting all the tactics exported by the Tactics module in the new monad API.Gravatar Pierre-Marie Pédrot2016-05-17
|\ \
| * | Removing some compatibility layers in Tactics.Gravatar Pierre-Marie Pédrot2016-05-17
| * | Removing the old refine tactic from the Tactics module.Gravatar Pierre-Marie Pédrot2016-05-17
| * | Put the "move" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-17
| * | Put the "change" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
| * | Put the "specialize_eq" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
| * | Put the "generalize dependent" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
| * | Put the "generalize" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16