Commits

Show all
Author Commit Message Labels Comments Date
Thomas Tuerk
improvements of relation library, bugfix in map library
Thomas Tuerk
merge Eq and Ineq type classes
Thomas Tuerk
improvements to relation library
Dominic Mulligan
Large changes to library for Coq backend * Improved bindings in library for Coq backend/ * Additions to coqharness.v for missing functionality.
Thomas Tuerk
bugfixes: intentity backend tests work again
Thomas Tuerk
rename library-new to library
Thomas Tuerk
removing the old library from the repository The new library is now mature enough to start replacing the old one completely for the library branch. This commit removes the old library and old infrastructure for testing it. Moreover, a new file "INSTALL.md" describes, how to use the new one.
Thomas Tuerk
make libraries work for ocaml
Thomas Tuerk
bugfixes to get the HOL libraries build again
Thomas Tuerk
added target "ocaml-lib-tests" target in library-new now the ocaml-tests can be executed easily
Thomas Tuerk
fixing bug in dictionary-passing / more work on libs
Thomas Tuerk
fix bug with not correctly adapted module prefix after inlining
Ohad Kammar
Bugfix: fix order of renaming of constants.
Ohad Kammar
Bugfix: renaming of set type for ocaml.
Thomas Tuerk
fix typechecking bug, set comprehensions now add the "ord" type-class constraint
Thomas Tuerk
Merge remote-tracking branch 'origin/library-format' into library-format
Thomas Tuerk
some work on generating libs added Makefile in library-new directory to generate the libraries for various backends
Gabriel Kerneis
Remove non-existant Option.get ocaml target_rep
Thomas Tuerk
work on relation library the library now uses only sets of pairs, but should (not tested yet) hopefully work for HOL and OCaml Testing will follow.
Thomas Tuerk
Merge remote-tracking branch 'origin/library-format' into library-format
Thomas Tuerk
fixed problem with different types of constants for different backends due to recent changes to dictionary passing
Ohad Kammar
Merge branch 'library-format' of bitbucket.org:Peter_Sewell/lem into library-format
Ohad Kammar
Implemented the old choose function. Bugfix in set_extra: Coq doesn't support the new choose function. Refactor: moved the now supported to_list function into its proper location in the file.
Gabriel Kerneis
Idiomatic extension check
Ohad Kammar
Bugfix: fixed module renaming of set_extra. Bugfix Transform.lem: added binding for the Set.to_list function. Documentation fix in set_extra. Refactored module renaming into the inside of the module.
Ohad Kammar
Merge branch 'library-format' of bitbucket.org:Peter_Sewell/lem into library-format
Ohad Kammar
Bugfix: without the module qualifier, Lem may get confused with the Set (or other) modules. Bugfix: Pmap module needs to be renamed in the lem backend.
Dominic Mulligan
Merge branch 'library-format' of https://bitbucket.org/Peter_Sewell/lem into library-format
Dominic Mulligan
Fixed bug wherein quantifiers were not being properly macro-expanded, removed unrestr. quant. from map.lem library * Fixed bug wherein quantifiers in set comprehensions were not being properly processed by the macro expander, so e.g. constructors with a target representation appearing in patterns are not properly replaced. * Removed unrestricted quantification in the map.lem library file by adding some new target representations for the Coq backend.
Thomas Tuerk
getting rid of some unnecessary dictionary arguments in theorem-prover backends Since equality is hard-coded, it does not need to be passed as a dictionary in the theorem prover backends. This change get's rid of type-classes like Eq, that are hardcoded for certain backends. The "Ord" typeclass is still used in many (unnecessary) places.
  1. Prev
  2. Next