diff options
| author | Pierre-Marie Pédrot | 2019-03-15 14:19:51 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-03-15 14:19:51 +0100 |
| commit | ed275fd5eb8b11003f8904010d853d2bd568db79 (patch) | |
| tree | e27b7778175cb0d9d19bd8bde9c593b335a85125 /vernac/comFixpoint.mli | |
| parent | a44c4a34202fa6834520fcd6842cc98eecf044ec (diff) | |
| parent | 1ba29c062e30181bda9d931dffe48e457dfee9d6 (diff) | |
Merge PR #8817: SProp: the definitionally proof irrelevant universe
Ack-by: JasonGross
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: gares
Ack-by: mattam82
Diffstat (limited to 'vernac/comFixpoint.mli')
| -rw-r--r-- | vernac/comFixpoint.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli index 338dfa5ef5..9bcb53697b 100644 --- a/vernac/comFixpoint.mli +++ b/vernac/comFixpoint.mli @@ -51,7 +51,7 @@ val interp_recursive : (* env / signature / univs / evar_map *) (Environ.env * EConstr.named_context * UState.universe_decl * Evd.evar_map) * (* names / defs / types *) - (Id.t list * EConstr.constr option list * EConstr.types list) * + (Id.t list * Sorts.relevance list * EConstr.constr option list * EConstr.types list) * (* ctx per mutual def / implicits / struct annotations *) (EConstr.rel_context * Impargs.manual_explicitation list * int option) list @@ -69,7 +69,7 @@ val extract_cofixpoint_components : structured_fixpoint_expr list * decl_notation list type recursive_preentry = - Id.t list * constr option list * types list + Id.t list * Sorts.relevance list * constr option list * types list val interp_fixpoint : cofix:bool -> |