aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
...
| | | | | | * | | Extraction: fix complexity issue #5310Gravatar Pierre Letouzey2017-02-07
* | | | | | | | | Merge PR#425: [travis] [External CI] [geocoq] don't build slow fileGravatar Maxime Dénès2017-02-07
|\ \ \ \ \ \ \ \ \
| | | | | | | | * | Add test-suite files for hintdb variables in Ltac.Gravatar Théo Zimmermann2017-02-07
| | | | | | | | * | Remove hackish autounfoldify now that hintdb can be bound to Ltac variables.Gravatar Théo Zimmermann2017-02-07
| | | | | | | | * | pre_ident can be bound to Ltac variables.Gravatar Théo Zimmermann2017-02-07
| |_|_|_|_|_|_|/ / |/| | | | | | | |
| * | | | | | | | [travis] [External CI] [geocoq] don't build slow fileGravatar Emilio Jesus Gallego Arias2017-02-07
* | | | | | | | | Merge PR#424: [travis] [External CI] iris-coq: fix dependenciesGravatar Maxime Dénès2017-02-07
|\ \ \ \ \ \ \ \ \
| * | | | | | | | | [travis] [External CI] iris-coq: fix dependenciesGravatar Emilio Jesus Gallego Arias2017-02-07
|/ / / / / / / / /
| | | * / / / / / Type cleanup in `Metasyntax`Gravatar Emilio Jesus Gallego Arias2017-02-07
| |_|/ / / / / / |/| | | | | | |
* | | | | | | | Merge PR#421: [travis] Perform parallel testingGravatar Maxime Dénès2017-02-07
|\| | | | | | |
| * | | | | | | [travis] [External CI] GeoCoqGravatar Emilio Jesus Gallego Arias2017-02-07
| * | | | | | | [travis] Enable 32bit test-suite + validate.Gravatar Emilio Jesus Gallego Arias2017-02-07
| * | | | | | | [travis] Move ci files from `tools` to `dev`.Gravatar Maxime Dénès2017-02-07
| * | | | | | | [travis] [External CI] C-Corn color coquelicot cpdt fiat-crypto floqc iris-co...Gravatar Emilio Jesus Gallego Arias2017-02-07
| * | | | | | | [travis] [External CI] Script renaming.Gravatar Emilio Jesus Gallego Arias2017-02-07
| * | | | | | | [travis] Improvements to main scriptGravatar Emilio Jesus Gallego Arias2017-02-07
| * | | | | | | [travis] [External CI] compcert HoTT math-compGravatar Emilio Jesus Gallego Arias2017-02-07
| * | | | | | | [travis] Run tests using a parallel matrix.Gravatar Emilio Jesus Gallego Arias2017-02-06
|/ / / / / / /
* | | | | | | Merge PR#419: [travis] CoqIde + doc + last available LSTGravatar Maxime Dénès2017-02-06
|\ \ \ \ \ \ \
| | | | | * | | fix Emacs compiler warning on '(lambda...)Gravatar Hendrik Tews2017-02-06
| * | | | | | | [travis] : more apt deps + parallel jobs + non-container basedGravatar Pierre-Yves Strub2017-02-04
| * | | | | | | [travis] CoqIde + doc + last available LSTGravatar Pierre-Yves Strub2017-02-04
|/ / / / / / /
* | | | | | | Merge PR#418: Travis CI configurationGravatar Maxime Dénès2017-02-03
|\ \ \ \ \ \ \
| * | | | | | | Travis CI configuration. Runs validate & test-suite.Gravatar Pierre-Yves Strub2017-02-03
|/ / / / / / /
| | | | * | | Fixing an anomaly with 'pat after cofix.Gravatar Hugo Herbelin2017-02-02
* | | | | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-02-01
|\ \ \ \ \ \ \ | | |_|_|/ / / | |/| | | | |
| * | | | | | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2017-02-01
| |\ \ \ \ \ \ | | | |_|_|/ / | | |/| | | |
| | * | | | | Fixing #5311 (anomaly on unexpected intro pattern).Gravatar Hugo Herbelin2017-01-31
| | * | | | | Merge PR#408: [native comp] Improve error message on linking error.Gravatar Maxime Dénès2017-01-30
| | |\ \ \ \ \
| * | | | | | | Fix a typo in STM universe communications.Gravatar Maxime Dénès2017-01-30
* | | | | | | | Merge PR#355: Remove unused feedback_content: GoalsGravatar Maxime Dénès2017-01-30
|\ \ \ \ \ \ \ \
| | * | | | | | | Fix bug #5262: Error should tell me which name is duplicated.Gravatar Pierre-Marie Pédrot2017-01-28
| | | | | * | | | Remove useless commentsGravatar Gaetan Gilbert2017-01-28
| | * | | | | | | Fix documentation typos.Gravatar Guillaume Melquiond2017-01-27
* | | | | | | | | Adding a printer for Proof.proof reflecting the focusing layout.Gravatar Hugo Herbelin2017-01-26
| | | | * | | | | [native comp] Improve error message on linking error.Gravatar Emilio Jesus Gallego Arias2017-01-26
| | | |/ / / / /
| | * | | | | | Fixing #5326 (anomaly on some unsupported case of 'pat).Gravatar Hugo Herbelin2017-01-26
| | * | | | | | Merge PR#383: fix #5244: set printing width ignored when given enough spaceGravatar Maxime Dénès2017-01-24
| | |\ \ \ \ \ \
| | * \ \ \ \ \ \ Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2017-01-23
| | |\ \ \ \ \ \ \ | | | | |/ / / / / | | | |/| | | | |
| | | * | | | | | Fixing unification regression #5323.Gravatar Hugo Herbelin2017-01-23
* | | | | | | | | Adding a new evar source to remember the name of evars which wereGravatar Hugo Herbelin2017-01-22
| | * | | | | | | Fixing bugs in typing "match" (regressions #5322 and #5324 + bugs with let-ins).Gravatar Hugo Herbelin2017-01-22
| | * | | | | | | Revert "Process Next Obligation proofs in parallel (fix #5314)"Gravatar Enrico Tassi2017-01-21
| | * | | | | | | Process Next Obligation proofs in parallel (fix #5314)Gravatar Enrico Tassi2017-01-20
| | * | | | | | | Do not add redundant side effects in tactic code.Gravatar Pierre-Marie Pédrot2017-01-20
* | | | | | | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-01-19
|\ \ \ \ \ \ \ \ \ | | |/ / / / / / / | |/| | | | | | |
| * | | | | | | | Mapping named_context_val preserves sharing when possible.Gravatar Pierre-Marie Pédrot2017-01-17
| * | | | | | | | STM: fix run-time classification of VernacInstance (fix #5313)Gravatar Enrico Tassi2017-01-17
| * | | | | | | | Fixing (part of) #5303 (clarifications around Record/Structure/Variant).Gravatar Hugo Herbelin2017-01-16
| * | | | | | | | Fix race condition in STM DAG generation (in debug mode).Gravatar Maxime Dénès2017-01-13
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 03:05:12 +0000