 11 Jul, 2016 1 commit


Robbert Krebbers authored
This class whose name is horrible and purpose is arbitrary seems to be a leftover of some experiment with ch2o, a long time a ago.

 05 Jul, 2016 1 commit


Robbert Krebbers authored

 31 May, 2016 1 commit


Robbert Krebbers authored

 23 Mar, 2016 2 commits


Ralf Jung authored

Robbert Krebbers authored

 05 Mar, 2016 2 commits
 04 Mar, 2016 2 commits


Robbert Krebbers authored

Robbert Krebbers authored

 03 Mar, 2016 1 commit


Robbert Krebbers authored

 24 Feb, 2016 3 commits


Robbert Krebbers authored
It now traverses terms at most once, whereas the setoid_rewrite approach was travering terms many times. Also, the tactic can now be extended by defining type class instances.

Robbert Krebbers authored

Robbert Krebbers authored
Also, use "set_solver by tac" to specify a tactic.

 22 Feb, 2016 2 commits


Robbert Krebbers authored
In most cases there is a lot of duplicate proof search performed by both naive_solver and eauto. Especially since naive_solver calls its tactic (in the case of set_solver this used to be eauto) quite eagerly this made it very slow. Note that set_solver is this too slow and should be improved.

Robbert Krebbers authored
In most cases there is a lot of duplicate proof search performed by both naive_solver and eauto. Especially since naive_solver calls its tactic (in the case of set_solver this used to be eauto) quite eagerly this made it very slow. Note that set_solver is this too slow and should be improved.

 17 Feb, 2016 3 commits


Robbert Krebbers authored
It is doing much more than just dealing with ∈, it solves all kinds of goals involving set operations (including ≡ and ⊆).

Robbert Krebbers authored
simplify_equality => simplify_eq simplify_equality' => simplify_eq/= simplify_map_equality => simplify_map_eq simplify_map_equality' => simplify_map_eq/= simplify_option_equality => simplify_option_eq simplify_list_equality => simplify_list_eq f_equal' => f_equal/= The /= suffixes (meaning: do simpl) are inspired by ssreflect.

Robbert Krebbers authored

 16 Feb, 2016 1 commit


Ralf Jung authored

 15 Feb, 2016 2 commits


Robbert Krebbers authored

Ralf Jung authored

 13 Feb, 2016 1 commit


Robbert Krebbers authored
Also, make our redefinition of done more robust under different orders of Importing modules.

 16 Jan, 2016 2 commits


Robbert Krebbers authored

Robbert Krebbers authored
This one (previously solve_elem_of) was hardly used. The tactic that uses naive_solver (previously esolve_elem_of, now solve_elem_of) has been extended with flags to say which hypotheses should be cleared/kept.

 04 Jan, 2016 1 commit


Ralf Jung authored

 11 Dec, 2015 1 commit


Robbert Krebbers authored

 20 Nov, 2015 1 commit


Robbert Krebbers authored
* Remove the order from RAs, it is now defined in terms of the ⋅ operation. * Define ownership using the stepindexed order. * Remove the order also from DRAs and change STS accordingly. While doing that, I changed STS to no longer use decidable token sets, which removes the requirement of decidable equality on tokens.

 18 Nov, 2015 1 commit


Robbert Krebbers authored

 17 Nov, 2015 1 commit


Robbert Krebbers authored

 16 Nov, 2015 2 commits


Robbert Krebbers authored

Robbert Krebbers authored

 03 Feb, 2017 1 commit


Robbert Krebbers authored

 01 Feb, 2017 1 commit


Robbert Krebbers authored
The port makes the following notable changes: * The carrier types of separation algebras and integer environments are no longer in Set. Now they have a type at a fixed type level above Set. This both works better in 8.5 and makes the formalization more general. I have tried putting them at polymorphic type levels, but that increased the compilation time by an order of magnitude. * I am using a custom f_equal tactic written in Ltac to circumvent bug #4069. That bug has been fixed, so this custom tactic can be removed when the next beta of 8.5 is out.

 04 Jun, 2015 1 commit


Robbert Krebbers authored

 02 Jun, 2015 1 commit


Robbert Krebbers authored

 22 Apr, 2015 1 commit


Robbert Krebbers authored

 16 Apr, 2015 1 commit


Robbert Krebbers authored

 02 Mar, 2015 1 commit


Robbert Krebbers authored

 08 Feb, 2015 2 commits


Robbert Krebbers authored

Robbert Krebbers authored
Important changes in the core semantics: * Types extended with function types. Since function types are a special kind of pointer types, types now have an additional mutual part called "ptr_type". * Pointers extended with function pointers. Theses are just names that refer to an actual function in the function environment. * Typing environments extended to assign argument and return types to function names. Before we used a separate environment for these, but since the argument and return types are already needed to type function pointers, this environment would appear in pretty much every typing judgment. As a sideeffect, the frontend has been rewritten entirely. The important changes are: * Type checking of expressions is more involved: there is a special kind of expression type corresponding to a function designator. * To handle things like block scoped extern function, more statefullness was needed. To prepare for future extensions, the entire frontend now uses a state monad.
