From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 31 Oct 2002 15:13:22 +0000 (+0000)
Subject: Bug fixed: the declared number of new goals of Apply was plainly wrong.
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5009b8ff136b9f8ef2f8fef35dfc8e3598d63e52;p=helm.git

Bug fixed: the declared number of new goals of Apply was plainly wrong.
---

diff --git a/helm/gTopLevel/primitiveTactics.ml b/helm/gTopLevel/primitiveTactics.ml
index 21d5d67c6..9974577a0 100644
--- a/helm/gTopLevel/primitiveTactics.ml
+++ b/helm/gTopLevel/primitiveTactics.ml
@@ -278,7 +278,7 @@ prerr_endline ("^^^^^TERMTY: " ^ CicPp.ppterm termty) ;
         let old_uninstantiatedmetas,new_uninstantiatedmetas =
          (* subst_in doesn't need the context. Hence the underscore. *)
          let subst_in _ = CicUnification.apply_subst subst in
-          classify_metas newmeta' in_subst_domain subst_in newmetasenv'
+          classify_metas newmeta in_subst_domain subst_in newmetasenv'
         in
          let bo' =
           apply_subst