diff --git a/README.md b/README.md index cad3bbf..868a65d 100644 --- a/README.md +++ b/README.md @@ -106,7 +106,7 @@ Il faudra ensuite placer l'automate comme constellation de référence et l'éto } ``` -### Construire des preuves de la logique linéaire multiplicatives +### Construire des preuves de la logique linéaire multiplicative Il est recommandé de suivre la construction proposée dans mon manuscrit de thèse. On traduit chaque axiome par une étoile binaire contenant la traduction des atomes associés. diff --git a/main.ml b/main.ml index e32472b..7cc2e19 100644 --- a/main.ml +++ b/main.ml @@ -43,16 +43,6 @@ let commands_list () = tab 2 ^ "Allow equations X=X which yields trivial loops (default setting)" ) - (* print_endline ( - "load as " ^ - tab 1 ^ - "Stores a constellation defined in as in the environement" - ); - print_endline ( - "store as " ^ - tab 1 ^ - "Stores a constellation defined in as in the environement" - ) *) let prompt () = print_string "> " @@ -110,11 +100,6 @@ let _ = let result = intexec ~withloops:!withloops cs in print_endline (string_of_constellation result) with _ -> print_endline "Syntax error. Please try again.") - (* | ["load"; filename; "as"; x] -> - let fchannel = open_in filename in - let lexbuf = Lexing.from_channel fchannel in - let cs = constc Lexer.read lexbuf in - env := (x, cs) :: (!env) *) | ["intmode"; "-f"; filename] -> (try let lexbuf = Lexing.from_channel (open_in filename) in