From a61f4371adf8e5f81866ce4e8684cafdd1dc050a Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 24 Oct 2020 13:12:40 +0200
Subject: Rewriting convoluted code of set_var_scope in constrintern.ml.

---
 interp/constrintern.ml | 17 ++++++++---------
 1 file changed, 8 insertions(+), 9 deletions(-)

(limited to 'interp')

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 *)
     ()
-- 
cgit v1.2.3