From: Stefano Zacchiroli Date: Wed, 27 Apr 2005 20:15:35 +0000 (+0000) Subject: renamed hbugs hint costructors to match latest API X-Git-Tag: single_binding~148 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d2331e9d78021cc61253d2127ac2f888892e224c;p=helm.git renamed hbugs hint costructors to match latest API --- diff --git a/helm/gTopLevel/hbugs.ml b/helm/gTopLevel/hbugs.ml index 35937b9b9..c8947c54d 100644 --- a/helm/gTopLevel/hbugs.ml +++ b/helm/gTopLevel/hbugs.ml @@ -119,17 +119,17 @@ module type Unit = sig end module Initialize (Tactics: InvokeTactics.Tactics) : Unit = struct let use_hint = function - | Use_ring_Luke -> Tactics.ring () - | Use_fourier_Luke -> Tactics.fourier () - | Use_reflexivity_Luke -> Tactics.reflexivity () - | Use_symmetry_Luke -> Tactics.symmetry () - | Use_assumption_Luke -> Tactics.assumption () - | Use_contradiction_Luke -> Tactics.contradiction () - | Use_exists_Luke -> Tactics.exists () - | Use_split_Luke -> Tactics.split () - | Use_left_Luke -> Tactics.left () - | Use_right_Luke -> Tactics.right () - | Use_apply_Luke term -> + | Use_ring -> Tactics.ring () + | Use_fourier -> Tactics.fourier () + | Use_reflexivity -> Tactics.reflexivity () + | Use_symmetry -> Tactics.symmetry () + | Use_assumption -> Tactics.assumption () + | Use_contradiction -> Tactics.contradiction () + | Use_exists -> Tactics.exists () + | Use_split -> Tactics.split () + | Use_left -> Tactics.left () + | Use_right -> Tactics.right () + | Use_apply term -> (* we remove the "cic:" prefix *) let term' = String.sub term 4 (String.length term - 4) in Tactics.apply ~term:term' ()