| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | [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 | 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 | |
| 2017-05-23 | Merge PR#518: Faster universe unification | Maxime Dénès | |
| 2017-05-23 | [vernac] Remove `Save thm id.` command. | Emilio Jesus Gallego Arias | |
| We'd like to cleanup the `proof_end` type so we can have a smaller path in proof save. Note that the construction: ``` Goal Type. ⋮ Save id. ``` has to be handled by the STM in the same path as Defined (but with an opaque flag), as `Save id` will alter the environment and cannot be processed in parallel. We thus try to simply such paths a bit, as complexity of `lemmas.ml` seems like an issue these days. The form `Save Theorem id` doesn't really seem used, and moreover we should really add a type of "Goal", and unify syntax. It is often the case that beginners try `Goal addnC n : n + 0 = n." etc... | |||
| 2017-05-23 | [vernac] Remove `Save.` command. | Emilio Jesus Gallego Arias | |
| It has been deprecated for a while in favor of `Qed`. | |||
| 2017-05-22 | Compatibility fix while waiting for integration of Pierre Courtieu's PR #449. | Hugo Herbelin | |
| 2017-05-22 | Using type classes in the interpretation of "specialize" and "contradiction". | Hugo Herbelin | |
| We do that by using constr_with_bindings rather than open_constr_with_bindings (+ extra call to typeclasses in "specialize"). If my understanding is right, the only effect would be to succeed more in cases where it was failing (in inh_conv_coerce_to_gen). In particular, "specialize" and "contradiction" already have a WITHHOLES test for rejecting pending holes. Incidentally, this answers enhancement #5153. | |||
| 2017-05-22 | Clarifying the interpretation path for the "constr_with_binding" argument. | Hugo Herbelin | |
| This fixes an inconsistency introduced in 554a6c806 (svn r12603) where both interp_constr_with_bindings and interp_open_constr_with_bindings were going through interp_open_constr (no type classes so as to not to commit too early on irreversible choices, accepting unresolved holes). We fix this by having interp_constr_with_bindings going to interp_constr (using type classes and failing on unresolved evars). The external impact is that any TACTIC EXTEND which refers to constr_with_binding has now to decide whether it intends it to use what the name suggest (using type classes and to fail if evars remain unresolved), thus keeping constr_with_binding, or the actual behavior which requires to use open_constr_with_bindings for strict compatibility. | |||
| 2017-05-20 | Added a test for #4765 (an example of printing abbreviation with binders). | Hugo Herbelin | |
| 2017-05-20 | Deprecate -nodoc. | Théo Zimmermann | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |