From cb8aed8950ddf9820be556b4c6ca1810ec83e9b9 Mon Sep 17 00:00:00 2001
From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Thu, 21 Oct 2004 08:13:49 +0000
Subject: [PATCH] fixed a buggy pattern matching

---
 helm/ocaml/tactics/variousTactics.ml | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml
index d89f702fc..9293d1439 100644
--- a/helm/ocaml/tactics/variousTactics.ml
+++ b/helm/ocaml/tactics/variousTactics.ml
@@ -224,10 +224,12 @@ let auto_tac mqi_handle =
  let auto_tac mqi_handle (proof,goal) =
   prerr_endline "Entro in Auto";
   try 
-    let (proof,_)::_ = auto_new mqi_handle [(proof, [(goal,depth)])] in
-    prerr_endline "AUTO_TAC HA FINITO";
-(*     CicMetaSubst.print_counters (); *)
-    (proof,[])
+    (match auto_new mqi_handle [(proof, [(goal,depth)])] with
+    | (proof,_)::_  ->
+      prerr_endline "AUTO_TAC HA FINITO";
+  (*     CicMetaSubst.print_counters (); *)
+      (proof,[])
+    | _ -> assert false)
   with 
   | NoOtherChoices ->
       prerr_endline("Auto failed");
-- 
2.39.2