aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2019-04-12 16:13:52 -0400
committerGravatar Jason Gross <jasongross9@gmail.com>2019-04-12 20:53:24 -0400
commitc5f081f62ff2e6a4dc6c8e08d896e5e01b53f46b (patch)
tree6c2675bcbba2cfd6d69f4ee4b7659c6866e01392
parent1384a29170bbb8b166b90f73bafea8d1948568af (diff)
Fix around coq/coq#262
-rw-r--r--src/GENERATEDIdentifiersWithoutTypes.v2
1 files changed, 1 insertions, 1 deletions
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