diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-26 15:30:02 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:30:43 +0100 |
| commit | 78a8d59b39dfcb07b94721fdcfd9241d404905d2 (patch) | |
| tree | 96cc7802206b80a19cc4760855357636892f9b9e /pretyping/inductiveops.ml | |
| parent | c8c8ccdaaffefdbd3d78c844552a08bcb7b4f915 (diff) | |
Introducing contexts parameterized by the inner term type.
This allows the decoupling of the notions of context containing kernel
terms and context containing tactic-level terms.
Diffstat (limited to 'pretyping/inductiveops.ml')
| -rw-r--r-- | pretyping/inductiveops.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 1dcd6399e..c00ceb02e 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -411,14 +411,14 @@ let build_dependent_constructor cs = applist (mkConstructU cs.cs_cstr, (List.map (lift cs.cs_nargs) cs.cs_params) - @(Context.Rel.to_extended_list 0 cs.cs_args)) + @(Context.Rel.to_extended_list mkRel 0 cs.cs_args)) let build_dependent_inductive env ((ind, params) as indf) = let arsign,_ = get_arity env indf in let nrealargs = List.length arsign in applist (mkIndU ind, - (List.map (lift nrealargs) params)@(Context.Rel.to_extended_list 0 arsign)) + (List.map (lift nrealargs) params)@(Context.Rel.to_extended_list mkRel 0 arsign)) (* builds the arity of an elimination predicate in sort [s] *) |