fix detype

Author: gares

Changelog.md

@@ -1,5 +1,14 @@
 # Changelog
 
+## [2.0.2] - 22/01/2024
+
+Requires Elpi 1.18.1 and Coq 8.19.
+
+### API
+- Fix `coq.elaborate-*` does not erase the type annotation of `Let`s (regression
+  introduced in 2.0.1). This fix may introduce differences in generated names
+- Fix `coq.elaborate-*` are not affected anymore by printing options
+
 ## [2.0.1] - 29/12/2023
 
 Requires Elpi 1.18.1 and Coq 8.19.

apps/derive/tests/test_projK.v

@@ -59,11 +59,11 @@ Check eq_refl 0 : projEnvelope1 nat 1 1 (Envelope nat 0 1) = 0.
 Check projEnvelope2 : forall A, A -> A -> zeta A -> A.
 Check eq_refl 0 : projEnvelope2 nat 1 1 (Envelope nat 1 0) = 0.
 Check projRedex1 : forall A, A -> beta A -> A.
-Check projWhy1 : forall n : peano, match n with 
+Check projWhy1 : forall n : peano, match n return Type with 
                     | Zero => peano
                     | Succ _ => unit
                     end -> iota -> peano.
-Check projWhy2 : forall n : peano, match n with 
+Check projWhy2 : forall n : peano, match n return Type with 
                     | Zero => peano
                     | Succ _ => unit
                     end -> iota -> { i : peano & match i with Zero => peano | Succ _ => unit end }.