From bdf8b4edb650c847f83d520d31f23f14c58233b6 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Mon, 5 Sep 2011 16:46:48 +0000
Subject: 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
---
 plugins/extraction/extraction.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index b9c42c30d5..b780b64bb3 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -1018,7 +1018,7 @@ let extract_inductive env kn =
 	  let l' = filter (succ i) l in
 	  if isDummy (expand env t) || List.mem i implicits then l'
 	  else t::l'
-    in filter 1 l
+    in filter (1+ind.ind_nparams) l
   in
   let packets =
     Array.mapi (fun i p -> { p with ip_types = Array.mapi (f i) p.ip_types })
-- 
cgit v1.2.3