diff options
| author | Hugo Herbelin | 2017-05-15 03:00:04 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-05-15 03:00:04 +0200 |
| commit | a05cdcb00edbf0e35190f2d724c4a8c46d6cf9a3 (patch) | |
| tree | 013dba5a8777625fe8debf7fcb4e01d07ad49297 | |
| parent | e3550a0acc39e235e01a727267b12a7c06f23b2c (diff) | |
Typo in comments of constrintern.
| -rw-r--r-- | interp/constrintern.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 3f99a3c7c0..b57a046796 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -900,7 +900,7 @@ let interp_reference vars r = (**********************************************************************) (** {5 Cases } *) -(** {6 Elemtary bricks } *) +(** {6 Elementary bricks } *) let apply_scope_env env = function | [] -> {env with tmp_scope = None}, [] | sc::scl -> {env with tmp_scope = sc}, scl |