From 830cdec8704d14bca0b3db390ecb9661e01eb106 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 23 Feb 2020 22:18:24 +0100
Subject: Helping issue #11659 by leaving only the Cast hack in the grammar.

We clean the hack bypassing the interpretation of "'pat" in binders
and move it to comDefinition.ml. In particular, we fix the exact
subterm to which Eval has to apply in the hack, and remove the
artificial cast we had introduced.
---
 test-suite/output/PatternsInBinders.out | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/output/PatternsInBinders.out b/test-suite/output/PatternsInBinders.out
index 4f09f00c56..bdfa8afb6a 100644
--- a/test-suite/output/PatternsInBinders.out
+++ b/test-suite/output/PatternsInBinders.out
@@ -4,7 +4,7 @@ fun '(x, y) => (y, x)
      : A * B -> B * A
 forall '(x, y), swap (x, y) = (y, x)
      : Prop
-proj_informative = fun '(exist _ x _) => x : A
+proj_informative = fun '(exist _ x _) => x
      : {x : A | P x} -> A
 foo = fun '(Bar n b tt p) => if b then n + p else n - p
      : Foo -> nat
@@ -29,8 +29,7 @@ exists '(x, y) '(z, w), swap (x, y) = (z, w)
 ∀ '(x, y), swap (x, y) = (y, x)
      : Prop
 both_z = 
-fun pat : nat * nat =>
-let '(n, p) as x := pat return (F x) in (Z n, Z p) : F (n, p)
+fun pat : nat * nat => let '(n, p) as x := pat return (F x) in (Z n, Z p)
      : forall pat : nat * nat, F pat
 fun '(x, y) '(z, t) => swap (x, y) = (z, t)
      : A * B -> B * A -> Prop
-- 
cgit v1.2.3