From badfee5b6d3480172a3da91148605298f2b27986 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Tue, 6 Apr 2004 09:50:39 +0000 Subject: [PATCH] bugfix: local context and canonical context previously don't have the same length --- helm/ocaml/tactics/primitiveTactics.ml | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) 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 ; -- 2.39.2