1. bug fixed in generalize_pattern: a lazy const_tac should have been

[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 aa056f3e2c35585c8d4c599bdbf055913918f1a9..8813e498bed94ae6425757af2e4d88ed1c025794 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -89,9 +89,9 @@ let rec tactic_of_ast status ast =
   | GrafiteAst.AutoBatch (_,params) ->
       Tactics.auto ~params ~dbd:(LibraryDb.instance ()) 
        ~universe:status.GrafiteTypes.universe
-  | GrafiteAst.Cases (_, what, (howmany, names)) ->
+  | GrafiteAst.Cases (_, what, pattern, (howmany, names)) ->
       Tactics.cases_intros ?howmany ~mk_fresh_name_callback:(namer_of names)
-        what
+        ~pattern what
   | GrafiteAst.Change (_, pattern, with_what) ->
      Tactics.change ~pattern with_what
   | GrafiteAst.Clear (_,id) -> Tactics.clear id
@@ -107,9 +107,10 @@ let rec tactic_of_ast status ast =
   | GrafiteAst.Decompose (_, names) ->
       let mk_fresh_name_callback = namer_of names in
       Tactics.decompose ~mk_fresh_name_callback ()
-  | GrafiteAst.Demodulate _ -> 
+  | GrafiteAst.Demodulate (_, params) -> 
       Tactics.demodulate 
-       ~dbd:(LibraryDb.instance ()) ~universe:status.GrafiteTypes.universe
+       ~dbd:(LibraryDb.instance ()) ~params 
+          ~universe:status.GrafiteTypes.universe
   | GrafiteAst.Destruct (_,xterms) -> Tactics.destruct xterms
   | GrafiteAst.Elim (_, what, using, pattern, (depth, names)) ->
       Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(namer_of names)
@@ -178,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) ->
@@ -192,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
@@ -556,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 
@@ -745,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