Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Update credits. | Guillaume Melquiond | 2015-01-12 |
| | |||
* | Fix files in test-suite having to do with Require inside modules. | Maxime Dénès | 2015-01-12 |
| | |||
* | Update headers. | Maxime Dénès | 2015-01-12 |
| | |||
* | Update test for #3363 now that Require is forbidden inside modules. | Maxime Dénès | 2015-01-12 |
| | |||
* | Fix a few typos. | Maxime Dénès | 2015-01-12 |
| | |||
* | Fixing name of evars in output test Notation.v. | Hugo Herbelin | 2015-01-12 |
| | |||
* | Not "Setting ?n=?p order to ?p:=?n to see if it solves some | Hugo Herbelin | 2015-01-12 |
| | | | | | | | incompatibilities wrt 8.4.", as it creates other problems (in Ergo and Compcert). This reverts commit bf388dfec041ab0fa74ae5d484600f6fcf515e4f. | ||
* | Fixing typo in previous commit. | Hugo Herbelin | 2015-01-12 |
| | |||
* | Fixing wrong duplication message when finding both a .ml and a .ml4 in coqdep. | Hugo Herbelin | 2015-01-11 |
| | |||
* | Avoiding a redundant information in unification error message. | Hugo Herbelin | 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 | 2015-01-11 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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. | ||
* | Extraction: discard unnecessary code inside modules without signatures | Pierre Letouzey | 2015-01-11 |
| | | | | | | | 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. | ||
* | Extraction: no more ascii blob in type variables (fix #3227) | Pierre Letouzey | 2015-01-11 |
| | | | | | | 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). | ||
* | 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 | 2015-01-11 |
| | | | | | | - Common.get_native_char instead of just a pp function of this char - Enrich the record projection table | ||
* | 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-10 |
| | |||
* | STM: fix handling of side effects in vio2vo | Enrico Tassi | 2015-01-09 |
| | |||
* | Continuing 785f82ee1 on reverting not only f5d7b2b1e but also | Hugo Herbelin | 2015-01-08 |
| | | | | | | fd98174afe6 about fixing hypothesis alpha-conversion strategy for This completion of the reverting fixes #3905. | ||
* | 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 | 2015-01-08 |
| | | | | 8.4. | ||
* | 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 | 2015-01-08 |
| | | | | | Had to put some hook in the handler of Proofview.NoSuchgoals. Documentation updated. CHANGE updated. | ||
* | 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-08 |
| | |||
* | 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 | 2015-01-07 |
| | | | | | | typed-based matching: it provokes a stack overflow in contrib ClassicalRealisability. To be investigated later on. (See 893a02f643858ba0b0172648e77af9ccb65f03df.) | ||
* | Aligning printing of universe constraints. | Hugo Herbelin | 2015-01-07 |
| | |||
* | Hook when state arrives on master. | Enrico Tassi | 2015-01-07 |
| | |||
* | Fix checker's treatment of template polymorphic | Matthieu Sozeau | 2015-01-06 |
| | | | | | inductive instantiation, now using substitution of levels. Fixes the test-suite file coqchk/univ. | ||
* | 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 | 2015-01-06 |
| | | | 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]. | ||
* | Improve error recovery in case of ill-formed coqdoc comment. (Fix for bug ↵ | Guillaume Melquiond | 2015-01-06 |
| | | | | #3802.) | ||
* | updated include file for debugging | Bruno Barras | 2015-01-06 |
| | |||
* | improve efficiency of the reduction interpreter of coqtop | Bruno Barras | 2015-01-06 |
| | | | | | | | Conflicts: kernel/closure.ml kernel/closure.mli kernel/reduction.ml | ||
* | improve efficiency of the reduction interpreter of the checker | Bruno Barras | 2015-01-06 |
| | | | | | | | Conflicts: checker/closure.ml checker/closure.mli checker/reduction.ml | ||
* | 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 | 2015-01-06 |
| | | | | 3cd718c, to the case of second_order_matching. | ||
* | Fixing old filter bug in second_order_matching. | Hugo Herbelin | 2015-01-06 |
| |