diff options
Diffstat (limited to 'plugins/funind/recdef.ml')
| -rw-r--r-- | plugins/funind/recdef.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 046c7aa43..e98ac5fb5 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -208,7 +208,7 @@ let (declare_f : Id.t -> logical_kind -> constr list -> global_reference -> glob (* Debugging mechanism *) let debug_queue = Stack.create () -let rec print_debug_queue b e = +let print_debug_queue b e = if not (Stack.is_empty debug_queue) then begin |