- bug fix in grafiteAstPp.ml
- some assertions in matitaEngine.ml
hLog.cmx: hLog.cmi
trie.cmo: trie.cmi
trie.cmx: trie.cmi
hLog.cmx: hLog.cmi
trie.cmo: trie.cmi
trie.cmx: trie.cmi
-discrimination_tree.cmo: trie.cmi discrimination_tree.cmi
-discrimination_tree.cmx: trie.cmx discrimination_tree.cmi
+discrimination_tree.cmo: trie.cmi hExtlib.cmi discrimination_tree.cmi
+discrimination_tree.cmx: trie.cmx hExtlib.cmx discrimination_tree.cmi
hTopoSort.cmo: hTopoSort.cmi
hTopoSort.cmx: hTopoSort.cmi
graphvizPp.cmo: graphvizPp.cmi
hTopoSort.cmo: hTopoSort.cmi
hTopoSort.cmx: hTopoSort.cmi
graphvizPp.cmo: graphvizPp.cmi
let rec pp_ntactic status ~map_unicode_to_tex =
let pp_tactic_pattern = pp_tactic_pattern ~map_unicode_to_tex in
function
let rec pp_ntactic status ~map_unicode_to_tex =
let pp_tactic_pattern = pp_tactic_pattern ~map_unicode_to_tex in
function
- | NApply (_,t) -> "napply " ^ NotationPp.pp_term status t
+ | NApply (_,t) -> "@" ^ NotationPp.pp_term status t
| NSmartApply (_,t) -> "fixme"
| NAuto (_,(None,flgs)) ->
"nautobatch" ^
| NSmartApply (_,t) -> "fixme"
| NAuto (_,(None,flgs)) ->
"nautobatch" ^
| NUnivConstraint (_) -> "not supported"
| NCoercion (_) -> "not supported"
| NObj (_,obj) -> NotationPp.pp_obj (NotationPp.pp_term status) obj
| NUnivConstraint (_) -> "not supported"
| NCoercion (_) -> "not supported"
| NObj (_,obj) -> NotationPp.pp_obj (NotationPp.pp_term status) obj
| NCopy (_,name,uri,map) ->
"copy " ^ name ^ " from " ^ NUri.string_of_uri uri ^ " with " ^
String.concat " and "
| NCopy (_,name,uri,map) ->
"copy " ^ name ^ " from " ^ NUri.string_of_uri uri ^ " with " ^
String.concat " and "
grafiteParser.cmi:
print_grammar.cmi: grafiteParser.cmi
grafiteParser.cmi:
print_grammar.cmi: grafiteParser.cmi
-dependenciesParser.cmo: dependenciesParser.cmi
-dependenciesParser.cmx: dependenciesParser.cmi
grafiteParser.cmo: grafiteParser.cmi
grafiteParser.cmx: grafiteParser.cmi
print_grammar.cmo: print_grammar.cmi
grafiteParser.cmo: grafiteParser.cmi
grafiteParser.cmx: grafiteParser.cmi
print_grammar.cmo: print_grammar.cmi
librarian.cmx: librarian.cmi
libraryMisc.cmo: libraryMisc.cmi
libraryMisc.cmx: libraryMisc.cmi
librarian.cmx: librarian.cmi
libraryMisc.cmo: libraryMisc.cmi
libraryMisc.cmx: libraryMisc.cmi
-libraryClean.cmo: libraryMisc.cmi libraryClean.cmi
-libraryClean.cmx: libraryMisc.cmx libraryClean.cmi
+libraryClean.cmo: libraryClean.cmi
+libraryClean.cmx: libraryClean.cmi
-utf8Macro.cmi:
-utf8MacroTable.cmo:
-utf8MacroTable.cmx:
-utf8Macro.cmo: utf8MacroTable.cmo utf8Macro.cmi
-utf8Macro.cmx: utf8MacroTable.cmx utf8Macro.cmi
+utf8Macro.cmi:
+utf8MacroTable.cmo:
+utf8MacroTable.cmx:
+utf8Macro.cmo: utf8MacroTable.cmo utf8Macro.cmi
+utf8Macro.cmx: utf8MacroTable.cmx utf8Macro.cmi
lablGraphviz.cmx: lablGraphviz.cmi
matitaclean.cmo: matitaMisc.cmi matitaInit.cmi matitaclean.cmi
matitaclean.cmx: matitaMisc.cmx matitaInit.cmx matitaclean.cmi
lablGraphviz.cmx: lablGraphviz.cmi
matitaclean.cmo: matitaMisc.cmi matitaInit.cmi matitaclean.cmi
matitaclean.cmx: matitaMisc.cmx matitaInit.cmx matitaclean.cmi
-matitac.cmo: matitaclean.cmi matitaMisc.cmi matitaInit.cmi matitaEngine.cmi
-matitac.cmx: matitaclean.cmx matitaMisc.cmx matitaInit.cmx matitaEngine.cmx
-matitaEngine.cmo: matitaEngine.cmi
-matitaEngine.cmx: matitaEngine.cmi
+matitac.cmo: matitaclean.cmi matitaMisc.cmi matitaInit.cmi matitaExcPp.cmi \
+ matitaEngine.cmi
+matitac.cmx: matitaclean.cmx matitaMisc.cmx matitaInit.cmx matitaExcPp.cmx \
+ matitaEngine.cmx
+matitaEngine.cmo: applyTransformation.cmi matitaEngine.cmi
+matitaEngine.cmx: applyTransformation.cmx matitaEngine.cmi
matitaExcPp.cmo: matitaEngine.cmi matitaExcPp.cmi
matitaExcPp.cmx: matitaEngine.cmx matitaExcPp.cmi
matitaGeneratedGui.cmo:
matitaExcPp.cmo: matitaEngine.cmi matitaExcPp.cmi
matitaExcPp.cmx: matitaEngine.cmx matitaExcPp.cmi
matitaGeneratedGui.cmo:
matitaGtkMisc.cmx: matitaTypes.cmx matitaGeneratedGui.cmx buildTimeConf.cmx \
matitaGtkMisc.cmi
matitaGui.cmo: matitaTypes.cmi matitaScript.cmi matitaMisc.cmi \
matitaGtkMisc.cmx: matitaTypes.cmx matitaGeneratedGui.cmx buildTimeConf.cmx \
matitaGtkMisc.cmi
matitaGui.cmo: matitaTypes.cmi matitaScript.cmi matitaMisc.cmi \
- matitaMathView.cmi matitaGtkMisc.cmi matitaGeneratedGui.cmo \
- matitaExcPp.cmi buildTimeConf.cmo matitaGui.cmi
+ matitaMathView.cmi matitaGuiTypes.cmi matitaGtkMisc.cmi \
+ matitaGeneratedGui.cmo matitaExcPp.cmi buildTimeConf.cmo matitaGui.cmi
matitaGui.cmx: matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \
matitaGui.cmx: matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \
- matitaMathView.cmx matitaGtkMisc.cmx matitaGeneratedGui.cmx \
- matitaExcPp.cmx buildTimeConf.cmx matitaGui.cmi
+ matitaMathView.cmx matitaGuiTypes.cmi matitaGtkMisc.cmx \
+ matitaGeneratedGui.cmx matitaExcPp.cmx buildTimeConf.cmx matitaGui.cmi
matitaInit.cmo: matitaExcPp.cmi buildTimeConf.cmo matitaInit.cmi
matitaInit.cmx: matitaExcPp.cmx buildTimeConf.cmx matitaInit.cmi
matitaMathView.cmo: virtuals.cmi matitaTypes.cmi matitaMisc.cmi \
matitaInit.cmo: matitaExcPp.cmi buildTimeConf.cmo matitaInit.cmi
matitaInit.cmx: matitaExcPp.cmx buildTimeConf.cmx matitaInit.cmi
matitaMathView.cmo: virtuals.cmi matitaTypes.cmi matitaMisc.cmi \
- matitaGuiTypes.cmi matitaGtkMisc.cmi matitaExcPp.cmi lablGraphviz.cmi \
- cicMathView.cmi buildTimeConf.cmo applyTransformation.cmi \
- matitaMathView.cmi
+ matitaGuiTypes.cmi matitaGtkMisc.cmi matitaGeneratedGui.cmo \
+ matitaExcPp.cmi lablGraphviz.cmi cicMathView.cmi buildTimeConf.cmo \
+ applyTransformation.cmi matitaMathView.cmi
matitaMathView.cmx: virtuals.cmx matitaTypes.cmx matitaMisc.cmx \
matitaMathView.cmx: virtuals.cmx matitaTypes.cmx matitaMisc.cmx \
- matitaGuiTypes.cmi matitaGtkMisc.cmx matitaExcPp.cmx lablGraphviz.cmx \
- cicMathView.cmx buildTimeConf.cmx applyTransformation.cmx \
- matitaMathView.cmi
+ matitaGuiTypes.cmi matitaGtkMisc.cmx matitaGeneratedGui.cmx \
+ matitaExcPp.cmx lablGraphviz.cmx cicMathView.cmx buildTimeConf.cmx \
+ applyTransformation.cmx matitaMathView.cmi
matitaMisc.cmo: matitaGuiTypes.cmi buildTimeConf.cmo matitaMisc.cmi
matitaMisc.cmx: matitaGuiTypes.cmi buildTimeConf.cmx matitaMisc.cmi
matita.cmo: predefined_virtuals.cmi matitaScript.cmi matitaInit.cmi \
matitaMisc.cmo: matitaGuiTypes.cmi buildTimeConf.cmo matitaMisc.cmi
matitaMisc.cmx: matitaGuiTypes.cmi buildTimeConf.cmx matitaMisc.cmi
matita.cmo: predefined_virtuals.cmi matitaScript.cmi matitaInit.cmi \
- matitaGui.cmi matitaGtkMisc.cmi buildTimeConf.cmo
+ matitaGui.cmi matitaGtkMisc.cmi buildTimeConf.cmo applyTransformation.cmi
matita.cmx: predefined_virtuals.cmx matitaScript.cmx matitaInit.cmx \
matita.cmx: predefined_virtuals.cmx matitaScript.cmx matitaInit.cmx \
- matitaGui.cmx matitaGtkMisc.cmx buildTimeConf.cmx
+ matitaGui.cmx matitaGtkMisc.cmx buildTimeConf.cmx applyTransformation.cmx
matitaScript.cmo: virtuals.cmi matitaTypes.cmi matitaMisc.cmi \
matitaMathView.cmi matitaGtkMisc.cmi matitaEngine.cmi cicMathView.cmi \
buildTimeConf.cmo matitaScript.cmi
matitaScript.cmo: virtuals.cmi matitaTypes.cmi matitaMisc.cmi \
matitaMathView.cmi matitaGtkMisc.cmi matitaEngine.cmi cicMathView.cmi \
buildTimeConf.cmo matitaScript.cmi
cicMathView.cmi: matitaGuiTypes.cmi applyTransformation.cmi
lablGraphviz.cmi:
matitaclean.cmi:
cicMathView.cmi: matitaGuiTypes.cmi applyTransformation.cmi
lablGraphviz.cmi:
matitaclean.cmi:
+matitaEngine.cmi: applyTransformation.cmi
matitaExcPp.cmi:
matitaGtkMisc.cmi: matitaGeneratedGui.cmo
matitaGui.cmi: matitaGuiTypes.cmi
matitaExcPp.cmi:
matitaGtkMisc.cmi: matitaGeneratedGui.cmo
matitaGui.cmi: matitaGuiTypes.cmi
-matitaGuiTypes.cmi: matitaTypes.cmi matitaGeneratedGui.cmo \
- applyTransformation.cmi
+matitaGuiTypes.cmi: matitaGeneratedGui.cmo applyTransformation.cmi
matitaInit.cmi:
matitaMathView.cmi: matitaTypes.cmi matitaGuiTypes.cmi
matitaMisc.cmi: matitaGuiTypes.cmi
matitaInit.cmi:
matitaMathView.cmi: matitaTypes.cmi matitaGuiTypes.cmi
matitaMisc.cmi: matitaGuiTypes.cmi
String.sub s lenp (lens-lenp)
;;
String.sub s lenp (lens-lenp)
;;
let indent = ref 0 in
let print_string ~right_justify s =
let ss =
match right_justify with
None -> ""
| Some (ss,len_ss) ->
let indent = ref 0 in
let print_string ~right_justify s =
let ss =
match right_justify with
None -> ""
| Some (ss,len_ss) ->
+ assert (80 - !indent - len_ss - String.length s >= 0);
String.make (80 - !indent - len_ss - String.length s) ' ' ^ ss
in
String.make (80 - !indent - len_ss - String.length s) ' ' ^ ss
in
print_string (String.make !indent ' ' ^ s ^ ss) in
fun enter ?right_justify s ->
if enter then (print_string ~right_justify s; incr indent) else (decr indent; print_string ~right_justify s)
print_string (String.make !indent ' ' ^ s ^ ss) in
fun enter ?right_justify s ->
if enter then (print_string ~right_justify s; incr indent) else (decr indent; print_string ~right_justify s)