From f4b9cc6f689b52e0408ac3231ba2a480d71216fb Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Mon, 2 Feb 2004 16:11:37 +0000 Subject: [PATCH] changed prototype of CicMetaSubst.apply_subst* --- helm/ocaml/tactics/primitiveTactics.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml index 518c6f86a..5c187b053 100644 --- a/helm/ocaml/tactics/primitiveTactics.ml +++ b/helm/ocaml/tactics/primitiveTactics.ml @@ -499,7 +499,7 @@ da subst1!!!! Dovrei rimuoverle o sono innocue?*) let apply_subst _ t = let t' = CicMetaSubst.apply_subst subst1 t in CicMetaSubst.apply_subst_reducing - subst2 (Some (emeta,List.length fargs)) t' + (Some (emeta,List.length fargs)) subst2 t' in let old_uninstantiatedmetas,new_uninstantiatedmetas = classify_metas newmeta in_subst_domain apply_subst @@ -521,8 +521,8 @@ da subst1!!!! Dovrei rimuoverle o sono innocue?*) let apply_subst' t = let t' = CicMetaSubst.apply_subst subst1 t in CicMetaSubst.apply_subst_reducing - ((metano,bo')::subst2) - (Some (emeta,List.length fargs)) t' + (Some (emeta,List.length fargs)) + ((metano,bo')::subst2) t' in subst_meta_and_metasenv_in_proof proof metano apply_subst' newmetasenv''' -- 2.39.2