1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
|
(************************************************************************)
(* * The Rocq Prover / The Rocq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * 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 Names
open EConstr
type template_binder = {
bind_sort : Sorts.t;
default : Sorts.t;
}
(** NB: the types and rel_contexts may mention previous args
eg "sigT : forall A, (A -> Type) -> Type" is
"TemplateArg ([], u, TemplateArg ([_:Rel 1], v, IndType (_, [], Type@{max(u,v)})))"
note the "Rel 1" *)
type template_arity =
| NonTemplateArg of Name.t binder_annot * types * template_arity
| TemplateArg of Name.t binder_annot * rel_context * template_binder * template_arity
| DefParam of Name.t binder_annot * constr * types * template_arity
| CtorType of Declarations.template_universes * types
| IndType of Declarations.template_universes * rel_context * Sorts.t
val get_template_arity
: Environ.env
-> Names.inductive
-> ctoropt:int option
-> template_arity
|
