diff options
| -rw-r--r-- | contrib/extraction/extraction.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml index 401e4f98f3..ba925b40b5 100644 --- a/contrib/extraction/extraction.ml +++ b/contrib/extraction/extraction.ml @@ -30,7 +30,7 @@ open Mlutil exception I of inductive_info -(* A flag used to avoid loop in extract_inductive *) +(* A flag used to avoid loops in [extract_inductive] *) let internal_call = ref (None : kernel_name option) let none = Evd.empty |