From 01304bffd3ee2a66216214a9e1a8ee7fdfdf16e3 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 12 Nov 2009 10:03:51 +0000 Subject: [PATCH] Code made more uniform. --- helm/software/components/ng_tactics/nTactics.ml | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml index 6011d912d..d366c87d2 100644 --- a/helm/software/components/ng_tactics/nTactics.ml +++ b/helm/software/components/ng_tactics/nTactics.ml @@ -586,7 +586,7 @@ let case1_tac name = if name = "_clearme" then clear_tac ["_clearme"] else id_tac ] ;; -let constructor ?(num=1) ~args status goal = +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 @@ -596,11 +596,9 @@ let constructor ?(num=1) ~args status goal = Ast.Appl (HExtlib.list_concat ~sep:[Ast.Implicit `Vector] ([Ast.NRef ref] :: List.map (fun _,_,x -> [x]) args)) in - exec (apply_tac ("",0,t)) status goal + exec (apply_tac ("",0,t)) status goal) ;; -let constructor_tac ?num ~args = distribute_tac (constructor ?num ~args);; - let assert0_tac (hyps,concl) = distribute_tac (fun status goal -> let gty = get_goalty status goal in let eq status ctx t1 t2 = -- 2.39.2