From 5333af1b6dba295b496e75b0ba864f87ebc1eb88 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 23 Sep 2003 17:40:08 +0000 Subject: [PATCH] Reindentation. --- helm/gTopLevel/gTopLevel.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 103a894ee..7d3985af3 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -1674,8 +1674,7 @@ let open_ () = | Cic.Variable _ | Cic.InductiveDefinition _ -> raise NotADefinition in - ProofEngine.set_proof - (Some (uri, metasenv, bo, ty)) ; + ProofEngine.set_proof (Some (uri, metasenv, bo, ty)) ; set_proof_engine_goal None ; refresh_goals notebook ; refresh_proof output ; -- 2.39.2