name specifications added for elim_intros, elim_intros_simpl and elim_type

[helm.git] / helm / ocaml / tactics / ring.ml

diff --git a/helm/ocaml/tactics/ring.ml b/helm/ocaml/tactics/ring.ml
index 298a87f3c8df8361fc4bcaee9f9cbaa5dc12c5d9..1d5fd903dead5cc09649faf676e9bb310e080b88 100644 (file)
--- a/helm/ocaml/tactics/ring.ml
+++ b/helm/ocaml/tactics/ring.ml
@@ -388,12 +388,13 @@ let elim_type_tac ~term status =
     @param term term to cut
     @param proof term used to prove second subgoal generated by elim_type
   *)
+(* FG: METTERE I NOMI ANCHE QUI? *)  
 let elim_type2_tac ~term ~proof =
  let elim_type2_tac ~term ~proof status =
   let module E = EliminationTactics in
   warn "in Ring.elim_type2";
   ProofEngineTypes.apply_tactic 
-   (Tacticals.thens ~start:(E.elim_type_tac ~term)
+   (Tacticals.thens ~start:(E.elim_type_tac term)
     ~continuations:[Tacticals.id_tac ; exact_tac ~term:proof]) status
  in
   ProofEngineTypes.mk_tactic (elim_type2_tac ~term ~proof)