equal
deleted
inserted
replaced
51 and search_bound = ref 20 (*unification quits above this depth*) |
51 and search_bound = ref 20 (*unification quits above this depth*) |
52 and trace_simp = ref false (*print dpairs before calling SIMPL*) |
52 and trace_simp = ref false (*print dpairs before calling SIMPL*) |
53 and trace_types = ref false (*announce potential incompleteness |
53 and trace_types = ref false (*announce potential incompleteness |
54 of type unification*) |
54 of type unification*) |
55 |
55 |
56 val sgr = ref(Sign.pure); |
56 val sgr = ref(Sign.proto_pure); |
57 |
57 |
58 type binderlist = (string*typ) list; |
58 type binderlist = (string*typ) list; |
59 |
59 |
60 type dpair = binderlist * term * term; |
60 type dpair = binderlist * term * term; |
61 |
61 |