"by j let x : T such that P(x)" generalized to allow arbitrary justifications.

[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 1714bf470ac8c070e97a98e3327eee7a4183bb50..db08a6038f86bcf08c23f6fc33ec3994ef79010e 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -173,7 +173,8 @@ let tactic_of_ast status ast =
   | GrafiteAst.Byinduction (_, t, id) -> Declarative.byinduction t id
   | GrafiteAst.Thesisbecomes (_, t) -> Declarative.thesisbecomes t
   | GrafiteAst.ExistsElim (_, t, id1, t1, id2, t2) ->
-     Declarative.existselim t id1 t1 id2 t2
+     Declarative.existselim ~dbd:(LibraryDb.instance())
+      ~universe:status.GrafiteTypes.universe t id1 t1 id2 t2
   | GrafiteAst.Case (_,id,params) -> Declarative.case id params
   | GrafiteAst.AndElim(_,t,id1,t1,id2,t2) -> Declarative.andelim t id1 t1 id2 t2
   | GrafiteAst.RewritingStep (_,termine,t1,t2,cont) ->