From 5009b8ff136b9f8ef2f8fef35dfc8e3598d63e52 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 31 Oct 2002 15:13:22 +0000 Subject: [PATCH] Bug fixed: the declared number of new goals of Apply was plainly wrong. --- helm/gTopLevel/primitiveTactics.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 -- 2.39.2