From b183713e0e33245a4e58b433a930a94224d1f629 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 5 Oct 2009 14:23:02 +0000 Subject: [PATCH] downcast removed --- helm/software/components/ng_tactics/nTactics.ml | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml index 1644186a1..760d84e8d 100644 --- a/helm/software/components/ng_tactics/nTactics.ml +++ b/helm/software/components/ng_tactics/nTactics.ml @@ -234,9 +234,7 @@ let distribute_tac tac (status : #tac_status) = in aux s go gc loc_tl in - let s0 = - (new NTacStatus.status status#obj ())#set_estatus - (status :> NEstatus.status) in + let s0 = (new NTacStatus.status status#obj ())#set_estatus status in let s0, go0, gc0 = s0, [], [] in let sn, gon, gcn = aux s0 go0 gc0 g in debug_print (lazy ("opened: " -- 2.39.2