From 5ea6d9e71ec0f2e55d42369cb15727713edab684 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 30 Sep 2019 00:03:17 +0200 Subject: [PATCH] matita gtk3: some bugs fixed + status#stack is a list of 5 components, not 4 + removed reference to Stdlib (was Pervasives) to comple with erlier versions of ocaml (ok with 4.0.5) --- matita/components/ng_tactics/nTactics.ml | 2 +- matita/matita/matitaEngine.ml | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/matita/components/ng_tactics/nTactics.ml b/matita/components/ng_tactics/nTactics.ml index 11427e9a7..721d9165b 100644 --- a/matita/components/ng_tactics/nTactics.ml +++ b/matita/components/ng_tactics/nTactics.ml @@ -704,7 +704,7 @@ let assert0_tac (hyps,concl) = distribute_tac (fun status goal -> let assert_tac seqs status = match status#stack with | [] -> assert false - | (g,_,_,_) :: _s -> + | (g,_,_,_,_) :: _s -> assert (List.length g = List.length seqs); (match seqs with [] -> id_tac diff --git a/matita/matita/matitaEngine.ml b/matita/matita/matitaEngine.ml index fea7161c1..6b4c6655b 100644 --- a/matita/matita/matitaEngine.ml +++ b/matita/matita/matitaEngine.ml @@ -122,9 +122,9 @@ let write_ast_to_file status fname statement = else (first_line := false; [Open_wronly; Open_trunc; Open_creat]) in let out_channel = - Stdlib.open_out_gen flaglist 0o0644 fname in - let _ = Stdlib.output_string out_channel ((if str.[0] <> '\n' then s else str) ^ "\n") in - let _ = Stdlib.close_out out_channel in + open_out_gen flaglist 0o0644 fname in + let _ = output_string out_channel ((if str.[0] <> '\n' then s else str) ^ "\n") in + let _ = close_out out_channel in str ) else -- 2.39.2