]> matita.cs.unibo.it Git - helm.git/commitdiff
Stupid bug fixed.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 20 Feb 2006 16:36:28 +0000 (16:36 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 20 Feb 2006 16:36:28 +0000 (16:36 +0000)
helm/software/components/grafite_engine/grafiteEngine.ml

index bea1ec74e14e9e7f563a8a9dc868289ba8062b5f..0bbb014038439614647c4c83f8456ef7f339cb77 100644 (file)
@@ -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 } },