aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2018-09-25 19:49:30 +0200
committerGravatar Jason Gross <jasongross9@gmail.com>2018-09-26 15:18:06 -0400
commit059f186db67852ac17de78dab1987aab77dd4bdb (patch)
treec3b8ca1107560023fb15536e9c0b1f173b6885bf
parent226b85c55a11e57b2b42edfb83c0b39136ed9128 (diff)
Compatibility after Coq PR#262 (continued).
This is a second instance of incompatibility induced by PR#262 (see 251ea49a). One fixes it the same, reducing the search space for a return clause by forbidding it to be obtained by small inversion.
-rw-r--r--src/Experiments/NewPipeline/CStringification.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Experiments/NewPipeline/CStringification.v b/src/Experiments/NewPipeline/CStringification.v
index f107a3ddd..3aebb2ec3 100644
--- a/src/Experiments/NewPipeline/CStringification.v
+++ b/src/Experiments/NewPipeline/CStringification.v
@@ -1239,7 +1239,7 @@ Module Compilers.
| type.arrow (type.base s) d
=> fun f
(x : (int.option.interp s -> ErrT (arith_expr_for_base s)))
- => match x int.option.None with
+ => match x int.option.None return _ with
| inl x'
=> @collect_args_and_apply_unknown_casts
d