diff options
Diffstat (limited to 'engine/evarutil.ml')
| -rw-r--r-- | engine/evarutil.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 0a5bba39b9..7c2ecca89e 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -860,7 +860,7 @@ let compare_constructor_instances evd u u' = [u] up to existential variable instantiation and equalisable universes. The term [t] is interpreted in [sigma1] while [u] is interpreted in [sigma2]. The universe constraints in [sigma2] are - assumed to be an extention of those in [sigma1]. *) + assumed to be an extension of those in [sigma1]. *) let eq_constr_univs_test sigma1 sigma2 t u = (* spiwack: mild code duplication with {!Evd.eq_constr_univs}. *) let open Evd in |