]> matita.cs.unibo.it Git - helm.git/commitdiff
matita gtk3: some bugs fixed matita-lablgtk3
authorFerruccio Guidi <fguidi@maelstrom.helm.cs.unibo.it>
Sun, 29 Sep 2019 22:03:17 +0000 (00:03 +0200)
committerFerruccio Guidi <fguidi@maelstrom.helm.cs.unibo.it>
Sun, 29 Sep 2019 22:03:17 +0000 (00:03 +0200)
+ 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
matita/matita/matitaEngine.ml

index 11427e9a748dedf5024df2756f24a0559e6e75a0..721d9165b7d32d0388ba084d32fa27b6ff672125 100644 (file)
@@ -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
index fea7161c157fbe7a015383d1a2a35252b40434a4..6b4c6655b03a9d1ddc4769b10a80e4ed05295d0d 100644 (file)
@@ -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