Merge branch 'permutations' into andrea

diff --cc ocaml/Makefile
index de63c63e0b3984ecc072e8ee650b49b8215572df,b56c3069aab3b9e1de417ba277f013403e2816b6..b662428199742560e9d34d61c7e7afe0fe7d859f
--- 1/ocaml/Makefile
--- 2/ocaml/Makefile
+++ b/ocaml/Makefile
@@@ -1,12 -1,21 +1,24 @@@
  OCAMLC = ocamlopt -g -rectypes
  LIB = unix.cmxa str.cmxa
- UTILS = parser.cmx console.cmx listx.cmx util.cmx pure.cmx num.cmx
+ UTILS = util.cmx console.cmx listx.cmx pure.cmx num.cmx parser.cmx
  
- all: andrea.out
+ all: a.out test4.out
+ 
+ run: test4.out
+       bash run
+ 
+ a.out: $(UTILS) lambda4.cmx problems.cmx
+       $(OCAMLC) -o a.out $(LIB) $^
+ 
+ sat.out: $(UTILS) lambda4.cmx sat.ml
+       $(OCAMLC) -o sat.out $(LIB) $^
+ #
+ test4.out: $(UTILS) lambda4.cmx test.ml
+       $(OCAMLC) -o test4.out $(LIB) $^
  
 +andrea.out: $(UTILS) andrea8.ml
 +      $(OCAMLC) -o andrea.out $(LIB) $(UTILS) andrea8.ml
 +
  %.cmi: %.mli
        $(OCAMLC) -c $<
  

diff --cc ocaml/num.mli
index f81e445fc3eeeff6f3fac13a1b53d1473b06bb81,33ea10fee01f5530e904fb10940efc77ba50d07b..39637bf1afe8c34ca409371d25b94d3e152d3542
--- 1/ocaml/num.mli
--- 2/ocaml/num.mli
+++ b/ocaml/num.mli
@@@ -24,10 -21,10 +21,9 @@@ val free_vars' : nf -> var lis
  val free_vars : nf -> int list
  module ToScott :
    sig
-     val t_of_i_num_var : nf i_num_var_ -> Pure.Pure.t
-     val t_of_nf : nf -> Pure.Pure.t
+     val scott_of_nf : nf -> Pure.Pure.t
    end
  val print : ?l:string list -> nf -> string
 -val string_of_nf : [<nf] -> string
  val cast_to_i_var : [< nf > `I `Var] -> i_var
  val cast_to_i_n_var : [< nf > `I `N `Var] -> i_n_var
  val cast_to_i_num_var : [< nf > `I `N `Match `Var] -> i_num_var