]> matita.cs.unibo.it Git - helm.git/commitdiff
Reindentation.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 23 Sep 2003 17:40:08 +0000 (17:40 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 23 Sep 2003 17:40:08 +0000 (17:40 +0000)
helm/gTopLevel/gTopLevel.ml

index 103a894ee79724bff7d7e839b8ec3dc591de3ea6..7d3985af3a56b63ef24059f16bac82e8f3a06232 100644 (file)
@@ -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 ;