aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/extraction
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-06-27 20:47:43 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-06-27 20:47:43 +0200
commit663a8647bbc32e11243091de80f9953ed5fb7eff (patch)
tree7fba0a308daee7586221f752e233dd8fa9c8f5f5 /plugins/extraction
parentd4725f692a5f202ca4c5d6341b586b0e377f6973 (diff)
parenta7ea32fbf3829d1ce39ce9cc24b71791727090c5 (diff)
Merge branch 'v8.5'
Diffstat (limited to 'plugins/extraction')
-rw-r--r--plugins/extraction/extraction.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index e40621965..0153348de 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. *)