From 41dfa9c8a69428f59683f5ab964b217c67ebe46e Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 6 Dec 2012 13:03:09 +0000 Subject: [PATCH] Bug fixed: %n was badly failing (with Failure "nth") when n was not a valid constructor. Now fail is raised (to be captured by try, etc.) --- matita/components/ng_tactics/nTactics.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/matita/components/ng_tactics/nTactics.ml b/matita/components/ng_tactics/nTactics.ml index 044f496f1..6870dab57 100644 --- a/matita/components/ng_tactics/nTactics.ml +++ b/matita/components/ng_tactics/nTactics.ml @@ -624,9 +624,9 @@ let case1_tac name = ;; let constructor_tac ?(num=1) ~args = distribute_tac (fun status goal -> - if num < 1 then fail (lazy "constructor numbers begin with 1"); let gty = get_goalty status goal in - let status, (r,_,_,_) = analyse_indty status gty in + let status, (r,consno,_,_) = analyse_indty status gty in + if num < 1 || num > consno then fail (lazy "Non existant constructor"); let ref = NReference.mk_constructor num r in let t = if args = [] then Ast.NRef ref else -- 2.39.2