diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-05-15 03:00:04 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 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 3f99a3c7c..b57a04679 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 |