diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-09-25 19:49:30 +0200 |
---|---|---|
committer | Jason Gross <jasongross9@gmail.com> | 2018-09-26 15:18:06 -0400 |
commit | 059f186db67852ac17de78dab1987aab77dd4bdb (patch) | |
tree | c3b8ca1107560023fb15536e9c0b1f173b6885bf | |
parent | 226b85c55a11e57b2b42edfb83c0b39136ed9128 (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.v | 2 |
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 |