From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Tue, 6 Apr 2004 09:50:39 +0000 (+0000)
Subject: bugfix: local context and canonical context previously don't have the
X-Git-Tag: dead_dir_walking~84
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=badfee5b6d3480172a3da91148605298f2b27986;p=helm.git

bugfix: local context and canonical context previously don't have the
same length
---

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 ;