From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Mon, 2 Feb 2004 16:11:37 +0000 (+0000)
Subject: changed prototype of CicMetaSubst.apply_subst*
X-Git-Tag: V_0_2_3~115
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f4b9cc6f689b52e0408ac3231ba2a480d71216fb;p=helm.git

changed prototype of CicMetaSubst.apply_subst*
---

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'''