From 17564e4922acda6b72bf39de7a8c23ed0c0178f6 Mon Sep 17 00:00:00 2001 From: Nicolas Braud-Santoni Date: Sat, 23 Jul 2016 16:21:44 -0400 Subject: Imported Upstream version 8.5.1 --- coq.mli | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'coq.mli') diff --git a/coq.mli b/coq.mli index 53d42eb..1004d2c 100644 --- a/coq.mli +++ b/coq.mli @@ -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 *) -- cgit v1.2.3