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 55b9d2e420ec8def3d11fd93902dfe1bb320486c..5909075d82f7aaf395d41ff5be5a2b2e4f887cc0 100644 (file)
--- 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 ;