diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-06-23 10:30:04 +0200 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-06-23 10:30:04 +0200 |
| commit | 4b4397e185cee54052819ad63bef3ecd56ba4512 (patch) | |
| tree | 4812511b49ee1f4ac0402e6074dfd92b69298f5f /plugins/extraction/extraction.ml | |
| parent | 7ae226092719b26f71b675d6ceb211801349bc00 (diff) | |
Fix typo.
Diffstat (limited to 'plugins/extraction/extraction.ml')
| -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. *) |