diff options
| -rw-r--r-- | plugins/extraction/extraction.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 0ac8e3c4c..114c5149f 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -36,7 +36,7 @@ let current_fixpoints = ref ([] : constant list) let none = Evd.empty (* NB: In OCaml, [type_of] and [get_of] might raise - [SingletonInductiveBecomeProp]. this exception will be catched + [SingletonInductiveBecomeProp]. This exception will be caught in late wrappers around the exported functions of this file, in order to display the location of the issue. *) |