Apply-Silvie tactic added!

diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml
index c00eb8404d2f8ca0a459bb28fbca4e0a328f02ac..ffd35c703b3ec30461ecbd94b58539c401094f86 100644 (file)
--- a/helm/software/components/grafite/grafiteAst.ml
+++ b/helm/software/components/grafite/grafiteAst.ml
@@ -47,6 +47,7 @@ type 'lazy_term reduction =
 type ('term, 'lazy_term, 'reduction, 'ident) tactic =
   | Absurd of loc * 'term
   | Apply of loc * 'term
+  | ApplyS of loc * 'term
   | Assumption of loc
   | Auto of loc * int option * int option * string option * string option 
       (* depth, width, paramodulation, full *) (* ALB *)

diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml
index 9038b3b6043a198c12add0c97da8d4c9106ef38b..9e1dffdcd48c226207b7da9ffd718303eb3ad1c2 100644 (file)
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/components/grafite/grafiteAstPp.ml
@@ -72,6 +72,7 @@ let rec pp_tactic ~term_pp ~lazy_term_pp =
   function
   | Absurd (_, term) -> "absurd" ^ term_pp term
   | Apply (_, term) -> "apply " ^ term_pp term
+  | ApplyS (_, term) -> "applyS " ^ term_pp term
   | Auto (_,_,_,Some kind,_) -> "auto " ^ kind
   | Auto _ -> "auto"
   | Assumption _ -> "assumption"

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index ff173bc37aa1d717ed3b7e32f69d26043b5a9b42..e4f70117a344bb41db8700aaa5d588d2cd3b834c 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -60,6 +60,8 @@ let tactic_of_ast ast =
   match ast with
   | GrafiteAst.Absurd (_, term) -> Tactics.absurd term
   | GrafiteAst.Apply (_, term) -> Tactics.apply term
+  | GrafiteAst.ApplyS (_, term) ->
+     Tactics.applyS ~term ~dbd:(LibraryDb.instance ())
   | GrafiteAst.Assumption _ -> Tactics.assumption
   | GrafiteAst.Auto (_,depth,width,paramodulation,full) ->
       AutoTactic.auto_tac ?depth ?width ?paramodulation ?full

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index 3d189983595ec968e62b30a3724e648d13c729d1..0e96aaf2dc871b303ed8436d158ab8a9c3229701 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -124,6 +124,9 @@ let disambiguate_tactic
     | GrafiteAst.Apply (loc, term) ->
         let metasenv,cic = disambiguate_term context metasenv term in
         metasenv,GrafiteAst.Apply (loc, cic)
+    | GrafiteAst.ApplyS (loc, term) ->
+        let metasenv,cic = disambiguate_term context metasenv term in
+        metasenv,GrafiteAst.ApplyS (loc, cic)
     | GrafiteAst.Assumption loc ->
         metasenv,GrafiteAst.Assumption loc
     | GrafiteAst.Auto (loc,depth,width,paramodulation,full) ->

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index 5bf73503b7503677b49341dae3956c7e58d84399..cbaed19b099d148a85805b75745fc4675e9297cc 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -128,6 +128,8 @@ EXTEND
         GrafiteAst.Absurd (loc, t)
     | IDENT "apply"; t = tactic_term ->
         GrafiteAst.Apply (loc, t)
+    | IDENT "applyS"; t = tactic_term ->
+        GrafiteAst.ApplyS (loc, t)
     | IDENT "assumption" ->
         GrafiteAst.Assumption loc
     | IDENT "auto";