diff options
Diffstat (limited to 'kernel/inductive.ml')
| -rw-r--r-- | kernel/inductive.ml | 34 |
1 files changed, 18 insertions, 16 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 28a09b81b0..91c042130a 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open CErrors @@ -796,18 +798,18 @@ let rec subterm_specif renv stack t = | Proj (p, c) -> let subt = subterm_specif renv stack c in - (match subt with - | Subterm (s, wf) -> - (* We take the subterm specs of the constructor of the record *) - let wf_args = (dest_subterms wf).(0) in - (* We extract the tree of the projected argument *) - let kn = Projection.constant p in - let cb = lookup_constant kn renv.env in - let pb = Option.get cb.const_proj in - let n = pb.proj_arg in - Subterm (Strict, List.nth wf_args n) - | Dead_code -> Dead_code - | Not_subterm -> Not_subterm) + (match subt with + | Subterm (s, wf) -> + (* We take the subterm specs of the constructor of the record *) + let wf_args = (dest_subterms wf).(0) in + (* We extract the tree of the projected argument *) + let kn = Projection.constant p in + let cb = lookup_constant kn renv.env in + let pb = Option.get cb.const_proj in + let n = pb.proj_arg in + spec_of_tree (List.nth wf_args n) + | Dead_code -> Dead_code + | Not_subterm -> Not_subterm) | Var _ | Sort _ | Cast _ | Prod _ | LetIn _ | App _ | Const _ | Ind _ | Construct _ | CoFix _ -> Not_subterm |