diff options
Diffstat (limited to 'engine/eConstr.mli')
| -rw-r--r-- | engine/eConstr.mli | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/engine/eConstr.mli b/engine/eConstr.mli index e4136a612..15463a8f6 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -73,6 +73,7 @@ val mkConstructU : pconstructor -> t val mkCase : case_info * t * t * t array -> t val mkFix : (t, t) pfixpoint -> t val mkCoFix : (t, t) pcofixpoint -> t +val mkArrow : t -> t -> t val applist : t * t list -> t @@ -81,6 +82,12 @@ val mkLambda_or_LetIn : Rel.Declaration.t -> t -> t val it_mkProd_or_LetIn : t -> Rel.t -> t val it_mkLambda_or_LetIn : t -> Rel.t -> t +val mkNamedLambda : Id.t -> types -> constr -> constr +val mkNamedLetIn : Id.t -> constr -> types -> constr -> constr +val mkNamedProd : Id.t -> types -> types -> types +val mkNamedLambda_or_LetIn : Named.Declaration.t -> types -> types +val mkNamedProd_or_LetIn : Named.Declaration.t -> types -> types + (** {6 Simple case analysis} *) val isRel : Evd.evar_map -> t -> bool @@ -141,6 +148,7 @@ val eq_constr_nounivs : Evd.evar_map -> t -> t -> bool val eq_constr_universes : Evd.evar_map -> t -> t -> Universes.universe_constraints option val leq_constr_universes : Evd.evar_map -> t -> t -> Universes.universe_constraints option val eq_constr_universes_proj : Environ.env -> Evd.evar_map -> t -> t -> Universes.universe_constraints option +val compare_constr : Evd.evar_map -> (t -> t -> bool) -> t -> t -> bool (** {6 Iterators} *) |