aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker
Commit message (Collapse)AuthorAge
* Adding a more efficient representation of OCaml objects in votour.Gravatar Pierre-Marie Pédrot2015-06-25
|
* Moved fatal_error from Coqtop to Errors and corrected dependencies accordingly.Gravatar Thomas Sibut-Pinote2015-06-25
| | | | This allows fatal_error to be used for printing anomalies at loading time.
* On-demand Require.Gravatar Pierre-Marie Pédrot2015-06-24
| | | | | | 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.
* Splitting the library representation on disk in two.Gravatar Pierre-Marie Pédrot2015-06-24
| | | | | The first part only contains the summary of the library, while the second one contains the effective content of it.
* Votour displays wordsize of segments before loading them.Gravatar Pierre-Marie Pédrot2015-06-20
|
* Remove almost all the uses of string concatenation when building error messages.Gravatar Guillaume Melquiond2015-04-23
| | | | | | 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.
* Removing references to deprecated syntax -I/-R -as.Gravatar Pierre-Marie Pédrot2015-03-31
|
* Exporting memory representation of STM tasks for votour.Gravatar Pierre-Marie Pédrot2015-03-25
|
* Functorized interface over object representation in votour.Gravatar Pierre-Marie Pédrot2015-03-24
| | | | | | 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.
* Fixing representation of dynamics in votour (again).Gravatar Pierre-Marie Pédrot2015-03-24
|
* coqchk: more prints when -debugGravatar Enrico Tassi2015-03-23
|
* Fixing internal representation of Dyn.t in votour.Gravatar Pierre-Marie Pédrot2015-03-18
|
* Now accepting unit props in mutual definitionsGravatar Bruno Barras2015-03-02
|
* Fix checker after addition of a universe context in with t := c constraints.Gravatar Matthieu Sozeau2015-02-26
|
* Revert "Using same code for browsing physical directories in coqtop and coqdep."Gravatar Hugo Herbelin2015-02-12
| | | | | | (Sorry, was not intended to be pushed) This reverts commit 5268efdefb396267bfda0c17eb045fa2ed516b3c.
* Revert "Capital letter in plugins." (Sorry, was not intended to be pushed)Gravatar Hugo Herbelin2015-02-12
| | | | This reverts commit bff2b36cb0e2dbd02c4f181fba545a420e847767.
* Capital letter in plugins.Gravatar Hugo Herbelin2015-02-12
|
* Using same code for browsing physical directories in coqtop and coqdep.Gravatar Hugo Herbelin2015-02-12
| | | | | | | 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).
* Fixing bug #4019, and checker blow-up at once.Gravatar Pierre-Marie Pédrot2015-02-11
|
* Clarifying the implementation of universe hashconsing.Gravatar Pierre-Marie Pédrot2015-02-11
|
* Windows: open .vo files in binary modeGravatar Enrico Tassi2015-02-05
|
* Update hash of cic.mli in checker/values.ml,Gravatar Matthieu Sozeau2015-01-13
| | | | letting make validate progress.
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Declarations.mli refactoring: module_type_body = module_bodyGravatar Pierre Letouzey2015-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.
* Fix checker's treatment of template polymorphicGravatar Matthieu Sozeau2015-01-06
| | | | | inductive instantiation, now using substitution of levels. Fixes the test-suite file coqchk/univ.
* rename: vi -> vioGravatar Enrico Tassi2015-01-06
|
* updated include file for debuggingGravatar Bruno Barras2015-01-06
|
* improve efficiency of the reduction interpreter of the checkerGravatar Bruno Barras2015-01-06
| | | | | | | Conflicts: checker/closure.ml checker/closure.mli checker/reduction.ml
* coqchk: flush the pp buffer from time to timeGravatar Enrico Tassi2014-12-26
|
* Vi2vo: fix handling of univ constraints coming from the bodyGravatar Enrico Tassi2014-12-23
|
* Fixing performance issue of checker validation.Gravatar Pierre-Marie Pédrot2014-12-19
| | | | | The validation process was passing most of its time in the construction of the name of the current context.
* Fixing checker representation of values.Gravatar Pierre-Marie Pédrot2014-12-19
|
* update md5 sums to make "make check" workGravatar Enrico Tassi2014-12-19
|
* Fix sigsegv in checkerGravatar Enrico Tassi2014-12-19
|
* Fixing checker representation of universe lists.Gravatar Pierre-Marie Pédrot2014-12-18
|
* Backporting the change in lists of universes to the checker.Gravatar Pierre-Marie Pédrot2014-12-18
|
* checker: Change in library on disk values, now using context_sets instead ofGravatar Matthieu Sozeau2014-12-17
| | | | constraints only.
* Ensuring the good invariants of hashcons table generation in the API.Gravatar Pierre-Marie Pédrot2014-12-17
|
* Update checker/values and cic due to changes in case_info and record_body.Gravatar Matthieu Sozeau2014-12-17
|
* Exit with code 129 when an anomaly occurs.Gravatar Xavier Clerc2014-11-14
|
* A patch for printing "match" when constructors are defined with let-inGravatar Hugo Herbelin2014-10-20
| | | | | | | | | | | 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.
* Remove debug printing codeGravatar Matthieu Sozeau2014-09-06
|
* Cleanup code for looking up projection bodies.Gravatar Matthieu Sozeau2014-09-06
|
* Fix checker to handle projections with eta and universe polymorphism correctly,Gravatar Matthieu Sozeau2014-09-06
| | | | simplifying conversion code.
* Fix checker to handle projections with eta and universe polymorphism correctly.Gravatar Matthieu Sozeau2014-09-06
|
* Fix checking of constants in checker. Prelude can now be checked.Gravatar Matthieu Sozeau2014-09-06
|
* Remove unused substitution functions in checker.Gravatar Matthieu Sozeau2014-09-05
|
* Fix checker treatment of inductives using subst_instances instead of ↵Gravatar Matthieu Sozeau2014-09-05
| | | | subst_univs_levels.
* Fix checker/values.ml with latest changes due to projections and universes.Gravatar Matthieu Sozeau2014-09-05
|
* Rename eta_expand_ind_stacks, fix the one from the checker and adaptGravatar Matthieu Sozeau2014-09-05
| | | | | it to the new representation of projections and the new mind_finite type.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 17:09:13 +0000