In substitutions, lazyly refresh the codomain of the univar map

This map is allowed to do name capture and is hence sensitive to bound variables renaming.
EasyCrypt · Dec 5, 2023 · 7c0adea · 7c0adea
1 parent dd02a37
commit 7c0adea
Showing 1 changed file with 9 additions and 2 deletions.
diff --git a/src/ecTypes.ml b/src/ecTypes.ml
@@ -214,8 +214,15 @@ let rec ty_subst s =
             | Some ty -> ty_subst s ty
           end
         end
-      | Tunivar id    -> Muid.find_def ty id s.ts_u
-      | Tvar id       -> Mid.find_def ty id s.ts_v
+      | Tunivar id -> begin
+          match Muid.find_opt id s.ts_u with
+          | None ->
+            ty
+          | Some ty ->
+            ty_subst s ty
+        end
+
+      | Tvar id -> Mid.find_def ty id s.ts_v
       | _ -> ty_map (ty_subst s) ty
 
 (* -------------------------------------------------------------------- *)