Skip to content

Add a definition of the environment in smaller files

Guillaume Claret requested to merge add-environment-with-definitions into master

With the aim to give a definition to as much environment elements as possible, we add files corresponding to each environment module. These are copy&pastes with all the axioms. In the main environment file, with check that these files are compatible with what coq-of-ocaml generates.

Next we will be able to add definitions for common axioms (like list operations, monadic definitions, ...).

Edited by Guillaume Claret

Merge request reports