| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-03-15 | Merge PR#267: Proposal for an update of the recommended style in programming ↵ | Maxime Dénès | |
| Coq. | |||
| 2017-03-14 | Merge PR#432: [cleanup] Change Id.t option to Name.t in TacFun | Maxime Dénès | |
| 2017-03-13 | [travis] Basic support for overlays. | Emilio Jesus Gallego Arias | |
| We now allow the user to overlay contribution repositories and branches by adding their own rules to `ci-basic-overlay.sh`. This just provides very basic support. | |||
| 2017-03-13 | Merge PR#456: Proposing improvement to the CI targets for local use | Maxime Dénès | |
| 2017-03-12 | Updating core.dbg after ltac moved to plugins directory. | Hugo Herbelin | |
| 2017-03-10 | [travis] Make the git_checkout function more reliable. | Théo Zimmermann | |
| This commit also documents the behavior of said function; and fix the location of the ssreflect clone to an absolute path (this is now necessary). | |||
| 2017-03-10 | [travis] Adding a template file and using it for all targets. | Théo Zimmermann | |
| 2017-03-10 | [travis] Change headband for wider compatibility. | Théo Zimmermann | |
| 2017-03-10 | Improve build of travis target on local machine. | Théo Zimmermann | |
| - Move the git clones to a specific subfolder to avoid pollution. - Do not fail when git clone already exist (but make sure it is up-to-date). | |||
| 2017-03-10 | [travis] Move GeoCoq to allow fail. | Emilio Jesus Gallego Arias | |
| We need to agree a bit more with upstream. | |||
| 2017-03-09 | [travis] Move GeoCoq to allow fail. | Emilio Jesus Gallego Arias | |
| We need to agree a bit more with upstream. | |||
| 2017-03-02 | [travis] Backport trunk's travis support. | Emilio Jesus Gallego Arias | |
| 2017-02-24 | [travis] [External CI] fiat-parsers | Emilio Jesus Gallego Arias | |
| 2017-02-23 | Fixing #use"include" after vernac is added and ltac is moved to a plugin. | Hugo Herbelin | |
| 2017-02-21 | [travis] track an 8.7 specific branch of HoTT. | Maxime Dénès | |
| This is required since we merged PR#309: Ltac as a plugin. | |||
| 2017-02-21 | Merge PR#309: Ltac as a plugin | Maxime Dénès | |
| 2017-02-19 | Fixing debugger after the split of toplevel into vernac. | Pierre-Marie Pédrot | |
| 2017-02-17 | remove obsolete file dev/Makefile.oug | Pierre Letouzey | |
| 2017-02-17 | Documenting the pluginification of Ltac. | Pierre-Marie Pédrot | |
| 2017-02-17 | Ltac as a plugin. | Pierre-Marie Pédrot | |
| This commit is essentially moving files around. In particular, the corresponding plugin still relies on a mllib file rather than a mlpack one. Otherwise, this causes link-time issues for third-party plugins depending on modules defined in the Ltac plugin. | |||
| 2017-02-16 | [cleanup] Change Id.t option to Name.t in TacFun | Tej Chajed | |
| 2017-02-15 | [travis] [External CI] CompCert official 8.6 support + UniMath | Emilio Jesus Gallego Arias | |
| 2017-02-15 | [travis] [External CI] Factor out math-comp installs. | Emilio Jesus Gallego Arias | |
| We make math-comp overlays easier, we also start structuring the scripts a bit more. | |||
| 2017-02-14 | Merge branch 'master'. | Pierre-Marie Pédrot | |
| 2017-02-14 | Moving printing code from Evd to Termops. | Pierre-Marie Pédrot | |
| 2017-02-14 | Ltac now uses evar-based constrs. | Pierre-Marie Pédrot | |
| 2017-02-14 | Tactic_matching API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-07 | Merge PR#425: [travis] [External CI] [geocoq] don't build slow file | Maxime Dénès | |
| 2017-02-07 | [travis] [External CI] [geocoq] don't build slow file | Emilio Jesus Gallego Arias | |
| Unfortunately `Ch16_coordinates_with_functions.v` takes alone ~15 minutes which is too much for Travis. Pity, because it was a nice use case. | |||
| 2017-02-07 | [travis] [External CI] iris-coq: fix dependencies | Emilio Jesus Gallego Arias | |
| 2017-02-07 | [travis] [External CI] GeoCoq | Emilio Jesus Gallego Arias | |
| 2017-02-07 | [travis] Move ci files from `tools` to `dev`. | Maxime Dénès | |
| 2017-01-26 | Adding a printer for Proof.proof reflecting the focusing layout. | Hugo Herbelin | |
| This is a modest contribution serving before all the purpose of displaying the focus stack and the shelf and give_up list. It does not print the sigma (while it could). Any improvements are welcome. | |||
| 2017-01-19 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2016-12-08 | Windows build scripts for 8.6 final. | Maxime Dénès | |
| 2016-12-08 | Fix paths in 32-bit windows build scripts. | Maxime Dénès | |
| 2016-12-07 | Add bat files for 8.6rc1 build. | Maxime Dénès | |
| 2016-12-07 | Add bat files for 8.6beta1 build. | Maxime Dénès | |
| 2016-12-07 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2016-12-02 | Merge remote-tracking branch 'github/pr/372' into v8.6 | Maxime Dénès | |
| Was PR#372: Update dev/doc/changes.txt with HintsResolveEntry changes | |||
| 2016-12-02 | Merge remote-tracking branch 'github/pr/368' into v8.6 | Maxime Dénès | |
| Was PR#368: Add example in dev/doc/changes involving Tacmach.project | |||
| 2016-12-02 | Merge remote-tracking branch 'github/pr/369' into v8.6 | Maxime Dénès | |
| Was PR#369: Make a note about wit_constr and Constrarg in dev/doc/changes | |||
| 2016-12-02 | Merge remote-tracking branch 'github/pr/371' into v8.6 | Maxime Dénès | |
| Was PR#371: Update dev/doc/changes with things about mem_named_context | |||
| 2016-11-30 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2016-11-24 | Fix some documentation typos. | Guillaume Melquiond | |
| Note: "dependant" does exist, but it is a noun and it means a person that is somehow financially dependent on someone else. | |||
| 2016-11-21 | (v8.6) Update dev/doc/changes.txt with HintsResolveEntry changes | Jason Gross | |
| 2016-11-21 | (v8.6) Update dev/doc/changes with things about mem_named_context | Jason Gross | |
| 2016-11-21 | (v8.6) Make a note about wit_constr and Constrarg in dev/doc/changes | Jason Gross | |
| 2016-11-21 | (v8.6) Add example in dev/doc/changes involving Tacmach.project | Jason Gross | |
| 2016-11-18 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |