Merge tag 'upstream/8.5.1'

Upstream version 8.5.1

1 files changed, 3 insertions, 3 deletions

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 *)