assert_tac now takes a list of sequents and also checks that the number of

[helm.git] / helm / software / components / grafite_engine / grafiteEngine.ml

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 1ad89f462f4c19e0580b3ce831f64275a70a5012..354413f1b9464307172ae2c18b3124887d3a07cd 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -586,10 +586,17 @@ let eval_ng_punct (_text, _prefix_len, punct) =
 let eval_ng_tac (text, prefix_len, tac) =
   match tac with
   | GrafiteAst.NApply (_loc, t) -> NTactics.apply_tac (text,prefix_len,t) 
-  | GrafiteAst.NAssert (_loc, hyps, concl) ->
+  | GrafiteAst.NAssert (_loc, seqs) ->
      NTactics.assert_tac
-      (List.map (function (id,`Decl t) -> id,`Decl (text,prefix_len,t) | (id,`Def (b,t)) -> id,`Def ((text,prefix_len,b),(text,prefix_len,t))) hyps,
-      (text,prefix_len,concl))
+      ((List.map
+        (function (hyps,concl) ->
+          List.map
+           (function
+              (id,`Decl t) -> id,`Decl (text,prefix_len,t)
+             |(id,`Def (b,t))->id,`Def((text,prefix_len,b),(text,prefix_len,t))
+           ) hyps,
+          (text,prefix_len,concl))
+       ) seqs)
   | GrafiteAst.NCases (_loc, what, where) ->
       NTactics.cases_tac 
         ~what:(text,prefix_len,what)