Merge tag 'upstream/8.6'

Upstream version 8.6

1 files changed, 3 insertions, 3 deletions

diff --git a/coq.mli b/coq.mli
index 1004d2c..4d46c7d 100644
--- a/coq.mli
+++ b/coq.mli
@@ -147,9 +147,9 @@ module Equivalence : sig
 end
 
 (** [match_as_equation ?context goal c] try to decompose c as a
-    relation applied to two terms. An optionnal rel_context can be
+    relation applied to two terms. An optionnal rel-context can be
     provided to ensure that the term remains typable *)
-val match_as_equation  : ?context:Context.rel_context -> goal_sigma -> Term.constr -> (Term.constr * Term.constr * Relation.t) option
+val match_as_equation  : ?context:Context.Rel.t -> 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 : Context.rel_context; 	(** the quantifications of the hypothese *)
+      context : Context.Rel.t;		(** the quantifications of the hypothese *)
       body : Term.constr; 		(** the body of the hypothese*)
       rel : Relation.t; 		(** the relation  *)
       left : Term.constr;		(** left hand side *)