From 26f228a4b15c270212bd2b33419400ef7d08f92a Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 5 Sep 2017 15:55:30 +0200
Subject: Glob_ops.fix_kind_eq: fix typo

---
 pretyping/glob_ops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping/glob_ops.ml')

diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index ba193da60d..988bdae033 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -112,7 +112,7 @@ let fix_kind_eq f k1 k2 = match k1, k2 with
     let eq (i1, o1) (i2, o2) =
       Option.equal Int.equal i1 i2 && fix_recursion_order_eq f o1 o2
     in
-    Int.equal i1 i2 && Array.equal eq a1 a1
+    Int.equal i1 i2 && Array.equal eq a1 a2
   | GCoFix i1, GCoFix i2 -> Int.equal i1 i2
   | (GFix _ | GCoFix _), _ -> false
 
-- 
cgit v1.2.3


From f50c823eb90af7088e2efec9e2c462dcacd12613 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 5 Sep 2017 15:57:13 +0200
Subject: Glob_ops.rename_glob_vars: fix typo

---
 pretyping/glob_ops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping/glob_ops.ml')

diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 988bdae033..4dfa789ba5 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -452,7 +452,7 @@ let rec rename_glob_vars l c = force @@ DAst.map_with_loc (fun ?loc -> function
       else r
   | GProd (na,bk,t,c) ->
       let na',l' = update_subst na l in
-      GProd (na,bk,rename_glob_vars l t,rename_glob_vars l' c)
+      GProd (na',bk,rename_glob_vars l t,rename_glob_vars l' c)
   | GLambda (na,bk,t,c) ->
       let na',l' = update_subst na l in
       GLambda (na',bk,rename_glob_vars l t,rename_glob_vars l' c)
-- 
cgit v1.2.3