X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FprimitiveTactics.ml;h=5909075d82f7aaf395d41ff5be5a2b2e4f887cc0;hb=75daba96a032eae3d8f3179b4cee36e280dc77c3;hp=55b9d2e420ec8def3d11fd93902dfe1bb320486c;hpb=09cfe0657d77c16be2cc1974cb5242939f1d98fb;p=helm.git

diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml
index 55b9d2e42..5909075d8 100644
--- a/helm/ocaml/tactics/primitiveTactics.ml
+++ b/helm/ocaml/tactics/primitiveTactics.ml
@@ -219,13 +219,10 @@ let
           in
            (match ty with
                C.Sort C.Type as s ->
-                let irl =
-                  CicMkImplicit.identity_relocation_list_for_metavariable context
-                in
                  let fresh_meta = !next_fresh_meta in
                  let fresh_meta' = fresh_meta + 1 in
                   next_fresh_meta := !next_fresh_meta + 2 ;
-                  let subst_item = uri,C.Meta (fresh_meta',irl) in
+                  let subst_item = uri,C.Meta (fresh_meta',[]) in
                    newmetasenvfragment :=
                     (fresh_meta,[],C.Sort C.Type) ::
                      (fresh_meta',[],C.Meta (fresh_meta,[])) :: !newmetasenvfragment ;