From: Claudio Sacerdoti Coen Date: Wed, 17 Mar 2010 14:56:31 +0000 (+0000) Subject: OCaml's inferred type simplified. X-Git-Tag: make_still_working~3001 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5d917dca1e20e201ada174da2c36796f73a24623;p=helm.git OCaml's inferred type simplified. --- diff --git a/helm/software/components/ng_tactics/nTactics.mli b/helm/software/components/ng_tactics/nTactics.mli index e1a5de895..a4b2bde68 100644 --- a/helm/software/components/ng_tactics/nTactics.mli +++ b/helm/software/components/ng_tactics/nTactics.mli @@ -28,10 +28,7 @@ val compare_statuses : past:#NTacStatus.lowtac_status -> present:#NTacStatus.low val distribute_tac: NTacStatus.lowtac_status NTacStatus.lowtactic -> 's NTacStatus.tactic -val exec : ((int * Continuationals.Stack.switch) list * 'a list * 'b list * - [> `NoTag ]) - list NTacStatus.status NTacStatus.tactic -> - (#NTacStatus.lowtac_status as 's) -> Continuationals.goal -> 's +val exec : NTacStatus.tac_status NTacStatus.tactic -> 's NTacStatus.lowtactic val block_tac: 's NTacStatus.tactic list -> 's NTacStatus.tactic val apply_tac: NTacStatus.tactic_term -> 's NTacStatus.tactic