From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:53:30 +0100 Subject: Imported Upstream version 8.6 --- tactics/hipattern.mli | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'tactics/hipattern.mli') diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli index 32938ce5..7cc41f1b 100644 --- a/tactics/hipattern.mli +++ b/tactics/hipattern.mli @@ -119,11 +119,11 @@ val match_with_equation: (** Match terms [eq A t u], [identity A t u] or [JMeq A t A u] Returns associated lemmas and [A,t,u] or fails PatternMatchingFailure *) -val find_eq_data_decompose : [ `NF ] Proofview.Goal.t -> constr -> +val find_eq_data_decompose : ([ `NF ], 'r) Proofview.Goal.t -> constr -> coq_eq_data * Univ.universe_instance * (types * constr * constr) (** Idem but fails with an error message instead of PatternMatchingFailure *) -val find_this_eq_data_decompose : [ `NF ] Proofview.Goal.t -> constr -> +val find_this_eq_data_decompose : ([ `NF ], 'r) Proofview.Goal.t -> constr -> coq_eq_data * Univ.universe_instance * (types * constr * constr) (** A variant that returns more informative structure on the equality found *) @@ -144,7 +144,7 @@ val is_matching_sigma : constr -> bool val match_eqdec : constr -> bool * constr * constr * constr * constr (** Match an equality up to conversion; returns [(eq,t1,t2)] in normal form *) -val dest_nf_eq : [ `NF ] Proofview.Goal.t -> constr -> (constr * constr * constr) +val dest_nf_eq : ([ `NF ], 'r) Proofview.Goal.t -> constr -> (constr * constr * constr) (** Match a negation *) val is_matching_not : constr -> bool -- cgit v1.2.3