From 176d8e004153e65688dc8ef4f22f7939fd6101b1 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 21 Jan 2016 18:45:36 +0100 Subject: New step on recent 9c2662eecc398f3 (strong invariants on tuple pattern). - Fixing dead code, doc. - Relaxing constraints on using an as-tuple in inversion. --- tactics/tacticals.mli | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'tactics/tacticals.mli') diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 4b7053611..ffcc71b45 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -111,10 +111,10 @@ type branch_assumptions = { ba : branch_args; (** the branch args *) assums : Context.Named.t} (** the list of assumptions introduced *) -(** [check_disjunctive_pattern_size loc pats n] returns an appropriate - error message if |pats| <> n; extends them if no pattern is given +(** [get_and_check_or_and_pattern loc pats branchsign] returns an appropriate + error message if |pats| <> |branchsign|; extends them if no pattern is given for let-ins in the case of a conjunctive pattern *) -val get_and_check_or_and_pattern : +val get_and_check_or_and_pattern : Loc.t -> delayed_open_constr or_and_intro_pattern_expr -> bool list array -> intro_patterns array -- cgit v1.2.3