| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-05-28 | Gitlab CI | Gaëtan Gilbert | |
| 2017-05-27 | Merge PR#686: [travis] temporary UniMath overlay | Maxime Dénès | |
| 2017-05-27 | [travis] temporary UniMath overlay | Maxime Dénès | |
| We are waiting for an upstream merge of a fix related to coq_makefile2. | |||
| 2017-05-26 | Merge PR#666: romega revisited : no more normalization trace, cleaned-up ↵ | Maxime Dénès | |
| resolution trace | |||
| 2017-05-26 | Merge PR#655: Extra functions exported in EConstr | Maxime Dénès | |
| 2017-05-25 | Merge PR#645: [stm] Tweak debug options. | Maxime Dénès | |
| 2017-05-25 | Merge PR#637: Short cleaning of the interpretation path for constr_with_bindings | Maxime Dénès | |
| 2017-05-25 | Merge PR#608: Allow Ltac2 as a plugin | Maxime Dénès | |
| 2017-05-25 | Merge PR#481: [option] Remove support for non-synchronous options. | Maxime Dénès | |
| 2017-05-25 | Merge PR#406: coq makefile2 | Maxime Dénès | |
| 2017-05-25 | Merge PR#402: Uniform attribute handling in interfaces | Maxime Dénès | |
| 2017-05-25 | [location] [travis] Add overlays for located_switch | Emilio Jesus Gallego Arias | |
| 2017-05-24 | [location] Fix warnings. | Emilio Jesus Gallego Arias | |
| 2017-05-24 | [location] Renaming "CAst.ast" to "CAst.t" | Matej Košík | |
| 2017-05-24 | Merge branch 'trunk' into located_switch | Emilio Jesus Gallego Arias | |
| 2017-05-24 | ROmega: division-aware ReflOmegaCore, allowing trace without terms | Pierre Letouzey | |
| The trace only mentions the constant k by which we want to divide the equation, not anymore the equation we obtain after the division. Shorter trace, and it won't take much more time to perform the few Z.div than checking as currently the equality of the initial equation and the final equation multiplied by k. | |||
| 2017-05-24 | [option] Remove support for non-synchronous options. | Emilio Jesus Gallego Arias | |
| Inspired by https://coq.inria.fr/bugs/show_bug.cgi?id=5229 , which this PR solves, I propose to remove support for non-synchronous options. It seems the few uses of `optsync = false` we legacy and shouldn't have any impact. Moreover, non synchronous options may create particularly tricky situations as for instance, they won't be propagated to workers. | |||
| 2017-05-24 | coq_makefile: use -include rather than include | Enrico Tassi | |
| This fixes bedrock and eliminates warnings. Thanks Jason Gross for debugging this! | |||
| 2017-05-24 | Merge PR#642: Small cleanup on `close_proof` type. | Maxime Dénès | |
| 2017-05-24 | Merge PR#650: Fixing an extra bug with pattern_of_constr | Maxime Dénès | |
| 2017-05-24 | Merge PR#671: unification.mli: Fix a spelling typo in a comment | Maxime Dénès | |
| 2017-05-23 | unification.mli: Fix a spelling typo in a comment | Jason Gross | |
| 2017-05-23 | add the only target | Enrico Tassi | |
| This makes the following work correctly: make only TGTS="foo bar" -j2 note that make foo bar -j2 is not doing what you think | |||
| 2017-05-23 | travis: coq_makefile needs the tipa package | Enrico Tassi | |
| 2017-05-23 | overlay for UniMath | Enrico Tassi | |
| 2017-05-23 | coq_makefile: avoid spurious ./ in generated .conf file | Enrico Tassi | |
| 2017-05-23 | Restore 8.5, 8.6 compatibility of STDTIME, TIMECMD | Jason Gross | |
| 2017-05-23 | coq_makefile: don't quote extra arguments (-arg) | Enrico Tassi | |
| Restores compatibility with 8.6 | |||
| 2017-05-23 | Make install a single colon target for retro compatibility | Enrico Tassi | |
| 2017-05-23 | enters coq_makefile2 | Enrico Tassi | |
| 2017-05-23 | test suite for coq_makefile2 | Enrico Tassi | |
| 2017-05-23 | coqdep: remove optimization making makefiles harder to write | Enrico Tassi | |
| 2017-05-23 | ocamlfind: coqtop -config prints ocamlfind as found by ./configure | Enrico Tassi | |
| Used to guess again the ocamlfind location at Coq's execution time. An option to override the value (inferred at ./configure time) is available. So, what is the point of guessing it? Either it stays there, or the user is doing a hack, and has a flag to do it. | |||
| 2017-05-23 | coqdep: set FOR_PACK variable for files that need to be packed | Enrico Tassi | |
| This enables one to have just one rule to compile .ml -> .cmx. By using $(FOR_PACK) in such rule one passes to ocamlopt -for-pack ModName only when necessary. Before this coq_makefile had to generate 2 different rules, depending if the module was mentioned in an .mlpack. | |||
| 2017-05-23 | print_config: print COQ_SRC_SUBDIRS | Enrico Tassi | |
| This way a makefile can just iterate on this list, intead of having a bunch of -I hardcoded in there by coq_makefile | |||
| 2017-05-23 | Document --print-version in Usage | Enrico Tassi | |
| 2017-05-23 | Put the list of Coq sources subdirectories in one place | Enrico Tassi | |
| and avoid duplication | |||
| 2017-05-23 | Usage.print_config moved to Envars | Enrico Tassi | |
| 2017-05-23 | CoqProject_file: document in API deprecated features | Enrico Tassi | |
| 2017-05-23 | CoqProject_file: API and code cleanup (tuples -> records) | Enrico Tassi | |
| 2017-05-23 | ide/project_file.ml4 -> lib/coqProject_file.ml4 + .mli | Enrico Tassi | |
| The .mli only acknowledges the current API. I'm not guilty your honor! | |||
| 2017-05-23 | ide/project_fie.ml4: include standard banner with copyright | Enrico Tassi | |
| 2017-05-23 | test suite for coq_makefile | Enrico Tassi | |
| 2017-05-23 | configure: -local set coqdoc destination dir to ./doc rather than "" | Enrico Tassi | |
| 2017-05-23 | Bigint.euclid: clarify which sign convention is used | Pierre Letouzey | |
| 2017-05-23 | Merge PR#661: Added a test for #4765 (an example of printing abbreviation ↵ | Maxime Dénès | |
| with binders) | |||
| 2017-05-23 | Merge PR#659: Mention ./configure in INSTALL.doc | Maxime Dénès | |
| 2017-05-23 | Merge PR#657: [test-suite] Add tests for goal printing. | Maxime Dénès | |
| 2017-05-23 | Merge PR#646: Revised behavior on ill-formed identifiers | Maxime Dénès | |
| 2017-05-23 | Merge PR#660: Change wrong bullet message. | Maxime Dénès | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |