Can now typecheck register declarations and assignments

Can now properly typecheck register declarations and assignments. Also
better support for assignments to mutable variables. Assignment to
immutable let bound variables is disallowed as it should be, and casts
when assiging to existing bound variables should be handled properly.

Added additional tests for these new features, and a new option
-just_check that allows the new checker to be run without the old.

1 files changed, 1 insertions, 0 deletions

diff --git a/src/process_file.mli b/src/process_file.mli
index bfc719cc..4c703dd2 100644
--- a/src/process_file.mli
+++ b/src/process_file.mli
@@ -49,6 +49,7 @@ val rewrite_ast_lem : Type_internal.tannot Ast.defs -> Type_internal.tannot Ast.
 val rewrite_ast_ocaml : Type_internal.tannot Ast.defs -> Type_internal.tannot Ast.defs
 
 val opt_new_typecheck : bool ref
+val opt_just_check : bool ref
                                                                               
 type out_type =
   | Lem_ast_out