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.

4 files changed, 6 insertions, 6 deletions

diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli
index d1b5697d75..49bafadc8e 100644
--- a/intf/constrexpr.mli
+++ b/intf/constrexpr.mli
@@ -72,7 +72,7 @@ and constr_expr =
   | CCoFix of Loc.t * Id.t located * cofix_expr list
   | CProdN of Loc.t * binder_expr list * constr_expr
   | CLambdaN of Loc.t * binder_expr list * constr_expr
-  | CLetIn of Loc.t * Name.t located * constr_expr * constr_expr
+  | CLetIn of Loc.t * Name.t located * constr_expr * constr_expr option * constr_expr
   | CAppExpl of Loc.t * (proj_flag * reference * instance_expr option) * constr_expr list
   | CApp of Loc.t * (proj_flag * constr_expr) *
       (constr_expr * explicitation located option) list
@@ -124,7 +124,7 @@ and recursion_order_expr =
 (** Anonymous defs allowed ?? *)
 and local_binder_expr =
   | CLocalAssum of Name.t located list * binder_kind * constr_expr
-  | CLocalDef of Name.t located * constr_expr
+  | CLocalDef of Name.t located * constr_expr * constr_expr option
   | CLocalPattern of Loc.t * cases_pattern_expr * constr_expr option
 
 and constr_notation_substitution =
diff --git a/intf/glob_term.mli b/intf/glob_term.mli
index ce862cf8a7..ced5a8b44f 100644
--- a/intf/glob_term.mli
+++ b/intf/glob_term.mli
@@ -42,7 +42,7 @@ type glob_constr =
   | GApp of Loc.t * glob_constr * glob_constr list
   | GLambda of Loc.t * Name.t * binding_kind *  glob_constr * glob_constr
   | GProd of Loc.t * Name.t * binding_kind * glob_constr * glob_constr
-  | GLetIn of Loc.t * Name.t * glob_constr * glob_constr
+  | GLetIn of Loc.t * Name.t * glob_constr * glob_constr option * glob_constr
   | GCases of Loc.t * case_style * glob_constr option * tomatch_tuples * cases_clauses
       (** [GCases(l,style,r,tur,cc)] = "match 'tur' return 'r' with 'cc'" (in [MatchStyle]) *)
   | GLetTuple of Loc.t * Name.t list * (Name.t * glob_constr option) *
@@ -80,7 +80,7 @@ and cases_clauses = cases_clause list
 
 type extended_glob_local_binder =
   | GLocalAssum of Loc.t * Name.t * binding_kind * glob_constr
-  | GLocalDef of Loc.t * Name.t * binding_kind * glob_constr * glob_constr
+  | GLocalDef of Loc.t * Name.t * binding_kind * glob_constr * glob_constr option
   | GLocalPattern of Loc.t * (cases_pattern * Id.t list) * Id.t * binding_kind * glob_constr
 
 (** A globalised term together with a closure representing the value
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
diff --git a/intf/pattern.mli b/intf/pattern.mli
index 329ae837e1..a32e7e4b94 100644
--- a/intf/pattern.mli
+++ b/intf/pattern.mli
@@ -68,7 +68,7 @@ type constr_pattern =
   | PProj of projection * constr_pattern
   | PLambda of Name.t * constr_pattern * constr_pattern
   | PProd of Name.t * constr_pattern * constr_pattern
-  | PLetIn of Name.t * constr_pattern * constr_pattern
+  | PLetIn of Name.t * constr_pattern * constr_pattern option * constr_pattern
   | PSort of glob_sort
   | PMeta of patvar option
   | PIf of constr_pattern * constr_pattern * constr_pattern