| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-06-24 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-06-24 | On-demand Require. | Pierre-Marie Pédrot | |
| Marshalled libraries are only loaded when needed and dropped thereafter. This might be costly for Require inside modules, but such a practice is discouraged anyway. | |||
| 2015-06-24 | Splitting the library representation on disk in two. | Pierre-Marie Pédrot | |
| The first part only contains the summary of the library, while the second one contains the effective content of it. | |||
| 2015-06-23 | Moved fatal_error from Coqtop to Errors and corrected dependencies accordingly. | Thomas Sibut-Pinote | |
| This allows fatal_error to be used for printing anomalies at loading time. | |||
| 2015-06-22 | Merge remote-tracking branch 'forge/v8.5' | Pierre Boutillier | |
| 2015-06-20 | Votour displays wordsize of segments before loading them. | Pierre-Marie Pédrot | |
| 2015-05-05 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-04-23 | Remove almost all the uses of string concatenation when building error messages. | Guillaume Melquiond | |
| Since error messages are ultimately passed to Format, which has its own buffers for concatenating strings, using concatenation for preparing error messages just doubles the workload and increases memory pressure. | |||
| 2015-04-09 | Merge branch 'v8.5' into trunk | Pierre Letouzey | |
| 2015-03-31 | Removing references to deprecated syntax -I/-R -as. | Pierre-Marie Pédrot | |
| 2015-03-30 | Merge branch 'v8.5' into trunk | Enrico Tassi | |
| 2015-03-25 | Exporting memory representation of STM tasks for votour. | Pierre-Marie Pédrot | |
| 2015-03-24 | Functorized interface over object representation in votour. | Pierre-Marie Pédrot | |
| This gives more safety in object manipulation, as we delimit the uses of Obj functions, and allows for an alternative implementation of the representation of OCaml structures. | |||
| 2015-03-24 | Fixing representation of dynamics in votour (again). | Pierre-Marie Pédrot | |
| 2015-03-23 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-03-23 | coqchk: more prints when -debug | Enrico Tassi | |
| 2015-03-18 | Fixing internal representation of Dyn.t in votour. | Pierre-Marie Pédrot | |
| 2015-03-02 | Now accepting unit props in mutual definitions | Bruno Barras | |
| 2015-03-02 | Now accepting unit props in mutual definitions | Bruno Barras | |
| 2015-02-26 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-02-26 | Fix checker after addition of a universe context in with t := c constraints. | Matthieu Sozeau | |
| 2015-02-16 | Using same code for browsing physical directories in coqtop and coqdep. | Hugo Herbelin | |
| In particular: - abstracting the code using calls to Unix opendir, stat, and closedir, - uniformly using warnings when a directory does not exist (coqtop was ignoring silently and coqdep was exiting via handle_unix_error), - uniformly expecting paths in Unix format and warning otherwise. | |||
| 2015-02-12 | Revert "Using same code for browsing physical directories in coqtop and coqdep." | Hugo Herbelin | |
| (Sorry, was not intended to be pushed) This reverts commit 5268efdefb396267bfda0c17eb045fa2ed516b3c. | |||
| 2015-02-12 | Revert "Capital letter in plugins." (Sorry, was not intended to be pushed) | Hugo Herbelin | |
| This reverts commit bff2b36cb0e2dbd02c4f181fba545a420e847767. | |||
| 2015-02-12 | Capital letter in plugins. | Hugo Herbelin | |
| 2015-02-12 | Using same code for browsing physical directories in coqtop and coqdep. | Hugo Herbelin | |
| In particular: - abstracting the code using calls to Unix opendir, stat, and closedir, - uniformly using warnings when a directory does not exist (coqtop was ignoring silently and coqdep was exiting via handle_unix_error). | |||
| 2015-02-11 | Fixing bug #4019, and checker blow-up at once. | Pierre-Marie Pédrot | |
| 2015-02-11 | Clarifying the implementation of universe hashconsing. | Pierre-Marie Pédrot | |
| 2015-02-05 | Windows: open .vo files in binary mode | Enrico Tassi | |
| 2015-01-13 | Update hash of cic.mli in checker/values.ml, | Matthieu Sozeau | |
| letting make validate progress. | |||
| 2015-01-12 | Update headers. | Maxime Dénès | |
| 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-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 | rename: vi -> vio | Enrico Tassi | |
| 2015-01-06 | updated include file for debugging | Bruno Barras | |
| 2015-01-06 | improve efficiency of the reduction interpreter of the checker | Bruno Barras | |
| Conflicts: checker/closure.ml checker/closure.mli checker/reduction.ml | |||
| 2014-12-26 | coqchk: flush the pp buffer from time to time | Enrico Tassi | |
| 2014-12-23 | Vi2vo: fix handling of univ constraints coming from the body | Enrico Tassi | |
| 2014-12-19 | Fixing performance issue of checker validation. | Pierre-Marie Pédrot | |
| The validation process was passing most of its time in the construction of the name of the current context. | |||
| 2014-12-19 | Fixing checker representation of values. | Pierre-Marie Pédrot | |
| 2014-12-19 | update md5 sums to make "make check" work | Enrico Tassi | |
| 2014-12-19 | Fix sigsegv in checker | Enrico Tassi | |
| 2014-12-18 | Fixing checker representation of universe lists. | Pierre-Marie Pédrot | |
| 2014-12-18 | Backporting the change in lists of universes to the checker. | Pierre-Marie Pédrot | |
| 2014-12-17 | checker: Change in library on disk values, now using context_sets instead of | Matthieu Sozeau | |
| constraints only. | |||
| 2014-12-17 | Ensuring the good invariants of hashcons table generation in the API. | Pierre-Marie Pédrot | |
| 2014-12-17 | Update checker/values and cic due to changes in case_info and record_body. | Matthieu Sozeau | |
| 2014-11-14 | Exit with code 129 when an anomaly occurs. | Xavier Clerc | |
| 2014-10-20 | A patch for printing "match" when constructors are defined with let-in | Hugo Herbelin | |
| but the internal representation dropped let-in. Ideally, the internal representation of the "match" should use contexts for the predicate and the branches. This would however be a rather significant change. In the meantime, just a hack. To do, there is still an extra @ in the constructor name that does not need to be there. | |||
| 2014-09-06 | Remove debug printing code | Matthieu Sozeau | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |