From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 20 Feb 2006 16:36:28 +0000 (+0000)
Subject: Stupid bug fixed.
X-Git-Tag: make_still_working~7546
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fa27a63c5a454664c98ce81f76133d088f4961cd;p=helm.git

Stupid bug fixed.
---

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index bea1ec74e..0bbb01403 100644
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -664,8 +664,8 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status cmd ->
                  ("Theorem already proved: " ^ UriManager.string_of_uri x ^ 
                   "\nPlease use a variant."));
            end;
-         let initial_proof = (Some uri, metasenv, bo, ty) in
-         let initial_stack = Continuationals.Stack.of_metasenv metasenv in
+         let initial_proof = (Some uri, metasenv', bo, ty) in
+         let initial_stack = Continuationals.Stack.of_metasenv metasenv' in
          { status with GrafiteTypes.proof_status =
             GrafiteTypes.Incomplete_proof
              { GrafiteTypes.proof = initial_proof; stack = initial_stack } },