aboutsummaryrefslogtreecommitdiff
path: root/kernel/relevanceops.ml
AgeCommit message (Collapse)Author
2021-01-04Change the representation of kernel case.Pierre-Marie Pédrot
We store bound variable names instead of functions for both branches and predicate, and we furthermore add the parameters in the node. Let bindings are not taken into account and require an environment lookup for retrieval.
2020-07-06Primitive persistent arraysMaxime Dénès
Persistent arrays expose a functional interface but are implemented using an imperative data structure. The OCaml implementation is based on Jean-Christophe Filliâtre's. Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr> Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
2020-07-01UIP in SPropGaëtan Gilbert
2020-03-18Rename Retypeops -> RelevanceopsGaëtan Gilbert
This module used to do retyping for the kernel in prototypes of SProp, but was switched to only relevance inference before the merge.