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 /engine/termops.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 'engine/termops.mli')
| -rw-r--r-- | engine/termops.mli | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/engine/termops.mli b/engine/termops.mli index dea59e9efc..1dd9941c5e 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -23,9 +23,9 @@ val pr_fix : ('a -> Pp.t) -> ('a, 'a) pfixpoint -> Pp.t [@@ocaml.deprecated "Use [Constr.debug_print_fix]"] (** about contexts *) -val push_rel_assum : Name.t * types -> env -> env -val push_rels_assum : (Name.t * Constr.types) list -> env -> env -val push_named_rec_types : Name.t array * Constr.types array * 'a -> env -> env +val push_rel_assum : Name.t Context.binder_annot * types -> env -> env +val push_rels_assum : (Name.t Context.binder_annot * Constr.types) list -> env -> env +val push_named_rec_types : Name.t Context.binder_annot array * Constr.types array * 'a -> env -> env val lookup_rel_id : Id.t -> ('c, 't) Context.Rel.pt -> int * 'c option * 't (** Associates the contents of an identifier in a [rel_context]. Raise @@ -40,8 +40,8 @@ val rel_list : int -> int -> constr list (** iterators/destructors on terms *) val mkProd_or_LetIn : rel_declaration -> types -> types val mkProd_wo_LetIn : rel_declaration -> types -> types -val it_mkProd : types -> (Name.t * types) list -> types -val it_mkLambda : constr -> (Name.t * types) list -> constr +val it_mkProd : types -> (Name.t Context.binder_annot * types) list -> types +val it_mkLambda : constr -> (Name.t Context.binder_annot * types) list -> constr val it_mkProd_or_LetIn : types -> rel_context -> types val it_mkProd_wo_LetIn : types -> rel_context -> types val it_mkLambda_or_LetIn : Constr.constr -> Constr.rel_context -> Constr.constr @@ -246,7 +246,7 @@ val add_vname : Id.Set.t -> Name.t -> Id.Set.t (** other signature iterators *) val process_rel_context : (rel_declaration -> env -> env) -> env -> env -val assums_of_rel_context : ('c, 't) Context.Rel.pt -> (Name.t * 't) list +val assums_of_rel_context : ('c, 't) Context.Rel.pt -> (Name.t Context.binder_annot * 't) list val lift_rel_context : int -> Constr.rel_context -> Constr.rel_context val substl_rel_context : Constr.constr list -> Constr.rel_context -> Constr.rel_context val smash_rel_context : Constr.rel_context -> Constr.rel_context (** expand lets in context *) |