Changes | Path |
+2 -0 |
metaprl/theories/itt/core/itt_list2.mli |
+42 -0 |
metaprl/theories/itt/core/itt_struct2.ml |
+1 -0 |
metaprl/theories/itt/core/itt_struct2.mli |
+59 -1 |
metaprl/theories/itt/extensions/vector/itt_vec_bind.ml |
+3419 -3358 |
metaprl/theories/itt/extensions/vector/itt_vec_bind.prla |
+2 -0 |
metaprl/theories/itt/extensions/vector/itt_vec_list1.mli |
+3549 -3799 |
metaprl/theories/itt/extensions/vector/itt_vec_sequent_term.prla |
+16 -0 |
metaprl/theories/itt/reflection/core/itt_hoas_debruijn.ml |
+1092 -513 |
metaprl/theories/itt/reflection/core/itt_hoas_debruijn.prla |
+4 -0 |
metaprl/theories/itt/reflection/core/itt_hoas_vbind.ml |
+1 -0 |
metaprl/theories/itt/reflection/experimental/MetaprlInfo |
+27 -0 |
metaprl/theories/itt/reflection/experimental/itt_hoas_bterm_wf.ml |
+3009 -5086 |
metaprl/theories/itt/reflection/experimental/itt_hoas_bterm_wf.prla |
Copied |
metaprl/theories/itt/reflection/experimental/itt_hoas_bterm_wf.prla2 |
+16102 -0 |
metaprl/theories/itt/reflection/experimental/itt_hoas_bterm_wf.prla2 |
+34 -0 |
metaprl/theories/itt/reflection/experimental/itt_hoas_lof.ml |
+3902 -2350 |
metaprl/theories/itt/reflection/experimental/itt_hoas_lof.prla |
+41 -4 |
metaprl/theories/itt/reflection/experimental/itt_hoas_sequent.ml |
+6951 -6489 |
metaprl/theories/itt/reflection/experimental/itt_hoas_sequent.prla |
Copied |
metaprl/theories/itt/reflection/experimental/itt_hoas_sequent.prla2 |
+18812 -0 |
metaprl/theories/itt/reflection/experimental/itt_hoas_sequent.prla2 |
+66 -0 |
metaprl/theories/itt/reflection/experimental/itt_hoas_sequent_term.ml |
+5103 -5047 |
metaprl/theories/itt/reflection/experimental/itt_hoas_sequent_term.prla |
Added |
metaprl/theories/itt/reflection/experimental/itt_hoas_sequent_term_wf.ml |
Added |
metaprl/theories/itt/reflection/experimental/itt_hoas_sequent_term_wf.mli |
Added |
metaprl/theories/itt/reflection/experimental/itt_hoas_sequent_term_wf.prla |
+1 -0 |
metaprl/theories/itt/reflection/experimental/itt_hoas_theory.mlz |
+1 -1 |
metaprl/theories/poplmark/naive/pmn_core_logic.ml |