X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FvariousTactics.ml;h=5e2e39c5df9343dab2d814aff8e59d4633469501;hb=1e51af833318b686d3852fbce5c1b516f3901b5a;hp=5be94e7df0dd87ee7b2c1368e30052d1e7318602;hpb=887340c4bccbc9f83dda7bb99c9d929852d9d1a9;p=helm.git

diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml
index 5be94e7df..5e2e39c5d 100644
--- a/helm/ocaml/tactics/variousTactics.ml
+++ b/helm/ocaml/tactics/variousTactics.ml
@@ -65,7 +65,7 @@ e li aggiunga nel context, poi si conta la lunghezza di questo nuovo
 contesto e si lifta di tot... COSA SIGNIFICA TUTTO CIO'?????? *)
 
 let generalize_tac 
- ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name) terms
+ ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) terms
  =
   let module PET = ProofEngineTypes in
   let generalize_tac mk_fresh_name_callback terms status =