From f9a4ca41bc1313300f5f9b9092fe24825f435706 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 1 Feb 2017 15:56:45 +0100
Subject: Replacing "cast surgery" in LetIn by a proper field (see PR #404).

This is a patch fulfilling the relevant remark of Maxime that an
explicit information at the ML type level would be better than "cast
surgery" to carry the optional type of a let-in.

There are a very few semantic changes.
- a "(x:t:=c)" in a block of binders is now written in the more
  standard way "(x:=c:t)"
- in notations, the type of a let-in is not displayed if not
  explicitly asked so.

See discussion at PR #417 for more information.
---
 intf/notation_term.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'intf/notation_term.mli')

diff --git a/intf/notation_term.mli b/intf/notation_term.mli
index 1ab9980a5c..753fa657a8 100644
--- a/intf/notation_term.mli
+++ b/intf/notation_term.mli
@@ -30,7 +30,7 @@ type notation_constr =
   | NLambda of Name.t * notation_constr * notation_constr
   | NProd of Name.t * notation_constr * notation_constr
   | NBinderList of Id.t * Id.t * notation_constr * notation_constr
-  | NLetIn of Name.t * notation_constr * notation_constr
+  | NLetIn of Name.t * notation_constr * notation_constr option * notation_constr
   | NCases of case_style * notation_constr option *
       (notation_constr * (Name.t * (inductive * Name.t list) option)) list *
       (cases_pattern list * notation_constr) list
-- 
cgit v1.2.3