changed prototype of CicMetaSubst.apply_subst*

diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml
index 518c6f86acc5daaa36c3724c2b404276972020dd..5c187b05367c92eecd6241b4db3378531b245fc1 100644 (file)
--- 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'''