diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:06:42 +0000 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:06:42 +0000 |
commit | 1117d2e4a00debfbfa0157cc3e780916df72c26b (patch) | |
tree | d8713b1126725f216e1d5ff1dcc9561d84069145 /coq.mli | |
parent | 17564e4922acda6b72bf39de7a8c23ed0c0178f6 (diff) |
New upstream version 8.6
Diffstat (limited to 'coq.mli')
-rw-r--r-- | coq.mli | 6 |
1 files changed, 3 insertions, 3 deletions
@@ -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 *) |