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: 0.4.95@7852~1644
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=df24c9854cfed6335626925ca1e8f9773424eb39;p=helm.git

Stupid bug fixed.
---

diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml
index bea1ec74e..0bbb01403 100644
--- a/components/grafite_engine/grafiteEngine.ml
+++ b/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 } },