| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-06-14 | Remove support for Coq 8.3. | Guillaume Melquiond | |
| 2017-06-14 | Remove support for Coq 8.2. | Guillaume Melquiond | |
| 2017-06-14 | Add a version to be used when parsing compatibility notations mentioning old ↵ | Guillaume Melquiond | |
| versions. | |||
| 2017-06-14 | Temporary overlays for bignums. | Maxime Dénès | |
| 2017-06-14 | Merge PR#498: Bignums as a separate opam package | Maxime Dénès | |
| 2017-06-13 | Remove some useless code in Term_typing | Gaëtan Gilbert | |
| The [let _typ = ...] comes from before universe polymorphism. In those times it was [let _typ, cst = ...] which produced something of use. The asserts come from 359e4ffe3 and before (2006 and before). In those times [Typeops.infer] rebuilt the term being typed, but nowadays the assert seems of little use. | |||
| 2017-06-13 | doc: improve grammar of RefMan-syn | William Lawvere | |
| 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 | Revert "[travis] temporary UniMath overlay" | Théo Zimmermann | |
| This reverts commit 7ca4e36af8a12236a618bd3a8d045439df40dd43. Not necessary anymore since UniMath/UniMath#715 has been merged. | |||
| 2017-06-13 | Improving documentation of tactic "move" (report #4561). | Hugo Herbelin | |
| 2017-06-13 | Merge PR#714: Print feature Proof-of-Concept (episode 2) | Maxime Dénès | |
| 2017-06-13 | Dualize the unsafe flag of refine into typecheck and make it mandatory. | Pierre-Marie Pédrot | |
| 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 | Documenting the change of default flag value of Refine.refine. | Pierre-Marie Pédrot | |
| 2017-06-13 | Turn the default behaviour of the refine primitive into the safe one. | Pierre-Marie Pédrot | |
| 2017-06-13 | Explicit the unsafe flag of all calls to Refine.refine. | Pierre-Marie Pédrot | |
| 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 | Document instantiate (ident := term) and make it the preferred variant. | Théo Zimmermann | |
| 2017-06-13 | Document Show ident. | Théo Zimmermann | |
| 2017-06-13 | Document evar naming syntax. | Théo Zimmermann | |
| 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 | [travis overlay] Partially Revert 013c0232953f1f58 | Jason Gross | |
| I've pushed commits which add `-bypass-API` to bedrock in the proper way, so these overlays are no longer needed | |||
| 2017-06-12 | [proof] Move bullets to their own module. | Emilio Jesus Gallego Arias | |
| Bullets were placed inside the `Proof_global` module, I guess that due to the global registration function. However, it has logically nothing to do with the functionality of `Proof_global` and the current placement may create some interference between the developers reworking proof state handling and bullets. We thus put the bullet functionality into its own, independent file. | |||
| 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 | zify: force reduction of (Z.max 0 0) and similar (fix #5439) | Pierre Letouzey | |
| Turn some "simpl" into "compute". Also do the same for the few "simpl (Z.of_nat ...)". This way, definition like Z.max are properly reduced, and moreover zify isn't sensible anymore to the "Arguments Z.of_nat : simpl never" that some user want (see also #5039). Unfortunately, the compute we're using now still honor the "Opaque" declarations, so a "Opaque Z.max" will block things again (see also #5374). | |||
| 2017-06-12 | zify: confusion between Pos2Z.inj_sub and Pos2Z.inj_sub_max (fix #5336) | Pierre Letouzey | |
| 2017-06-12 | [lib] Remove obsolete state-management function add_frozen_state | Emilio Jesus Gallego Arias | |
| AFAICS this function predates modern state-handling; nowadays summaries are stored by the STM and nobody were using this information. | |||
| 2017-06-12 | Remove commented documentation for Show Tree. | Théo Zimmermann | |
| 2017-06-12 | Fix ocamldebug for the API | Gaëtan Gilbert | |
| 2017-06-12 | Remove Show Thesis command which was never implemented. | Théo Zimmermann | |
| 2017-06-12 | Remove non-working Show Tree and Show Node commands. | Théo Zimmermann | |
| 2017-06-12 | Remove more dead code (follow-up of previous commit). | Théo Zimmermann | |
| 2017-06-12 | Remove Show Implicit Arguments command. | Théo Zimmermann | |
| The command has been broken for 15 years. It is basically dead code. Its former behavior can be mimicked with Set Printing Implicit. Show. | |||
| 2017-06-12 | Remove Show Goal "uid" command. | Théo Zimmermann | |
| Introduced for Proof-General but unused at the current time, undocumented and can raise anomalies. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |