diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-13 20:38:41 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:28:50 +0100 |
| commit | 485bbfbed4ae4a28119c4e42c5e40fd77abf4f8a (patch) | |
| tree | ab397f012c1d9ea53e041759309b08cccfeac817 /engine/eConstr.mli | |
| parent | 771be16883c8c47828f278ce49545716918764c4 (diff) | |
Tactics API using EConstr.
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} *) |