From 19120824965a98e3afd8dd0993baa144e7ae5414 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gares@fettunta.org>
Date: Wed, 17 Oct 2018 11:16:21 +0200
Subject: [PATCH] few comments

---
 derive/induction.elpi                  | 1 +
 theories/derive/tests/test_induction.v | 2 ++
 2 files changed, 3 insertions(+)

diff --git a/derive/induction.elpi b/derive/induction.elpi
index 2a579b392..7571653b3 100644
--- a/derive/induction.elpi
+++ b/derive/induction.elpi
@@ -12,6 +12,7 @@ subst A B :- copy A B, !.
 % local db associating to each constructor the hypothesis to be used
 type induction-hyp-db term -> term -> prop.
 
+% TODO: fix for W (strip under lambda + map-db under forall)
 strip-last-arg (app [Hd|Args]) X R :-
   appendR Prefix [X] Args,
   if (Prefix = []) (R = Hd) (mk-app Hd Prefix R).
diff --git a/theories/derive/tests/test_induction.v b/theories/derive/tests/test_induction.v
index b989fdf73..d1b9a5be6 100644
--- a/theories/derive/tests/test_induction.v
+++ b/theories/derive/tests/test_induction.v
@@ -12,7 +12,9 @@ Elpi derive.induction Coverage.option.
 Elpi derive.induction Coverage.pair.
 Elpi derive.induction Coverage.seq.
 Elpi derive.induction Coverage.tree.
+(* TODO: non uniform params *)
 Fail Elpi derive.induction Coverage.nest.
+(* TODO: w *)
 Fail Elpi derive.induction Coverage.w.
 Elpi derive.induction Coverage.vect.
 Fail Elpi derive.induction Coverage.dyn.