Merge pull request #816 from LPCIC/fix-luno

Fix deriv.paramX non-uniform parameter bug

Author: gares

apps/derive/elpi/param2.elpi

@@ -119,9 +119,9 @@ param-match (fun N T B) P1 PRM :-
 
 pred param-indt i:inductive, i:bool, i:int, i:int, i:term, i:list term, i:list term,
      i:inductive, o:bool, o:int, o:int, o:term, o:list term.
-param-indt GR IsInd Lno _ Ty Knames Ktypes
+param-indt GR IsInd Lno Luno Ty Knames Ktypes
  	   NameR IsInd LnoR LunoR TyR KtypesR :- do! [
-  LnoR is 3 * Lno, LunoR = LnoR,
+  LnoR is 3 * Lno, LunoR is 3 * Luno,
   param (global (indt GR)) (global (indt GR)) (global (indt NameR)) => do! [
     param Ty _ TyR,
     map2 Knames Ktypes param-indc KtypesR

apps/derive/tests/test_param1.v

@@ -186,4 +186,8 @@ Fixpoint nat_eq (n m : nat) {struct n} : bool :=
 
 Elpi derive.param1 nat_eq.
 
+Inductive Acc {A : Type} (R : A -> A -> Prop) | (x : A) : Prop :=
+    Acc_intro : (forall y : A, R y x -> Acc y) -> Acc x.
+Elpi derive.param1 Acc.
+
 End OtherTests.

apps/derive/tests/test_param2.v

@@ -101,3 +101,7 @@ Fail Elpi derive.param2 fb.
 Definition fa_R := O_R.
 Elpi derive.param2.register fa fa_R.
 Elpi derive.param2 fb.
+
+Inductive Acc {A : Type} (R : A -> A -> Prop) | (x : A) : Prop :=
+    Acc_intro : (forall y : A, R y x -> Acc y) -> Acc x.
+Elpi derive.param2 Acc.