X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FvariousTactics.ml;h=64b9ff790618c6305938d685229ecbb73c6801be;hb=c137ba88f68a47e567077909a23993c3c8c9854d;hp=28acd57ec250400b5144b5098999b68cca72e412;hpb=7b922ad1f9832c1edb3acea8f0c910fa2c0c20e5;p=helm.git diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml index 28acd57ec..64b9ff790 100644 --- a/helm/ocaml/tactics/variousTactics.ml +++ b/helm/ocaml/tactics/variousTactics.ml @@ -83,7 +83,7 @@ let generalize_tac ~start: (P.cut_tac (C.Prod( - (mk_fresh_name_callback context C.Anonymous typ), + (mk_fresh_name_callback metasenv context C.Anonymous typ), typ, (ProofEngineReduction.replace_lifting_csc 1 ~equality:(==)