diff options
| author | letouzey | 2011-09-05 16:46:48 +0000 |
|---|---|---|
| committer | letouzey | 2011-09-05 16:46:48 +0000 |
| commit | bdf8b4edb650c847f83d520d31f23f14c58233b6 (patch) | |
| tree | 36c3abf7b5a2a67d2306a7df37fb0cddc0ce025d /plugins | |
| parent | 82406b12adc9f59a186a38f863b0180855314b50 (diff) | |
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
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/extraction/extraction.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 }) |