Stupid bug fixed.

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index bea1ec74e14e9e7f563a8a9dc868289ba8062b5f..0bbb014038439614647c4c83f8456ef7f339cb77 100644 (file)
--- 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 } },