From d91a0c27402f0f19a30147bb9d87387ca2a91fd0 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 2 Feb 2017 10:18:48 +0100
Subject: "Standardizing" the name LocalPatten into LocalRawPattern.

---
 ide/texmacspp.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'ide')

diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml
index 6fbed38fb4..7bbf393ac9 100644
--- a/ide/texmacspp.ml
+++ b/ide/texmacspp.ml
@@ -235,7 +235,7 @@ and pp_local_binder lb = (* don't know what it is for now *)
       let ppl =
         List.map (fun (loc, nam) -> (xmlCst (string_of_name nam) loc)) namll in
       xmlTyped (ppl @ [pp_expr ce])
-  | LocalPattern _ ->
+  | LocalRawPattern _ ->
       assert false
 and pp_local_decl_expr lde = (* don't know what it is for now *)
   match lde with
-- 
cgit v1.2.3


From 648ce5e08f7245f2a775abd1304783c4167e9f2e Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 2 Feb 2017 18:24:58 +0100
Subject: Unifying standard "constr_level" names for constructors of
 local_binder_expr.

RawLocal -> CLocal
---
 ide/texmacspp.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'ide')

diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml
index 7bbf393ac9..e705e4e5a1 100644
--- a/ide/texmacspp.ml
+++ b/ide/texmacspp.ml
@@ -228,14 +228,14 @@ and pp_decl_notation ((_, s), ce, sc) = (* don't know what it is for now *)
   Element ("decl_notation", ["name", s], [pp_expr ce])
 and pp_local_binder lb = (* don't know what it is for now *)
   match lb with
-  | LocalRawDef ((_, nam), ce) ->
+  | CLocalDef ((_, nam), ce) ->
       let attrs = ["name", string_of_name nam] in
       pp_expr ~attr:attrs ce
-  | LocalRawAssum (namll, _, ce) ->
+  | CLocalAssum (namll, _, ce) ->
       let ppl =
         List.map (fun (loc, nam) -> (xmlCst (string_of_name nam) loc)) namll in
       xmlTyped (ppl @ [pp_expr ce])
-  | LocalRawPattern _ ->
+  | CLocalPattern _ ->
       assert false
 and pp_local_decl_expr lde = (* don't know what it is for now *)
   match lde with
-- 
cgit v1.2.3


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.
---
 ide/texmacspp.ml | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

(limited to 'ide')

diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml
index e705e4e5a1..e787e48bf1 100644
--- a/ide/texmacspp.ml
+++ b/ide/texmacspp.ml
@@ -15,6 +15,7 @@ open Bigint
 open Decl_kinds
 open Extend
 open Libnames
+open Constrexpr_ops
 
 let unlock loc =
   let start, stop = Loc.unloc loc in
@@ -228,9 +229,10 @@ and pp_decl_notation ((_, s), ce, sc) = (* don't know what it is for now *)
   Element ("decl_notation", ["name", s], [pp_expr ce])
 and pp_local_binder lb = (* don't know what it is for now *)
   match lb with
-  | CLocalDef ((_, nam), ce) ->
+  | CLocalDef ((loc, nam), ce, ty) ->
       let attrs = ["name", string_of_name nam] in
-      pp_expr ~attr:attrs ce
+      let value = match ty with Some t -> CCast (Loc.merge (constr_loc ce) (constr_loc t),ce, CastConv t) | None -> ce in
+      pp_expr ~attr:attrs value
   | CLocalAssum (namll, _, ce) ->
       let ppl =
         List.map (fun (loc, nam) -> (xmlCst (string_of_name nam) loc)) namll in
@@ -465,7 +467,8 @@ and pp_expr ?(attr=[]) e =
            [Element ("scrutinees", [], List.map pp_case_expr cel)] @
            [pp_branch_expr_list bel]))
   | CRecord (_, _) -> assert false
-  | CLetIn (loc, (varloc, var), value, body) ->
+  | CLetIn (loc, (varloc, var), value, typ, body) ->
+      let value = match typ with Some t -> CCast (Loc.merge (constr_loc value) (constr_loc t),value, CastConv t) | None -> value in
       xmlApply loc
         (xmlOperator "let" loc ::
          [xmlCst (string_of_name var) varloc; pp_expr value; pp_expr body])
-- 
cgit v1.2.3