vrahli
diff --git a/‎README.md
+2-2 b/‎README.md
+2-2
diff --git a/‎TODO
+1-1 b/‎TODO
+1-1
diff --git a/‎nuprl_terms/Makefile ‎nuprl_checker/Makefile b/‎nuprl_terms/Makefile ‎nuprl_checker/Makefile
diff --git a/‎nuprl_terms/NuprlAsciiLex.mll ‎nuprl_checker/NuprlAsciiLex.mll b/‎nuprl_terms/NuprlAsciiLex.mll ‎nuprl_checker/NuprlAsciiLex.mll
diff --git a/‎nuprl_terms/NuprlAsciiParse.mly ‎nuprl_checker/NuprlAsciiParse.mly b/‎nuprl_terms/NuprlAsciiParse.mly ‎nuprl_checker/NuprlAsciiParse.mly
diff --git a/‎nuprl_terms/NuprlTerms.ml ‎nuprl_checker/NuprlTerms.ml b/‎nuprl_terms/NuprlTerms.ml ‎nuprl_checker/NuprlTerms.ml
diff --git a/‎nuprl_terms/NuprlTerms.mli ‎nuprl_checker/NuprlTerms.mli b/‎nuprl_terms/NuprlTerms.mli ‎nuprl_checker/NuprlTerms.mli
diff --git a/‎nuprl_terms/Parse.ml ‎nuprl_checker/Parse.ml b/‎nuprl_terms/Parse.ml ‎nuprl_checker/Parse.ml
diff --git a/‎nuprl_terms/Parse.mli ‎nuprl_checker/Parse.mli b/‎nuprl_terms/Parse.mli ‎nuprl_checker/Parse.mli
diff --git a/‎nuprl_terms/ParserNuprlAscii.ml ‎nuprl_checker/ParserNuprlAscii.ml b/‎nuprl_terms/ParserNuprlAscii.ml ‎nuprl_checker/ParserNuprlAscii.ml
diff --git a/‎nuprl_terms/ParserNuprlAscii.mli ‎nuprl_checker/ParserNuprlAscii.mli b/‎nuprl_terms/ParserNuprlAscii.mli ‎nuprl_checker/ParserNuprlAscii.mli
diff --git a/‎nuprl_terms/README.md ‎nuprl_checker/README.md b/‎nuprl_terms/README.md ‎nuprl_checker/README.md
diff --git a/‎nuprl_terms/equal_wf_primitive.term ‎nuprl_checker/equal_wf_primitive.term b/‎nuprl_terms/equal_wf_primitive.term ‎nuprl_checker/equal_wf_primitive.term
diff --git a/‎nuprl_terms/true_wf_primitive.term ‎nuprl_checker/true_wf_primitive.term b/‎nuprl_terms/true_wf_primitive.term ‎nuprl_checker/true_wf_primitive.term
diff --git a/‎nuprl_terms/uall_wf.term-list ‎nuprl_checker/uall_wf.term-list b/‎nuprl_terms/uall_wf.term-list ‎nuprl_checker/uall_wf.term-list
diff --git a/‎nuprl_terms/uall_wf_primitive.term ‎nuprl_checker/uall_wf_primitive.term b/‎nuprl_terms/uall_wf_primitive.term ‎nuprl_checker/uall_wf_primitive.term
@@ -128,8 +128,8 @@ of a principle to recursively define choice sequences.
 * We started implemented a theorem prover backend that relies on a
 verified library of definitions and proofs.  This
 `rules/proof_with_lib_example1.v` for an example.  We can use this
-backend as a proof checker for Nuprl.  See `nuprl_terms/README.md` for
-more details.
+backend as a proof checker for Nuprl.  See `nuprl_checker/README.md`
+for more details.
 
 
 CONTRIBUTORS
 
@@ -1,5 +1,5 @@
 * I'm currently working on exporting Nuprl proofs to our Coq
-  implementation.  See nuprl_terms/README.md for more details.
+  implementation.  See nuprl_checker/README.md for more details.
 
 * [DONE] Divide cequiv/approx_star.v into several files, one for each
   non canonical operator so that they can be compiled in parallel.