From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 12 Nov 2009 10:03:51 +0000 (+0000)
Subject: Code made more uniform.
X-Git-Tag: make_still_working~3211
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=01304bffd3ee2a66216214a9e1a8ee7fdfdf16e3;p=helm.git

Code made more uniform.
---

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 =