diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/declaremods.ml | 2 | ||||
| -rw-r--r-- | library/impargs.ml | 2 | ||||
| -rw-r--r-- | library/nametab.ml | 8 |
3 files changed, 5 insertions, 7 deletions
diff --git a/library/declaremods.ml b/library/declaremods.ml index 4d8a65651..a61e59d6d 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -1043,7 +1043,7 @@ let iter_all_segments f = List.iter apply_obj objects) !modtab_objects in - let rec apply_node = function + let apply_node = function | sp, Leaf o -> f sp o | _ -> () in diff --git a/library/impargs.ml b/library/impargs.ml index 30a402302..a7d4bcbfb 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -695,7 +695,7 @@ let rec select_impargs_size n = function | (LessArgsThan p, impls)::l -> if n <= p then impls else select_impargs_size n l -let rec select_stronger_impargs = function +let select_stronger_impargs = function | [] -> [] (* Tolerance for (DefaultImpArgs,[]) *) | (_,impls)::_ -> impls diff --git a/library/nametab.ml b/library/nametab.ml index cae6e7278..0aac3873a 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -505,8 +505,8 @@ let global_inductive r = (********************************************************************) (* Registration of tables as a global table and rollback *) -type frozen = ccitab * dirtab * kntab * kntab - * globrevtab * mprevtab * knrevtab * knrevtab +type frozen = ccitab * dirtab * mptab * kntab + * globrevtab * mprevtab * mptrevtab * knrevtab let init () = the_ccitab := SpTab.empty; @@ -518,9 +518,7 @@ let init () = the_modtyperevtab := MPmap.empty; the_tacticrevtab := KNmap.empty - - -let freeze () = +let freeze () : frozen = !the_ccitab, !the_dirtab, !the_modtypetab, |