Extraction Implicit: fix the numbering of constructor arguments

 For constructors, the numbers of parameters used to be wrongly
 ignored. Consider for instance :

  Inductive listn (A:Type) : nat -> Type :=
   | niln : listn A 0
   | consn : forall n, A -> listn A n -> listn A (S n).

 Saying "Extraction Implicit consn [n]" should now work correctly,
 and correspond to the alternative syntax "Extraction Implicit consn [2]",
 where 2 is the position of the argument n when counting with
 inductive parameters.

 Note that saying "Extraction Implicit consn [1]" (or [A]) is now
 a no-op : constructors have always been cleaned-up from their
 parameters during extraction.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14449 85f007b7-540e-0410-9357-904b9bb8a0f7

0 files changed, 0 insertions, 0 deletions