diff options
Diffstat (limited to 'library/impargs.ml')
| -rw-r--r-- | library/impargs.ml | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/library/impargs.ml b/library/impargs.ml index 63351392e..e203a594d 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -318,8 +318,7 @@ let implicits_of_global = function (*s Registration as global tables and rollback. *) -type frozen_t = bool - * implicits Spmap.t +type frozen_t = implicits Spmap.t * implicits Indmap.t * implicits Constrmap.t * implicits Spmap.t @@ -331,11 +330,10 @@ let init () = var_table := Spmap.empty let freeze () = - (!implicit_args, !constants_table, !inductives_table, + (!constants_table, !inductives_table, !constructors_table, !var_table) -let unfreeze (imps,ct,it,const,vt) = - implicit_args := imps; +let unfreeze (ct,it,const,vt) = constants_table := ct; inductives_table := it; constructors_table := const; |