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.

1 files changed, 2 insertions, 5 deletions

diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
index 2b63ed6d6e..3b233d6ef4 100644
--- a/plugins/decl_mode/decl_interp.ml
+++ b/plugins/decl_mode/decl_interp.ml
@@ -264,7 +264,7 @@ let prod_one_id (loc,id) glob =
 	 GHole (loc,Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), glob)
 
 let let_in_one_alias (id,pat) glob =
-  GLetIn (Loc.ghost,Name id, glob_of_pat pat, glob)
+  GLetIn (Loc.ghost,Name id, glob_of_pat pat, None, glob)
 
 let rec bind_primary_aliases map pat =
   match pat with
@@ -359,10 +359,7 @@ let interp_cases info env sigma params (pat:cases_pattern_expr) hyps =
     let rids=ref ([],pat_vars) in
     let npatt= deanonymize rids patt in
       List.rev (fst !rids),npatt in
-  let term2 =
-    GLetIn(Loc.ghost,Anonymous,
-	   GCast(Loc.ghost,glob_of_pat npatt,
-		 CastConv app_ind),term1) in
+  let term2=GLetIn(Loc.ghost,Anonymous,glob_of_pat npatt,Some app_ind,term1) in
   let term3=List.fold_right let_in_one_alias aliases term2 in
   let term4=List.fold_right prod_one_id loc_ids term3 in
   let term5=List.fold_right prod_one_hyp params term4 in