| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-01-14 | CHANGES: my recent updates to Ltac. | Arnaud Spiwack | |
| - gfail - multimatch - tryif/then/else | |||
| 2015-01-13 | Bump version and magic numbers in configure. | Maxime Dénès | |
| 2015-01-13 | Made -print-mod-uid more silent and robust. | Maxime Dénès | |
| This is a follow-up on Pierre's 5d80a385. | |||
| 2015-01-13 | Refresh some copyright headers. | Maxime Dénès | |
| 2015-01-13 | Native compiler: if debug flag not present, remove .native files. | Maxime Dénès | |
| 2015-01-13 | More documentation of the Local Definitions and Axioms. | Pierre-Marie Pédrot | |
| 2015-01-13 | More in CHANGES about local definitions | Pierre-Marie Pédrot | |
| 2015-01-13 | TCs: Properly handle Hint Extern with conclusions of the form _ -> _ | Matthieu Sozeau | |
| in typeclasses eauto, remaining compatible with eauto and still producing eta-reduced applications for Hint Resolves. Fixes bug #3794. | |||
| 2015-01-13 | Fix test-suite file, we were testing that no anomaly was raised | Matthieu Sozeau | |
| and this is the case now. | |||
| 2015-01-13 | Update hash of cic.mli in checker/values.ml, | Matthieu Sozeau | |
| letting make validate progress. | |||
| 2015-01-13 | Fix bug when discharging universe constraints coming from variables | Matthieu Sozeau | |
| into monomorphic constants, which was still using the de Bruijn encoding Bug revealed by discharging of hidden internal monomorphic definition in otherwise polymorphic developments. Makes coqchk work on Hurkens again. | |||
| 2015-01-13 | Fix issue in printing due to de Bruijn bug when constructing compatibility | Matthieu Sozeau | |
| constr for primitive records (not used anywhere else than printing). Problem reported by P. LeFanu Lumsdaine on HoTT/HoTT. Also add some minor fixes in detyping and pretty printing related to universes. | |||
| 2015-01-12 | typo in coqide compilation rules after -thread requirement | Pierre Boutillier | |
| 2015-01-12 | Derive -> derive occurences | Pierre Boutillier | |
| 2015-01-12 | Coq_makefile erases native compiler files | Pierre Boutillier | |
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |