| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-01-08 | Document native_compute. | Maxime Dénès | |
| 2015-01-07 | Initiating who-did-what for 8.5 | Hugo Herbelin | |
| 2015-01-07 | Committing whodidwhat files. | Hugo Herbelin | |
| 2015-01-07 | Reverting the tentative try to restore the use of second-order | Hugo Herbelin | |
| typed-based matching: it provokes a stack overflow in contrib ClassicalRealisability. To be investigated later on. (See 893a02f643858ba0b0172648e77af9ccb65f03df.) | |||
| 2015-01-07 | Aligning printing of universe constraints. | Hugo Herbelin | |
| 2015-01-07 | Hook when state arrives on master. | Enrico Tassi | |
| 2015-01-06 | Fix checker's treatment of template polymorphic | Matthieu Sozeau | |
| inductive instantiation, now using substitution of levels. Fixes the test-suite file coqchk/univ. | |||
| 2015-01-06 | Safer version of the implementation of stores. | Pierre-Marie Pédrot | |
| 2015-01-06 | remove unused iArray | Enrico Tassi | |
| 2015-01-06 | rename: vi -> vio | Enrico Tassi | |
| 2015-01-06 | Fix some documentation typos. | Guillaume Melquiond | |
| 2015-01-06 | Fix setoid rewrite. | Arnaud Spiwack | |
| Because of f66b84de608830600e43f6d1a97c29226b6b58ea (Refine primitive: [unsafe] is now true by default), setoid rewrite could produce ill-typed term. Since setoid rewrite relies on the checks of refine to ensure well-typed, turned the check explicitely on with [~unsafe:false]. | |||
| 2015-01-06 | Improve error recovery in case of ill-formed coqdoc comment. (Fix for bug ↵ | Guillaume Melquiond | |
| #3802.) | |||
| 2015-01-06 | updated include file for debugging | Bruno Barras | |
| 2015-01-06 | improve efficiency of the reduction interpreter of coqtop | Bruno Barras | |
| Conflicts: kernel/closure.ml kernel/closure.mli kernel/reduction.ml | |||
| 2015-01-06 | improve efficiency of the reduction interpreter of the checker | Bruno Barras | |
| Conflicts: checker/closure.ml checker/closure.mli checker/reduction.ml | |||
| 2015-01-06 | Fixing test for bug #2830. | Pierre-Marie Pédrot | |
| 2015-01-06 | Rename ill-named "imports" field of safe_env into "required". | Maxime Dénès | |
| 2015-01-06 | Propagating the relaxing of filtering started in 48509b6, fixed in | Hugo Herbelin | |
| 3cd718c, to the case of second_order_matching. | |||
| 2015-01-06 | Fixing old filter bug in second_order_matching. | Hugo Herbelin | |
| 2015-01-05 | Added more informative messages about bullets. | Pierre Courtieu | |
| Updated doc, but not tests-suite yet. | |||
| 2015-01-05 | kernel/ind Change interface of declare_mind and declare_mutual | Matthieu Sozeau | |
| Removing unused argument and fixing bug #3899, now warning when a record cannot be made primitive in Set Primitive Projections mode because it has no projection or at least one undefinable projection. | |||
| 2015-01-05 | In Show Universes, print universes before normalization. | Matthieu Sozeau | |
| 2015-01-05 | Updating documentation about bullets. | Pierre Courtieu | |
| Error messages were outdated. | |||
| 2015-01-05 | Removing GUtil dependency from ide/document.ml. | Pierre-Marie Pédrot | |
| We reimplement a quick-n-dirty Gtk-free signal handler. | |||
| 2015-01-05 | Adding an option to deactivate the progress bar. | Pierre-Marie Pédrot | |
| 2015-01-05 | Implementing a segment-viewer in CoqIDE. | Pierre-Marie Pédrot | |
| This allows a nifty display of the current state of the document through a dedicated progress bar. Also closes bug #3764. | |||
| 2015-01-04 | STM: Make assert unneeded (Close 3898) | Enrico Tassi | |
| 2015-01-04 | Adapting two files from test-suite to now forbidden Require's in modules. | Hugo Herbelin | |
| Status of 335 and 3363 which are explicitly testing Require in modules still to be addressed (to remove from test suite?). | |||
| 2015-01-03 | Fixing 48509b61 which improved unification as expected but actually | Hugo Herbelin | |
| not using the intended test. By fixing the intended test, the need for a delta-expansion resulting from this commit in PFsection6.v (line 1255) of ssreflect disappears. | |||
| 2015-01-03 | Fixing #3896 (incorrect sigma given to printer). | Hugo Herbelin | |
| 2015-01-03 | Tentatively trying to restore the use of second-order typed-based | Hugo Herbelin | |
| unification algorithm in consider_remaining_unif_problems. If it happens to be problematic, one can backtrack to the "optimization" from 3bd9cb26b which has a restriction on rels/vars. | |||
| 2015-01-03 | Fixing #3895 (thanks to PMP for diagnosis). | Hugo Herbelin | |
| 2015-01-01 | An optimization in the use of unification candidates so as to get the | Hugo Herbelin | |
| following working: Definition test {A B:Type} {H:A=B} (a:A) : B := rew H in a. | |||
| 2014-12-30 | Document the new behavior of lazymatch. | Guillaume Melquiond | |
| 2014-12-30 | Fixing #3892: Ensure that notation variables do not capture names | Hugo Herbelin | |
| hidden behind another notation. | |||
| 2014-12-30 | Simplifying second_order_matching: no need to invert the linear | Hugo Herbelin | |
| initial segment of the context of the evar. | |||
| 2014-12-30 | Compatibility ocaml 3.12. | Hugo Herbelin | |
| 2014-12-30 | more CHANGES | Enrico Tassi | |
| 2014-12-30 | Minor fixes for the win32 installer | Enrico Tassi | |
| 2014-12-29 | Fixing bug #3632 for good. | Pierre-Marie Pédrot | |
| 2014-12-29 | Proof using: do not clear letins (unless they use a cleared var) | Enrico Tassi | |
| 2014-12-28 | Use [Proof using] to make sure that [List.in_flat_map] doesn't grab too many ↵ | Arnaud Spiwack | |
| section variable. For some reason, the subproofs solved by [auto] had started using [Hfinjective] from the section context. | |||
| 2014-12-28 | Call nf_constraints also when compiling directly to vo | Enrico Tassi | |
| After commit b46944e the system got way slower, hence the optimization is relevant also for non polymorphic constants. Putting it back now, but we shall find something in between: an optimization that does not clash with async proofs but that gives some performance improvement over no optimization at all. | |||
| 2014-12-28 | Proof using: call "clear" to remove from sight the vars not selected | Enrico Tassi | |
| As discussed on coqdev, clear is not perfect, Hints for trivial using cleared section vars are still used. But it is better than nothing I guess. | |||
| 2014-12-28 | remove debug prints (leftover) | Enrico Tassi | |
| 2014-12-27 | STM: check with the kernel proof terms on the worker too | Enrico Tassi | |
| Before this commit the worker was sending back a proof term as built by tactics. The master receives the proof terms and eventually (when one clicks on the gears in CoqIDE) check it with the kernel. This meant that errors like the ones produced by the "fix" tactics were discovered very late. Now a worker checks with its kernel the proof term before sending it back. The term is also checked by the master, eventually, but the error is signaled early. | |||
| 2014-12-27 | STM: fix processing of errors | Enrico Tassi | |
| 2014-12-27 | STM: module Pp is open | Enrico Tassi | |
| 2014-12-27 | proof_global: make it possible to call close_proof in a worker | Enrico Tassi | |
| Given that the proof state contains a callback (a terminator) that is not sent (dropped by the ephemeron mechanism at marshall time) de-referencing the ephemeron during this function makes it impossible to call it in a worker. Now the worker can call the function and replace the terminator with a good one. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |