X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FproofEngineTypes.ml;h=334c594da4b9d7d5564d5305825d463b83736e7d;hb=b38de2d3fa8bbe346c59c18bbeb889f29e493f63;hp=178be54d441a6e16ef01b3d6ec876be3ff974da9;hpb=bac72fcaa876137ab7a5630e0c1badc2a627dce8;p=helm.git

diff --git a/helm/ocaml/tactics/proofEngineTypes.ml b/helm/ocaml/tactics/proofEngineTypes.ml
index 178be54d4..334c594da 100644
--- a/helm/ocaml/tactics/proofEngineTypes.ml
+++ b/helm/ocaml/tactics/proofEngineTypes.ml
@@ -42,4 +42,4 @@ exception Fail of string
 
   (** constraint: the returned value will always be constructed by Cic.Name **)
 type mk_fresh_name_type =
- Cic.context -> Cic.name -> typ:Cic.term -> Cic.name
+ Cic.metasenv -> Cic.context -> Cic.name -> typ:Cic.term -> Cic.name