diff options
Diffstat (limited to 'interp')
| -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 405d63dfe7..1162b6e153 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -915,7 +915,7 @@ let raw_cases_pattern_expr_loc = function | RCPatAtom (loc,_) -> loc | RCPatOr (loc,_) -> loc -(** {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 |