Merge PR #13455: Fix comparison of extracted array literals

Reviewed-by: ejgallego
coq · Nov 24, 2020 · b4cc5fa · b4cc5fa
2 parents 90cb2b0 + 60ed425
commit b4cc5fa
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 1 deletion.
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
@@ -399,7 +399,11 @@ let rec eq_ml_ast t1 t2 = match t1, t2 with
 | MLmagic t1, MLmagic t2 -> eq_ml_ast t1 t2
 | MLuint i1, MLuint i2 -> Uint63.equal i1 i2
 | MLfloat f1, MLfloat f2 -> Float64.equal f1 f2
-| _, _ -> false
+| MLparray (t1,def1), MLparray (t2, def2) -> Array.equal eq_ml_ast t1 t2 && eq_ml_ast def1 def2
+| (MLrel _|MLapp _|MLlam _|MLletin _|MLglob _|MLcons _
+  |MLtuple _|MLcase _|MLfix _|MLexn _|MLdummy _|MLaxiom
+  | MLmagic _| MLuint _| MLfloat _|MLparray _), _
+  -> false
 
 and eq_ml_pattern p1 p2 = match p1, p2 with
 | Pcons (gr1, p1), Pcons (gr2, p2) ->

diff --git a/test-suite/bugs/closed/bug_13453.v b/test-suite/bugs/closed/bug_13453.v
@@ -0,0 +1,6 @@
+Require Extraction.
+
+Primitive array := #array_type.
+
+Definition a : array nat := [| 0%nat | 0%nat |].
+Extraction a.