aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker
Commit message (Collapse)AuthorAge
* 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.
* "allows to", like "allowing to", is improperGravatar Jason Gross2014-08-25
| | | | | | | | | | | It's possible that I should have removed more "allows", as many instances of "foo allows to bar" could have been replaced by "foo bars" (e.g., "[Qed] allows to check and save a complete proof term" could be "[Qed] checks and saves a complete proof term"), but not always (e.g., "the optional argument allows to ignore universe polymorphism" should not be "the optional argument ignores universe polymorphism" but "the optional argument allows the caller to instruct Coq to ignore universe polymorphism" or something similar).
* Port last changes of the guard condition to checker.Gravatar Maxime Dénès2014-08-06
|
* STM: encapsulate Pp.message in Feedback.feedbackGravatar Carst Tankink2014-08-04
|
* A tentative uniform naming policy in module Inductiveops.Gravatar Hugo Herbelin2014-08-01
| | | | | | | | | | | | - realargs: refers either to the indices of an inductive, or to the proper args of a constructor - params: refers to parameters (which are common to inductive and constructors) - allargs = params + realargs - realdecls: refers to the defining context of indices or proper args of a constructor (it includes letins) - paramdecls: refers to the defining context of params (it includes letins) - alldecls = paramdecls + realdecls
* Porting guard fix to checker.Gravatar Maxime Dénès2014-07-22
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 02:13:27 +0000