| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-06-14 | Merge PR#498: Bignums as a separate opam package | Maxime Dénès | |
| 2017-06-13 | Makefile.build: do *not* build PLUGINSCMO by default (followup of PR #709) | Pierre Letouzey | |
| 2017-06-13 | Merge PR#385: Equality of sigma types | Maxime Dénès | |
| 2017-06-13 | Merge PR#766: Fix ocamldebug for the API | Maxime Dénès | |
| 2017-06-13 | Merge PR#714: Print feature Proof-of-Concept (episode 2) | Maxime Dénès | |
| 2017-06-13 | [travis] overlay for corn | Pierre Letouzey | |
| 2017-06-13 | [travis] extra test ci-bignums (+factorize other scripts) | Pierre Letouzey | |
| 2017-06-13 | [travis] overlay + extra deps for math-classes (and formal-topology) | Pierre Letouzey | |
| 2017-06-13 | Merge PR#757: Better sectioning on travis log printing in test-suite | Maxime Dénès | |
| 2017-06-13 | [travis] adapt CoLoR compilation to depend on the bignum package | Pierre Letouzey | |
| 2017-06-13 | BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo) | Pierre Letouzey | |
| See now https://github.com/coq/bignums Int31 is still in the stdlib. Some proofs there has be adapted to avoid the need for BigNumPrelude. | |||
| 2017-06-13 | Merge PR#743: Update .gitignore | Maxime Dénès | |
| 2017-06-13 | Merge PR#764: Point ci-hott at a newer version of HoTT | Maxime Dénès | |
| 2017-06-13 | Merge PR#772: Store plugins/micromega/micromega.{ml,mli} files in the ↵ | Maxime Dénès | |
| repository. Try to generate them later. | |||
| 2017-06-12 | Store plugins/micromega/micromega.{ml,mli} files in the repository. Try to ↵ | Matej Košík | |
| generate them later. | |||
| 2017-06-12 | Merge PR#715: Add coq-dpdgraph ci | Maxime Dénès | |
| 2017-06-12 | Merge PR#709: Bytecode compilation apart from 'make world', again | Maxime Dénès | |
| 2017-06-12 | Merge PR#718: API cleanup: aliases | Maxime Dénès | |
| 2017-06-12 | Temporary overlay, waiting for upstream PR merges. | Maxime Dénès | |
| 2017-06-12 | Merge PR#707: add support for "-bypass-API" argument to "coq_makefile" | Maxime Dénès | |
| 2017-06-12 | add overlays | Matej Košík | |
| 2017-06-12 | Add support for "-bypass-API" argument of "coq_makefile" | Matej Košík | |
| Plugin-writers can now use: -bypass-API parameter with "coq_makefile". The effect of that is that instead of -I API the plugin will be compiled with: -I config" -I dev -I lib -I kernel -I library -I engine -I pretyping -I interp -I parsing -I proofs -I tactics -I toplevel -I printing -I intf -I grammar -I ide -I stm -I vernac | |||
| 2017-06-12 | make test-suite/save-logs.sh usable also on old MacOS X | Maxime Denes | |
| 2017-06-12 | Fix ocamldebug for the API | Gaëtan Gilbert | |
| 2017-06-11 | Point ci-hott at a newer version of HoTT | Jason Gross | |
| 2017-06-10 | Remove remaining vo.itarget files (obsolete since PR #499) | Pierre Letouzey | |
| 2017-06-10 | Fix Travis sectioning | Jason Gross | |
| It drops anything after a `/`, so we change all `/`s into `.`. There must be a better way to do this that doesn't involve so much bash hackery, right? | |||
| 2017-06-10 | Remove (useless) aliases from the API. | Matej Košík | |
| 2017-06-09 | Better sectioning on travis log printing in test-suite | Jason Gross | |
| 2017-06-09 | Makefile.common: remove an obsolete comment after PR#499 | Pierre Letouzey | |
| 2017-06-08 | Mirror dpdgraph's travis test more accurately | Jason Gross | |
| 2017-06-08 | Remove coq-dpdgraph overlay | Jason Gross | |
| 2017-06-08 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2017-06-08 | Remove overlay. | Maxime Dénès | |
| 2017-06-08 | Merge PR#652: Put all plugins behind an "API". | Maxime Dénès | |
| 2017-06-07 | Update .gitignore | Jason Gross | |
| 2017-06-07 | add overlays | Matej Košík | |
| 2017-06-07 | Put "ssreflect" behind "API". | Matej Košík | |
| 2017-06-07 | Put all plugins behind an "API". | Matej Kosik | |
| 2017-06-07 | Merge PR#698: Trunk misc | Maxime Dénès | |
| 2017-06-07 | Merge PR#717: [proof] Deprecate "proof mode" API | Maxime Dénès | |
| 2017-06-07 | Merge PR#669: Ssr merge | Maxime Dénès | |
| 2017-06-06 | Overlay. | Maxime Dénès | |
| 2017-06-06 | Merge the ssr plugin. | Maxime Dénès | |
| 2017-06-06 | Remove some overlays. | Maxime Dénès | |
| 2017-06-06 | Merge PR#623: Remove the Sigma (monotonous state) API. | Maxime Dénès | |
| 2017-06-06 | Overlays. | Maxime Dénès | |
| 2017-06-06 | Remove the Sigma (monotonous state) API. | Maxime Dénès | |
| Reminder of (some of) the reasons for removal: - Despite the claim in sigma.mli, it does *not* prevent evar leaks, something like: fun env evd -> let (evd',ev) = new_evar env evd in (evd,ev) will typecheck even with Sigma-like type annotations (with a proof of reflexivity) - The API stayed embryonic. Even typing functions were not ported to Sigma. - Some unsafe combinators (Unsafe.tclEVARS) were replaced with slightly less unsafe ones (e.g. s_enter), but those ones were not marked unsafe at all (despite still being so). - There was no good story for higher order functions manipulating evar maps. Without higher order, one can most of the time get away with reusing the same name for the updated evar map. - Most of the code doing complex things with evar maps was using unsafe casts to sigma. This code should be fixed, but this is an orthogonal issue. Of course, this was showing a nice and elegant use of GADTs, but the cost/benefit ratio in practice did not seem good. | |||
| 2017-06-06 | Merge PR#662: Fixing bug #5233 and another bug with implicit arguments + a ↵ | Maxime Dénès | |
| short econstr-cleaning of record.ml | |||
| 2017-06-06 | Merge PR#728: A few typos. | Maxime Dénès | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |