SimonBoulier
SimonBoulier
I would want to clean a bit the headers. * Do we have to keep the `(* Distributed under the terms of the MIT license. *)`? Some files does not...
Everywhere in the code we convert our `Constr.t` to some `EConstr.t` and back. I consider moving everything to `EConstr` (and continue carrying the evarmap). Do you agree it is the...
Template polymorphism is not implemented. For template polymorphism see: [refman](https://coq.inria.fr/refman/cic.html#Template-polymorphism) The following compiles in Coq: ``` Definition T := {A : Type & {B : Type & A}}. ``` While...
There is a test in this file which fails. (Usually it is commented because it takes much time.)
Also there is something very confusing. As far as I understand: ``` Require Import Program. From Equations Require Import Equations. ``` will use `dependent induction` of `Program`. But ``` Require...