From: acondolu <andrea.condoluci@unibo.it>
Date: Tue, 25 Jul 2017 09:21:38 +0000 (+0200)
Subject: Merge branch 'permutations' into andrea
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4c157f176c89dcb5633d60c5be8a444ae0529c29;p=fireball-separation.git

Merge branch 'permutations' into andrea
---

4c157f176c89dcb5633d60c5be8a444ae0529c29
diff --cc ocaml/Makefile
index de63c63,b56c306..b662428
--- a/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 f81e445,33ea10f..39637bf
--- a/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