diff options
| author | Hugo Herbelin | 2020-10-24 13:12:40 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-11-20 19:39:17 +0100 |
| commit | a61f4371adf8e5f81866ce4e8684cafdd1dc050a (patch) | |
| tree | c69af6b21a12ba65d00803c3559e2ad623fcaee3 | |
| parent | 6479926c576a1ab6aaa2f0524407f4383fcc1838 (diff) | |
Rewriting convoluted code of set_var_scope in constrintern.ml.
| -rw-r--r-- | interp/constrintern.ml | 17 |
1 files changed, 8 insertions, 9 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index c7ed066f7e..b13225d91f 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -298,21 +298,20 @@ let error_expect_binder_notation_type ?loc id = let set_var_scope ?loc id istermvar (tmp_scope,subscopes as scopes) ntnvars = try let used_as_binder,idscopes,typ = Id.Map.find id ntnvars in - if not istermvar then used_as_binder := true; - let () = if istermvar then + if istermvar then begin (* scopes have no effect on the interpretation of identifiers *) - begin match !idscopes with + (match !idscopes with | None -> idscopes := Some scopes | Some (tmp_scope', subscopes') -> let s' = make_current_scope tmp_scope' subscopes' in let s = make_current_scope tmp_scope subscopes in - if not (List.equal String.equal s' s) then error_inconsistent_scope ?loc id s' s + if not (List.equal String.equal s' s) then error_inconsistent_scope ?loc id s' s); + (match typ with + | Notation_term.NtnInternTypeOnlyBinder -> error_expect_binder_notation_type ?loc id + | Notation_term.NtnInternTypeAny -> ()) end - in - match typ with - | Notation_term.NtnInternTypeOnlyBinder -> - if istermvar then error_expect_binder_notation_type ?loc id - | Notation_term.NtnInternTypeAny -> () + else + used_as_binder := true with Not_found -> (* Not in a notation *) () |