ViewVC logotype

Revision 3086

Jump to revision: Previous Next
Author: nogin
Date: Sun Oct 22 20:58:58 2000 UTC (20 years, 9 months ago)
Changed paths: 11
Log Message:
1) Proved some *Formation rules that used to be primitive (using in part
Alexei's cut rule idea). We should probably continue this job and
eliminate "primitiveness" from as much Formation rules as we can.

2) unitSqequal rule should be primitive

3) mk: don't pass -j1 to make when MAKE_JOBS = 1

4) In MP toploop, when a non-negatice integer is found where
an address was expected, that integer is considered to be
the hypothesis number. This enables applying primitive rules
from the MP toploop.

Changed paths

Path Details
Directorymetaprl/mk/preface modified , text changed
Directorymetaprl/refiner/refsig/term_man_sig.ml modified , text changed
Directorymetaprl/refiner/term_ds/term_man_ds.ml modified , text changed
Directorymetaprl/refiner/term_gen/term_man_gen.ml modified , text changed
Directorymetaprl/theories/itt/itt_list.ml modified , text changed
Directorymetaprl/theories/itt/itt_list.prla modified , text changed
Directorymetaprl/theories/itt/itt_unit.ml modified , text changed
Directorymetaprl/theories/itt/itt_unit.prla added
Directorymetaprl/theories/itt/itt_void.ml modified , text changed
Directorymetaprl/theories/itt/itt_void.prla modified , text changed
Directorymetaprl/theories/tactic/mptop.ml modified , text changed

  ViewVC Help
Powered by ViewVC 1.1.26