diff options
Diffstat (limited to 'coq.mli')
| -rw-r--r-- | coq.mli | 6 |
1 files changed, 3 insertions, 3 deletions
@@ -40,6 +40,7 @@ val cps_evar_relation : Term.constr -> (Term.constr -> Proof_type.tactic) -> Pro (** [cps_mk_letin name v] binds the constr [v] using a letin tactic *) val cps_mk_letin : string -> Term.constr -> ( Term.constr -> Proof_type.tactic) -> Proof_type.tactic +val retype : Term.constr -> Proof_type.tactic val decomp_term : Term.constr -> (Term.constr , Term.types) Term.kind_of_term val lapp : Term.constr lazy_t -> Term.constr array -> Term.constr @@ -79,7 +80,6 @@ end module Leibniz : sig val eq_refl : Term.types -> Term.constr -> Term.constr - val eq : Term.types -> Term.constr end module Option : sig @@ -149,7 +149,7 @@ end (** [match_as_equation ?context goal c] try to decompose c as a relation applied to two terms. An optionnal rel_context can be provided to ensure that the term remains typable *) -val match_as_equation : ?context:Term.rel_context -> goal_sigma -> Term.constr -> (Term.constr * Term.constr * Relation.t) option +val match_as_equation : ?context:Context.rel_context -> goal_sigma -> Term.constr -> (Term.constr * Term.constr * Relation.t) option (** {2 Some tacticials} *) @@ -190,7 +190,7 @@ type hypinfo = { hyp : Term.constr; (** the actual constr corresponding to the hypothese *) hyptype : Term.constr; (** the type of the hypothesis *) - context : Term.rel_context; (** the quantifications of the hypothese *) + context : Context.rel_context; (** the quantifications of the hypothese *) body : Term.constr; (** the body of the hypothese*) rel : Relation.t; (** the relation *) left : Term.constr; (** left hand side *) |