aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker
Commit message (Collapse)AuthorAge
...
| * | Implementing Herbelin's fix for the "NonPar" bugGravatar mlasson2015-09-03
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Hugo Herbelin proposed to modify directly the function "check_correct_par" to simplify commit c12b430 (see the pullrequest's discussion). Note that the constructor "LocalNonPar" has now three arguments (instead of two). In LocalNonPar (n,i,l) n denotes the position among real arguments (ie. ignoring letins), i is the rel index of the expecting argument in the context of parameters and l is the index of the inductive.
| * | Reverting 16 last commits, committed mistakenly using the wrong push command.Gravatar Hugo Herbelin2015-08-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Sorry so much. Reverted: 707bfd5719b76d131152a258d49740165fbafe03. 164637cc3a4e8895ed4ec420e300bd692d3e7812. b9c96c601a8366b75ee8b76d3184ee57379e2620. 21e41af41b52914469885f40155702f325d5c786. 7532f3243ba585f21a8f594d3dc788e38dfa2cb8. 27fb880ab6924ec20ce44aeaeb8d89592c1b91cd. fe340267b0c2082b3af8bc965f7bc0e86d1c3c2c. d9b13d0a74bc0c6dff4bfc61e61a3d7984a0a962. 6737055d165c91904fc04534bee6b9c05c0235b1. 342fed039e53f00ff8758513149f8d41fa3a2e99. 21525bae8801d98ff2f1b52217d7603505ada2d2. b78d86d50727af61e0c4417cf2ef12cbfc73239d. 979de570714d340aaab7a6e99e08d46aa616e7da. f556da10a117396c2c796f6915321b67849f65cd. d8226295e6237a43de33475f798c3c8ac6ac4866. fdab811e58094accc02875c1f83e6476f4598d26.
| * | Hconsing continuedGravatar Hugo Herbelin2015-08-02
| | |
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-07-18
|\| |
| * | Univs/Inductive: fix typechecking of casesGravatar Matthieu Sozeau2015-07-15
| | | | | | | | | | | | | | | | | | | | | I was trying to be a bit too clever with not substituting the universe instance everywhere: the constructor type/inductive arity has to be instantiated before instantiate_params runs, which became true only for constructor types since my last commit.
| * | Updating checksum in checker (9c732a5cc continued).Gravatar Hugo Herbelin2015-07-12
| | | | | | | | | | | | | | | | | | Calling md5sum test earlier, at the time coqchk is built, rather than at testing time, hopefully moving it closer to what it is supposed to occur.
| * | Unused variables reported by OCaml.Gravatar Hugo Herbelin2015-07-10
| | |
| * | Option -type-in-type: added support in checker and making it contaminatingGravatar Hugo Herbelin2015-07-10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | in vo files (this was not done yet in 24d0027f0 and 090fffa57b). Reused field "engagement" to carry information about both impredicativity of set and type in type. For the record: maybe some further checks to do around the sort of the inductive types in coqchk?
| * | Kernel/Checker: Cleanup fixes of substitutions due to let-ins.Gravatar Matthieu Sozeau2015-07-09
| | | | | | | | | | | | | | | Avoid undeeded large substitutions, and add test-suite file for fixed bug 4283 in closed/
| * | Template polymorphism: A bug-fix for Bug #4258Gravatar mlasson2015-07-09
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Reviewed by M. Sozeau This commit fixes template polymorphism and makes it more precise, applying to non-linear uses of the same universe in parameters of template-polymorphic inductives. See bug report and https://github.com/coq/coq/pull/69 for full details. I also removed some deadcode in checker/inductive.ml. I do not know if it is also necessary to fix checker/indtypes.ml.
| * | Checker: Report bugfixes from kernel/inductive.mlGravatar Matthieu Sozeau2015-07-08
| | | | | | | | | | | | Wrong handling of mind_params_ctxt...
| * | Checker: Fix bug #4282Gravatar Matthieu Sozeau2015-07-07
| | | | | | | | | | | | | | | Adapt to new [projection] abstract type comprising a constant and a boolean.
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-06-28
|\| |
| * | 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.
| | * Adjust checker after `Assume [Positive]`.Gravatar Arnaud Spiwack2015-06-25
| |/ |/|
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-06-24
|\|
| * 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.
* | Moved fatal_error from Coqtop to Errors and corrected dependencies accordingly.Gravatar Thomas Sibut-Pinote2015-06-23
| | | | | | | | This allows fatal_error to be used for printing anomalies at loading time.
* | Merge remote-tracking branch 'forge/v8.5'Gravatar Pierre Boutillier2015-06-22
|\|
| * Votour displays wordsize of segments before loading them.Gravatar Pierre-Marie Pédrot2015-06-20
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-05-05
|\|
| * 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.
* | Merge branch 'v8.5' into trunkGravatar Pierre Letouzey2015-04-09
|\|
| * Removing references to deprecated syntax -I/-R -as.Gravatar Pierre-Marie Pédrot2015-03-31
| |
* | Merge branch 'v8.5' into trunkGravatar Enrico Tassi2015-03-30
|\|
| * 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
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-03-23
|\|
| * 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
| |
* | Now accepting unit props in mutual definitionsGravatar Bruno Barras2015-03-02
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-02-26
|\|
| * Fix checker after addition of a universe context in with t := c constraints.Gravatar Matthieu Sozeau2015-02-26
| |
* | Using same code for browsing physical directories in coqtop and coqdep.Gravatar Hugo Herbelin2015-02-16
| | | | | | | | | | | | | | | | 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.
| * 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
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 04:55:00 +0000