Much ado about nothing:

[helm.git] / helm / software / components / acic_procedural / proceduralTypes.ml

diff --git a/helm/software/components/acic_procedural/proceduralTypes.ml b/helm/software/components/acic_procedural/proceduralTypes.ml
index 3ef27ea4020392e83173ee70dbc0d8af52247f69..8dac90f26bde2c20a7d9e0a5ebee5adcc986960e 100644 (file)
--- a/helm/software/components/acic_procedural/proceduralTypes.ml
+++ b/helm/software/components/acic_procedural/proceduralTypes.ml
@@ -98,6 +98,7 @@ let mk_arel i b = Cic.ARel ("", "", i, b)
 
 (* grafite ast constructors *************************************************)
 
+(*
 let floc = H.dummy_floc
 
 let mk_note str = G.Comment (floc, G.Note (floc, str))
@@ -138,8 +139,8 @@ let mk_rewrite direction what where pattern =
    mk_tactic tactic
 
 let mk_elim what using pattern =
-   let pattern = Some what, [], Some pattern in
-   let tactic = G.Elim (floc, pattern, using, Some 0, []) in
+   let pattern = None, [], Some pattern in
+   let tactic = G.Elim (floc, what, using, pattern, Some 0, []) in
    mk_tactic tactic
 
 let mk_apply t =
@@ -201,6 +202,8 @@ and render_steps sep a = function
       render_steps sep (render_step (Some mk_dot) a p) ps
 
 let render_steps a = render_steps None a
+*)
+let render_steps sep a = assert false
 
 (* counting *****************************************************************)