From 844d512b117303b04729498623eff10b030e6837 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 22 Oct 2004 12:30:16 +0000 Subject: [PATCH] ported to typed explicit subst --- helm/ocaml/tactics/proofEngineHelpers.ml | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml index 03257dfa1..d78b94afa 100644 --- a/helm/ocaml/tactics/proofEngineHelpers.ml +++ b/helm/ocaml/tactics/proofEngineHelpers.ml @@ -28,8 +28,12 @@ let new_meta_of_proof ~proof:(_, metasenv, _, _) = let subst_meta_in_proof proof meta term newmetasenv = let uri,metasenv,bo,ty = proof in - (* empty context is ok for term since it wont be used by apply_subst *) - let subst_in = CicMetaSubst.apply_subst [meta,([], term)] in + (* empty context is ok for term since it wont be used by apply_subst *) + (* hack: since we do not know the context and the type of term, we + create a substitution with cc =[] and type = Implicit; they will be + in any case dropped by apply_subst, but it would be better to rewrite + the code. Cannot we just use apply_subst_metasenv, etc. ?? *) + let subst_in = CicMetaSubst.apply_subst [meta,([], term,Cic.Implicit None)] in let metasenv' = newmetasenv @ (List.filter (function (m,_,_) -> m <> meta) metasenv) in -- 2.39.2