From 6c71f229e191796120bc50a859e1257a686ea49d Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 20 Feb 2006 15:55:35 +0000 Subject: [PATCH] Packing of implicit coercions must be also performed as soon as an object (or proof status) is created. --- helm/software/components/grafite_engine/grafiteEngine.ml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index 26fc540d8..bea1ec74e 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -628,8 +628,8 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status cmd -> (match types with (name,_,_,_)::_ -> name | _ -> assert false) | _ -> assert false in let uri = - UriManager.uri_of_string (GrafiteTypes.qualify status name ^ ext) - in + UriManager.uri_of_string (GrafiteTypes.qualify status name ^ ext) in + let obj = CicRefine.pack_coercion_obj obj in let metasenv = GrafiteTypes.get_proof_metasenv status in match obj with | Cic.CurrentProof (_,metasenv',bo,ty,_,_) -> @@ -664,7 +664,6 @@ 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; - assert (metasenv = metasenv'); let initial_proof = (Some uri, metasenv, bo, ty) in let initial_stack = Continuationals.Stack.of_metasenv metasenv in { status with GrafiteTypes.proof_status = -- 2.39.2