code refactoring for paramodulation

[helm.git] / helm / software / components / ng_tactics / nTactics.ml

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index fc0a8013cca3b09deb1b8ab9703499dc0f66d4f5..a384d54d56259f89952a7a14f8d013022cee568a 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -601,11 +601,13 @@ let auto ~params:(l,_) status goal =
         (status, (t,ty) :: l))
       (status,[]) l
   in
-  let pt, metasenv, subst = 
-    Paramod.nparamod status metasenv subst (ctx_of gty) (NCic.Rel ~-1,t) l 
-  in      
-  let status = status#set_obj (n,h,metasenv,subst,o) in
-  instantiate status goal (NTacStatus.mk_cic_term (ctx_of gty) pt)
+  match
+    NCicParamod.nparamod status metasenv subst (ctx_of gty) (NCic.Rel ~-1,t) l 
+  with
+  | [] -> raise (NTacStatus.Error (lazy "no proof found",None))
+  | (pt, metasenv, subst)::_ -> 
+      let status = status#set_obj (n,h,metasenv,subst,o) in
+      instantiate status goal (NTacStatus.mk_cic_term (ctx_of gty) pt)
 ;;
 
 let auto_tac ~params status =