From c5f081f62ff2e6a4dc6c8e08d896e5e01b53f46b Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 12 Apr 2019 16:13:52 -0400 Subject: Fix around coq/coq#262 Reported as https://github.com/coq/coq/issues/9955 --- src/GENERATEDIdentifiersWithoutTypes.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/GENERATEDIdentifiersWithoutTypes.v b/src/GENERATEDIdentifiersWithoutTypes.v index 1fca4e115..a7763c0c1 100644 --- a/src/GENERATEDIdentifiersWithoutTypes.v +++ b/src/GENERATEDIdentifiersWithoutTypes.v @@ -637,7 +637,7 @@ Module Compilers. (eta_ident_cps_gen (fun idc => let ii := ident_infos_of idc in - match dep_types ii, indep_types ii with + match dep_types ii, indep_types ii return _ with (* COQBUG(https://github.com/coq/coq/issues/9955) *) | [], [] => true | _, _ => false end))) in -- cgit v1.2.3