1. PrimitiveTactics.new_metasenv_for_apply changed a little bit, moved to

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

diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml
index e2003f48d4ab1b2b437393245b5b3aa8d9fa4476..8bbe05dcb77b1cc78f19e857033aec95e3bee5a2 100644 (file)
--- a/helm/ocaml/tactics/variousTactics.ml
+++ b/helm/ocaml/tactics/variousTactics.ml
@@ -72,6 +72,7 @@ let generalize_tac
  ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
  pattern
  =
+(*
   let module PET = ProofEngineTypes in
   let generalize_tac mk_fresh_name_callback
        ~pattern:(term,hyps_pat,concl_pat) status
@@ -142,4 +143,5 @@ let generalize_tac
        status
  in
   PET.mk_tactic (generalize_tac mk_fresh_name_callback ~pattern)
+*) assert false
 ;;