diff options
Diffstat (limited to 'engine')
-rw-r--r-- | engine/eConstr.mli | 2 | ||||
-rw-r--r-- | engine/evarutil.mli | 4 | ||||
-rw-r--r-- | engine/evd.mli | 2 | ||||
-rw-r--r-- | engine/termops.mli | 24 |
4 files changed, 16 insertions, 16 deletions
diff --git a/engine/eConstr.mli b/engine/eConstr.mli index 913825a9f..ecb36615f 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -321,7 +321,7 @@ sig val to_named_decl : (t, types) Context.Named.Declaration.pt -> (Constr.t, Constr.types) Context.Named.Declaration.pt (** Physical identity. Does not care for defined evars. *) - val to_named_context : (t, types) Context.Named.pt -> Context.Named.t + val to_named_context : (t, types) Context.Named.pt -> Constr.named_context val to_sorts : ESorts.t -> Sorts.t (** Physical identity. Does not care for normalization. *) diff --git a/engine/evarutil.mli b/engine/evarutil.mli index 8ce1b625f..135aa73fc 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -128,7 +128,7 @@ val advance : evar_map -> Evar.t -> Evar.t option [nf_evar]. *) val undefined_evars_of_term : evar_map -> constr -> Evar.Set.t -val undefined_evars_of_named_context : evar_map -> Context.Named.t -> Evar.Set.t +val undefined_evars_of_named_context : evar_map -> Constr.named_context -> Evar.Set.t val undefined_evars_of_evar_info : evar_map -> evar_info -> Evar.Set.t type undefined_evars_cache @@ -161,7 +161,7 @@ val jv_nf_evar : val tj_nf_evar : evar_map -> unsafe_type_judgment -> unsafe_type_judgment -val nf_named_context_evar : evar_map -> Context.Named.t -> Context.Named.t +val nf_named_context_evar : evar_map -> Constr.named_context -> Constr.named_context val nf_rel_context_evar : evar_map -> rel_context -> rel_context val nf_env_evar : evar_map -> env -> env diff --git a/engine/evd.mli b/engine/evd.mli index 64db70451..d638bb2d3 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -230,7 +230,7 @@ val existential_opt_value : evar_map -> econstr pexistential -> econstr option val existential_opt_value0 : evar_map -> existential -> constr option -val evar_instance_array : (Context.Named.Declaration.t -> 'a -> bool) -> evar_info -> +val evar_instance_array : (Constr.named_declaration -> 'a -> bool) -> evar_info -> 'a array -> (Id.t * 'a) list val instantiate_evar_array : evar_info -> econstr -> econstr array -> econstr diff --git a/engine/termops.mli b/engine/termops.mli index f9aa6ba63..80988989f 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -43,14 +43,14 @@ val it_mkProd : types -> (Name.t * types) list -> types val it_mkLambda : constr -> (Name.t * 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 -> Context.Rel.t -> Constr.constr +val it_mkLambda_or_LetIn : Constr.constr -> Constr.rel_context -> Constr.constr val it_mkNamedProd_or_LetIn : types -> named_context -> types -val it_mkNamedProd_wo_LetIn : Constr.types -> Context.Named.t -> Constr.types +val it_mkNamedProd_wo_LetIn : Constr.types -> Constr.named_context -> Constr.types val it_mkNamedLambda_or_LetIn : constr -> named_context -> constr (* Ad hoc version reinserting letin, assuming the body is defined in the context where the letins are expanded *) -val it_mkLambda_or_LetIn_from_no_LetIn : Constr.constr -> Context.Rel.t -> Constr.constr +val it_mkLambda_or_LetIn_from_no_LetIn : Constr.constr -> Constr.rel_context -> Constr.constr (** {6 Generic iterators on constr} *) @@ -225,7 +225,7 @@ val names_of_rel_context : env -> names_context (* [context_chop n Γ] returns (Γ₁,Γ₂) such that [Γ]=[Γ₂Γ₁], [Γ₁] has [n] hypotheses, excluding local definitions, and [Γ₁], if not empty, starts with an hypothesis (i.e. [Γ₁] has the form empty or [x:A;Γ₁'] *) -val context_chop : int -> Context.Rel.t -> Context.Rel.t * Context.Rel.t +val context_chop : int -> Constr.rel_context -> Constr.rel_context * Constr.rel_context (* [env_rel_context_chop n env] extracts out the [n] top declarations of the rel_context part of [env], counting both local definitions and @@ -239,19 +239,19 @@ 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 lift_rel_context : int -> Context.Rel.t -> Context.Rel.t -val substl_rel_context : Constr.constr list -> Context.Rel.t -> Context.Rel.t -val smash_rel_context : Context.Rel.t -> Context.Rel.t (** expand lets in context *) +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 *) val map_rel_context_in_env : - (env -> Constr.constr -> Constr.constr) -> env -> Context.Rel.t -> Context.Rel.t + (env -> Constr.constr -> Constr.constr) -> env -> Constr.rel_context -> Constr.rel_context val map_rel_context_with_binders : (int -> 'c -> 'c) -> ('c, 'c) Context.Rel.pt -> ('c, 'c) Context.Rel.pt val fold_named_context_both_sides : - ('a -> Context.Named.Declaration.t -> Context.Named.Declaration.t list -> 'a) -> - Context.Named.t -> init:'a -> 'a + ('a -> Constr.named_declaration -> Constr.named_declaration list -> 'a) -> + Constr.named_context -> init:'a -> 'a val mem_named_context_val : Id.t -> named_context_val -> bool -val compact_named_context : Context.Named.t -> Context.Compacted.t +val compact_named_context : Constr.named_context -> Constr.compacted_context val map_rel_decl : ('a -> 'b) -> ('a, 'a) Context.Rel.Declaration.pt -> ('b, 'b) Context.Rel.Declaration.pt val map_named_decl : ('a -> 'b) -> ('a, 'a) Context.Named.Declaration.pt -> ('b, 'b) Context.Named.Declaration.pt @@ -313,6 +313,6 @@ val set_print_constr : (env -> Evd.evar_map -> constr -> Pp.t) -> unit val print_constr : constr -> Pp.t val print_constr_env : env -> Evd.evar_map -> constr -> Pp.t val print_named_context : env -> Pp.t -val pr_rel_decl : env -> Context.Rel.Declaration.t -> Pp.t +val pr_rel_decl : env -> Constr.rel_declaration -> Pp.t val print_rel_context : env -> Pp.t val print_env : env -> Pp.t |