proof simplified

[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 bc56ce35dd7b16678b4553a63353c13c24866b97..3746403d951ea382e8360c2fcd2f933dc0f1cc07 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -179,9 +179,9 @@ let rec tactic_of_ast status ast =
   (* Implementazioni Aggiunte *)
   | GrafiteAst.Assume (_, id, t) -> Declarative.assume id t
   | GrafiteAst.Suppose (_, t, id, t1) -> Declarative.suppose t id t1
-  | GrafiteAst.By_term_we_proved (_, t, ty, id, t1) ->
-     Declarative.by_term_we_proved ~dbd:(LibraryDb.instance())
-      ~universe:status.GrafiteTypes.universe t ty id t1
+  | GrafiteAst.By_just_we_proved (_, just, ty, id, t1) ->
+     Declarative.by_just_we_proved ~dbd:(LibraryDb.instance())
+      ~universe:status.GrafiteTypes.universe just ty id t1
   | GrafiteAst.We_need_to_prove (_, t, id, t2) ->
      Declarative.we_need_to_prove t id t2
   | GrafiteAst.Bydone (_, t) ->
@@ -193,11 +193,13 @@ let rec tactic_of_ast status ast =
      Declarative.we_proceed_by_induction_on t t1
   | GrafiteAst.Byinduction (_, t, id) -> Declarative.byinduction t id
   | GrafiteAst.Thesisbecomes (_, t) -> Declarative.thesisbecomes t
-  | GrafiteAst.ExistsElim (_, t, id1, t1, id2, t2) ->
+  | GrafiteAst.ExistsElim (_, just, id1, t1, id2, t2) ->
      Declarative.existselim ~dbd:(LibraryDb.instance())
-      ~universe:status.GrafiteTypes.universe t id1 t1 id2 t2
+      ~universe:status.GrafiteTypes.universe just 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.AndElim(_,just,id1,t1,id2,t2) ->
+     Declarative.andelim ~dbd:(LibraryDb.instance ())
+      ~universe:status.GrafiteTypes.universe just id1 t1 id2 t2
   | GrafiteAst.RewritingStep (_,termine,t1,t2,cont) ->
      Declarative.rewritingstep ~dbd:(LibraryDb.instance ())
       ~universe:status.GrafiteTypes.universe termine t1 t2 cont
@@ -557,7 +559,7 @@ let add_coercions_of_record_to_moo obj lemmas status =
       let is_a_coercion uri =
         try
           let obj,_ = 
-            CicEnvironment.get_cooked_obj  CicUniv.empty_ugraph uri in
+            CicEnvironment.get_cooked_obj  CicUniv.oblivion_ugraph uri in
           let attrs = CicUtil.attributes_of_obj obj in
           try 
             match List.find 
@@ -746,7 +748,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
                    let t = CicUtil.term_of_uri u in
                    let ty',g = 
                      CicTypeChecker.type_of_aux' 
-                       metasenv' [] t CicUniv.empty_ugraph
+                       metasenv' [] t CicUniv.oblivion_ugraph
                    in
                    fst(CicReduction.are_convertible [] ty' ty g)) 
                similar