| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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. | |||
| 2017-06-11 | Point ci-hott at a newer version of HoTT | Jason Gross | |
| 2017-06-11 | [proof] Deprecate redundant wrappers. | Emilio Jesus Gallego Arias | |
| As we would like to reduce the role of proof_global in future versions, we start to deprecate old compatibility aliases in `Pfedit` in favor of the real functions underlying the 8.5 proof engine. We also deprecate a couple of alias types and explicitly mark the few remaining uses of `Pfedit`. | |||
| 2017-06-11 | A stronger test that #use"include";; works well. | Hugo Herbelin | |
| 2017-06-11 | Fixing base_include after loc is an option (30d3515). | Hugo Herbelin | |
| 2017-06-11 | Normalize deprecation notices of ./configure | Théo Zimmermann | |
| Always output a warning on stderr when a deprecated option is used. | |||
| 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 | don't leak unqualified identifiers from the macro | Matej Košík | |
| 2017-06-10 | Remove (useless) aliases from the API. | Matej Košík | |
| 2017-06-10 | [toplevel] Print error header on fatal batch error. | Emilio Jesus Gallego Arias | |
| 2017-06-09 | Better sectioning on travis log printing in test-suite | Jason Gross | |
| 2017-06-09 | Fix Bug #5568, no dup notation warnings on repeated module imports | Paul Steckler | |
| 2017-06-09 | A fix to #5414 (ident bound by ltac names now known for "match"). | Hugo Herbelin | |
| Also taking into account a name in the return clause and in the indices. Note the double meaning ``bound as a term to match'' and ``binding in the "as" clause'' when the term to match is a variable for all of "match", "if" and "let". | |||
| 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 | Fix bug 5026 (the stdlib shouldn't define inconsistent notations). | Théo Zimmermann | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |