From fa27a63c5a454664c98ce81f76133d088f4961cd Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 20 Feb 2006 16:36:28 +0000 Subject: [PATCH] Stupid bug fixed. --- helm/software/components/grafite_engine/grafiteEngine.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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 } }, -- 2.39.2