| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2021-03-22 | [cbn internal] env is a regular positional argument | Gaëtan Gilbert | |
| This is more consistent with other code. | |||
| 2021-03-06 | Inline the refold and tactic_mode flags for the cbn tactic. | Pierre-Marie Pédrot | |
| They were unconditionally set to true, leading to a lot of dead branches. | |||
| 2021-02-24 | Infrastructure for fine-grained debug flags | Maxime Dénès | |
| 2021-01-18 | Move the only use of strong_with_flags to its single calling module. | Pierre-Marie Pédrot | |
| This also allows to move the strong variant of cbn to the Cbn module. | |||
| 2021-01-04 | Remove redundant univ and parameter info from CaseInvert | Gaëtan Gilbert | |
| 2021-01-04 | Change 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-10-21 | Add missing deprecations in Projection API. | Pierre-Marie Pédrot | |
| 2020-10-21 | Same little game with Projection. | Pierre-Marie Pédrot | |
| 2020-10-21 | Deprecate the non-qualified equality functions on kerpairs. | Pierre-Marie Pédrot | |
| This allows to quickly spot the parts of the code that rely on the canonical ordering. When possible we directly introduce the quotient-aware versions. | |||
| 2020-10-08 | Dropping the misleading int argument of Pp.h. | Hugo Herbelin | |
| An h-box inhibits the breaking semantics of any cut/spc/brk in the enclosed box. We tentatively replace its occurrence by an h or hv, assuming in particular that if the indentation is not 0, an hv box was intended. | |||
| 2020-07-24 | Fixes reduction effect printing in the presence of non purely applicative ↵ | Hugo Herbelin | |
| stacks. | |||
| 2020-07-06 | Primitive persistent arrays | Maxime 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-01 | UIP in SProp | Gaëtan Gilbert | |
| 2020-06-04 | Move the Cbn module to tactics/. | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |