| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-01-11 | some credits for STM | Enrico Tassi | |
| 2015-01-11 | Extraction: discard code unnecessary to fulfill a module signature | Pierre Letouzey | |
| 2015-01-11 | Declarations.mli refactoring: module_type_body = module_body | Pierre Letouzey | |
| After this commit, module_type_body is a particular case of module_type. For a [module_type_body], the implementation field [mod_expr] is supposed to be always [Abstract]. This is verified by coqchk, even if this isn't so crucial, since [mod_expr] is never read in the case of a module type. Concretely, this amounts to the following rewrite on field names for module_type_body: - typ_expr --> mod_type - typ_expr_alg --> mod_type_alg - typ_* --> mod_* and adding two new fields to mtb: - mod_expr (always containing Abstract) - mod_retroknowledge (always containing []) This refactoring should be completely transparent for the user. Pros: code sharing, for instance subst_modtype = subst_module. Cons: a runtime invariant (mod_expr = Abstract) which isn't enforced by typing. I tried a polymorphic typing of mod_expr, to share field names while not having mtb = mb, but the OCaml typechecker isn't clever enough with polymorphic mutual fixpoints, and reject code sharing (e.g. between subst_modtype and subst_module). In the future (with ocaml>=4), some GADT could maybe help here, but for now the current solution seems good enough. | |||
| 2015-01-11 | Extraction: discard unnecessary code inside modules without signatures | Pierre Letouzey | |
| In the case of an inner module without explicit signature, (and not used later in a functor application), we now extract only the needed items (used later or asked by the user), instead of blindly extracting all fields as earlier. | |||
| 2015-01-11 | Extraction: no more ascii blob in type variables (fix #3227) | Pierre Letouzey | |
| Since type variables are local to the definition, we simply rename them in case of unicode chars. We also get rid of any ' to avoid Ocaml illegal 'a' type var (clash with char litteral). | |||
| 2015-01-11 | Extraction : some more support functions for a future "Extraction Compute" | Pierre Letouzey | |
| 2015-01-11 | Extraction: minor tweaks to ease ongoing experiments about Lambda | Pierre Letouzey | |
| - Common.get_native_char instead of just a pp function of this char - Enrich the record projection table | |||
| 2015-01-10 | Adding more sharing in Map.udpate and Map.modify. | Pierre-Marie Pédrot | |
| 2015-01-10 | CHANGES: mention "Optimize (Heap|Proof)" | Enrico Tassi | |
| 2015-01-09 | STM: fix handling of side effects in vio2vo | Enrico Tassi | |
| 2015-01-08 | Continuing 785f82ee1 on reverting not only f5d7b2b1e but also | Hugo Herbelin | |
| fd98174afe6 about fixing hypothesis alpha-conversion strategy for This completion of the reverting fixes #3905. | |||
| 2015-01-08 | Fixing compilation of penultimate commit d08532d. | Hugo Herbelin | |
| 2015-01-08 | Setting ?n=?p order to ?p:=?n to see if it solves some incompatibilities wrt ↵ | Hugo Herbelin | |
| 8.4. | |||
| 2015-01-08 | Avoiding introducing yet another convention in naming files. | Hugo Herbelin | |
| 2015-01-08 | Update + English in CHANGES | Hugo Herbelin | |
| 2015-01-08 | Start credits for 8.5. | Matthieu Sozeau | |
| 2015-01-08 | Small fix in whodidwhat 8.5. | Pierre Courtieu | |
| 2015-01-08 | Fixed and extend bullet related info/error messages. + doc. | Pierre Courtieu | |
| Had to put some hook in the handler of Proofview.NoSuchgoals. Documentation updated. CHANGE updated. | |||
| 2015-01-08 | Fix some documentation typos. | Guillaume Melquiond | |
| 2015-01-08 | Add a few words in whodidwhat. | Maxime Dénès | |
| 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. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |