| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-01-12 | fixup to vi -> vio renaming | Enrico Tassi | |
| 2015-01-12 | Whodidwhat-8.5: a global pass | Arnaud Spiwack | |
| Updating my own work and others when I could think of them. | |||
| 2015-01-12 | whodidwhat-8.5: typo. | Arnaud Spiwack | |
| 2015-01-12 | Add -no-native-compiler flag to list dumped by --help. | Maxime Dénès | |
| 2015-01-12 | Add myself to credits. | Maxime Dénès | |
| 2015-01-12 | 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 | |
| incompatibilities wrt 8.4.", as it creates other problems (in Ergo and Compcert). This reverts commit bf388dfec041ab0fa74ae5d484600f6fcf515e4f. | |||
| 2015-01-12 | Fixing typo in previous commit. | Hugo Herbelin | |
| 2015-01-11 | 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 | |
| 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 | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |