diff options
Diffstat (limited to 'plugins/extraction/modutil.ml')
| -rw-r--r-- | plugins/extraction/modutil.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index b398bc07a0..654695c232 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -108,7 +108,7 @@ let ast_iter_references do_term do_cons do_type a = Array.iter (fun (_,p,_) -> patt_iter_references do_cons p) v | MLrel _ | MLlam _ | MLapp _ | MLletin _ | MLtuple _ | MLfix _ | MLexn _ - | MLdummy _ | MLaxiom | MLmagic _ -> () + | MLdummy _ | MLaxiom | MLmagic _ | MLuint _ -> () in iter a let ind_iter_references do_term do_cons do_type kn ind = |