| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | Add parsers-examples target to fiat-parsers ci | Jason Gross | |
| This tests a bit more of fiat-parsers, adding an extra ~3 minutes to the build. | |||
| 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 | Postponing of universe constraints unification in term equality. | Pierre-Marie Pédrot | |
| Instead of calling the universe unification at each term node, we accumulate them and try to perform unification at the very end. This seems to be experimentally faster. | |||
| 2017-05-23 | Bigint.euclid: clarify which sign convention is used | Pierre Letouzey | |
| 2017-05-23 | Fix bindings handling of setoid_rewrite. | Cyprien Mangin | |
| This fixes the discrepancy between "rewrite H with (1 := x)" and "setoid_rewrite H with (1 := x)". | |||
| 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 | refl_omega: some code refactoring | Pierre Letouzey | |
| 2017-05-22 | refl_omega.v: explicitely identify atom indexes and omega vars | Pierre Letouzey | |
| 2017-05-22 | ReflOmegaCore: misc cleanup, <? instead of bgt, etc | Pierre Letouzey | |
| 2017-05-22 | ROmega : O_STATE turned into a O_SUM | Pierre Letouzey | |
| We benefit from the fact that we normalize now *all* hypotheses even the one defining the "stated" variable: it is produced as ...def of v... = v and normalized as -v + ...def of v... = 0 which is precisely what we should add to the initial equation during a O_STATE. | |||
| 2017-05-22 | ROmega: less contructors in the final omega trace | Pierre Letouzey | |
| Now that O_SUM is properly optimized (cf. the [fusion] function), we could use it to encode CONTRADICTION and NEGATE_CONTRADICT(_INV). This way, the trace has almost the same size, but ReflOmegaCore.v is shorter and easier to maintain. | |||
| 2017-05-22 | ROmega : merge O_CONSTANT* into a single O_BAD_CONSTANT | Pierre Letouzey | |
| 2017-05-22 | ReflOmegaCore: reverse some integer mult (coefs k1,k2 will often be simple) | Pierre Letouzey | |
| 2017-05-22 | ReflOmegaCore: comment, reorganize, permut some constructors, etc | Pierre Letouzey | |
| 2017-05-22 | romega: add a tactic named unsafe_romega (for debugging, or bold users) | Pierre Letouzey | |
| In this variant, the proof term produced by romega isn't verified at the tactic run-time (no vm_compute). In theory, [unsafe_romega] should behave exactly as [romega], but faster. Now, if there's a bug in romega, we'll be notified only at the following Qed. This could be interesting for debugging purpose : you could inspect the produced buggish term via a Show Proof. | |||
| 2017-05-22 | romega: no more normalization trace, replaced by some Coq-side computation | Pierre Letouzey | |
| This is a major change : - Generated proofs are quite shorter, since only the resolution trace remains. - No time penalty mesured (it even tends to be slightly faster this way). - Less infrastructure in ReflOmegaCore and refl_omega. - Warning: the normalization functions in ML and in Coq should be kept in sync, as well as the variable order. - Btw: get rid of ML constructor Oufo | |||
| 2017-05-22 | romega/const_omega : a few improvements (less try with, no gen equality) | Pierre Letouzey | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |