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.

---
 printing/ppconstr.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'printing')

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index d92d832759..2c2f32209c 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -319,7 +319,7 @@ let tag_var = tag Tag.variable
   let begin_of_binder = function
   LocalRawDef((loc,_),_) -> fst (Loc.unloc loc)
     | LocalRawAssum((loc,_)::_,_,_) -> fst (Loc.unloc loc)
-    | LocalPattern(loc,_,_) -> fst (Loc.unloc loc)
+    | LocalRawPattern(loc,_,_) -> fst (Loc.unloc loc)
     | _ -> assert false
 
   let begin_of_binders = function
@@ -368,7 +368,7 @@ let tag_var = tag Tag.variable
         | _ -> c, CHole (Loc.ghost, None, Misctypes.IntroAnonymous, None) in
       surround (pr_lname na ++ pr_opt_type pr_c topt ++
                   str":=" ++ cut() ++ pr_c c)
-    | LocalPattern (loc,p,tyo) ->
+    | LocalRawPattern (loc,p,tyo) ->
       let p = pr_patt lsimplepatt p in
       match tyo with
         | None ->
@@ -384,7 +384,7 @@ let tag_var = tag Tag.variable
     match bl with
       | [LocalRawAssum (nal,k,t)] ->
         kw n ++ pr_binder false pr_c (nal,k,t)
-      | (LocalRawAssum _ | LocalPattern _) :: _ as bdl ->
+      | (LocalRawAssum _ | LocalRawPattern _) :: _ as bdl ->
         kw n ++ pr_undelimited_binders sep pr_c bdl
       | _ -> assert false
 
@@ -402,7 +402,7 @@ let tag_var = tag Tag.variable
               CCases (_,LetPatternStyle,None, [CRef (Ident (_,id'),None),None,None],[(_,[_,[p]],b)]))
          when Id.equal id id' && not (Id.Set.mem id (Topconstr.free_vars_of_constr_expr b)) ->
       let bl,c = extract_prod_binders b in
-      LocalPattern (loc,p,None) :: bl, c
+      LocalRawPattern (loc,p,None) :: bl, c
     | CProdN (loc,(nal,bk,t)::bl,c) ->
       let bl,c = extract_prod_binders (CProdN(loc,bl,c)) in
       LocalRawAssum (nal,bk,t) :: bl, c
@@ -418,7 +418,7 @@ let tag_var = tag Tag.variable
                 CCases (_,LetPatternStyle,None, [CRef (Ident (_,id'),None),None,None],[(_,[_,[p]],b)]))
          when Id.equal id id' && not (Id.Set.mem id (Topconstr.free_vars_of_constr_expr b)) ->
       let bl,c = extract_lam_binders b in
-      LocalPattern (loc,p,None) :: bl, c
+      LocalRawPattern (loc,p,None) :: bl, c
     | CLambdaN (loc,(nal,bk,t)::bl,c) ->
       let bl,c = extract_lam_binders (CLambdaN(loc,bl,c)) in
       LocalRawAssum (nal,bk,t) :: bl, c
@@ -469,7 +469,7 @@ let tag_var = tag Tag.variable
             let names_of_binder = function
               | LocalRawAssum (nal,_,_) -> nal
               | LocalRawDef (_,_) -> []
-              | LocalPattern _ -> assert false
+              | LocalRawPattern _ -> assert false
             in let ids = List.flatten (List.map names_of_binder bl) in
                if List.length ids > 1 then
                  spc() ++ str "{" ++ keyword "struct" ++ spc () ++ pr_id id ++ str"}"
-- 
cgit v1.2.3


From 4e4fb7bd42364fd623f8e0e0d3007cd79d78764b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 2 Feb 2017 18:21:51 +0100
Subject: Renaming local_binder into local_binder_expr.

This is a bit long, but it is to keep a symmetry with constr_expr.
---
 printing/ppconstr.mli | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'printing')

diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli
index a0106837ad..f92caf426e 100644
--- a/printing/ppconstr.mli
+++ b/printing/ppconstr.mli
@@ -19,12 +19,12 @@ open Names
 open Misctypes
 
 val extract_lam_binders :
-  constr_expr -> local_binder list * constr_expr
+  constr_expr -> local_binder_expr list * constr_expr
 val extract_prod_binders :
-  constr_expr -> local_binder list * constr_expr
+  constr_expr -> local_binder_expr list * constr_expr
 val split_fix :
   int -> constr_expr -> constr_expr ->
-  local_binder list *  constr_expr * constr_expr
+  local_binder_expr list *  constr_expr * constr_expr
 
 val prec_less : int -> int * Ppextend.parenRelation -> bool
 
@@ -50,12 +50,12 @@ val pr_patvar : patvar -> std_ppcmds
 val pr_glob_level : glob_level -> std_ppcmds
 val pr_glob_sort : glob_sort -> std_ppcmds
 val pr_guard_annot : (constr_expr -> std_ppcmds) ->
-  local_binder list ->
+  local_binder_expr list ->
   ('a * Names.Id.t) option * recursion_order_expr ->
   std_ppcmds
 
 val pr_record_body : (reference * constr_expr) list -> std_ppcmds
-val pr_binders : local_binder list -> std_ppcmds
+val pr_binders : local_binder_expr list -> std_ppcmds
 val pr_constr_pattern_expr : constr_pattern_expr -> std_ppcmds
 val pr_lconstr_pattern_expr : constr_pattern_expr -> std_ppcmds
 val pr_constr_expr : constr_expr -> std_ppcmds
-- 
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
---
 printing/ppconstr.ml | 36 ++++++++++++++++++------------------
 1 file changed, 18 insertions(+), 18 deletions(-)

(limited to 'printing')

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 2c2f32209c..d895693cc9 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -317,9 +317,9 @@ let tag_var = tag Tag.variable
             pr_sep_com spc (pr ltop) rhs))
 
   let begin_of_binder = function
-  LocalRawDef((loc,_),_) -> fst (Loc.unloc loc)
-    | LocalRawAssum((loc,_)::_,_,_) -> fst (Loc.unloc loc)
-    | LocalRawPattern(loc,_,_) -> fst (Loc.unloc loc)
+  CLocalDef((loc,_),_) -> fst (Loc.unloc loc)
+    | CLocalAssum((loc,_)::_,_,_) -> fst (Loc.unloc loc)
+    | CLocalPattern(loc,_,_) -> fst (Loc.unloc loc)
     | _ -> assert false
 
   let begin_of_binders = function
@@ -360,15 +360,15 @@ let tag_var = tag Tag.variable
             hov 1 (if many then surround_impl b s else surround_implicit b s)
 
   let pr_binder_among_many pr_c = function
-    | LocalRawAssum (nal,k,t) ->
+    | CLocalAssum (nal,k,t) ->
       pr_binder true pr_c (nal,k,t)
-    | LocalRawDef (na,c) ->
+    | CLocalDef (na,c) ->
       let c,topt = match c with
         | CCast(_,c, (CastConv t|CastVM t|CastNative t)) -> c, t
         | _ -> c, CHole (Loc.ghost, None, Misctypes.IntroAnonymous, None) in
       surround (pr_lname na ++ pr_opt_type pr_c topt ++
                   str":=" ++ cut() ++ pr_c c)
-    | LocalRawPattern (loc,p,tyo) ->
+    | CLocalPattern (loc,p,tyo) ->
       let p = pr_patt lsimplepatt p in
       match tyo with
         | None ->
@@ -382,9 +382,9 @@ let tag_var = tag Tag.variable
   let pr_delimited_binders kw sep pr_c bl =
     let n = begin_of_binders bl in
     match bl with
-      | [LocalRawAssum (nal,k,t)] ->
+      | [CLocalAssum (nal,k,t)] ->
         kw n ++ pr_binder false pr_c (nal,k,t)
-      | (LocalRawAssum _ | LocalRawPattern _) :: _ as bdl ->
+      | (CLocalAssum _ | CLocalPattern _) :: _ as bdl ->
         kw n ++ pr_undelimited_binders sep pr_c bdl
       | _ -> assert false
 
@@ -395,33 +395,33 @@ let tag_var = tag Tag.variable
   let rec extract_prod_binders = function
   (*  | CLetIn (loc,na,b,c) as x ->
       let bl,c = extract_prod_binders c in
-      if bl = [] then [], x else LocalRawDef (na,b) :: bl, c*)
+      if bl = [] then [], x else CLocalDef (na,b) :: bl, c*)
     | CProdN (loc,[],c) ->
       extract_prod_binders c
     | CProdN (loc,[[_,Name id],bk,t],
               CCases (_,LetPatternStyle,None, [CRef (Ident (_,id'),None),None,None],[(_,[_,[p]],b)]))
          when Id.equal id id' && not (Id.Set.mem id (Topconstr.free_vars_of_constr_expr b)) ->
       let bl,c = extract_prod_binders b in
-      LocalRawPattern (loc,p,None) :: bl, c
+      CLocalPattern (loc,p,None) :: bl, c
     | CProdN (loc,(nal,bk,t)::bl,c) ->
       let bl,c = extract_prod_binders (CProdN(loc,bl,c)) in
-      LocalRawAssum (nal,bk,t) :: bl, c
+      CLocalAssum (nal,bk,t) :: bl, c
     | c -> [], c
 
   let rec extract_lam_binders = function
   (*  | CLetIn (loc,na,b,c) as x ->
       let bl,c = extract_lam_binders c in
-      if bl = [] then [], x else LocalRawDef (na,b) :: bl, c*)
+      if bl = [] then [], x else CLocalDef (na,b) :: bl, c*)
     | CLambdaN (loc,[],c) ->
       extract_lam_binders c
     | CLambdaN (loc,[[_,Name id],bk,t],
                 CCases (_,LetPatternStyle,None, [CRef (Ident (_,id'),None),None,None],[(_,[_,[p]],b)]))
          when Id.equal id id' && not (Id.Set.mem id (Topconstr.free_vars_of_constr_expr b)) ->
       let bl,c = extract_lam_binders b in
-      LocalRawPattern (loc,p,None) :: bl, c
+      CLocalPattern (loc,p,None) :: bl, c
     | CLambdaN (loc,(nal,bk,t)::bl,c) ->
       let bl,c = extract_lam_binders (CLambdaN(loc,bl,c)) in
-      LocalRawAssum (nal,bk,t) :: bl, c
+      CLocalAssum (nal,bk,t) :: bl, c
     | c -> [], c
 
   let split_lambda = function
@@ -450,7 +450,7 @@ let tag_var = tag Tag.variable
       let (na,_,def) = split_lambda def in
       let (na,t,typ) = split_product na typ in
       let (bl,typ,def) = split_fix (n-1) typ def in
-      (LocalRawAssum ([na],default_binder_kind,t)::bl,typ,def)
+      (CLocalAssum ([na],default_binder_kind,t)::bl,typ,def)
 
   let pr_recursive_decl pr pr_dangling dangling_with_for id bl annot t c =
     let pr_body =
@@ -467,9 +467,9 @@ let tag_var = tag Tag.variable
         match (ro : Constrexpr.recursion_order_expr) with
           | CStructRec ->
             let names_of_binder = function
-              | LocalRawAssum (nal,_,_) -> nal
-              | LocalRawDef (_,_) -> []
-              | LocalRawPattern _ -> assert false
+              | CLocalAssum (nal,_,_) -> nal
+              | CLocalDef (_,_) -> []
+              | CLocalPattern _ -> assert false
             in let ids = List.flatten (List.map names_of_binder bl) in
                if List.length ids > 1 then
                  spc() ++ str "{" ++ keyword "struct" ++ spc () ++ pr_id id ++ str"}"
-- 
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.
---
 printing/ppconstr.ml | 18 ++++++++----------
 1 file changed, 8 insertions(+), 10 deletions(-)

(limited to 'printing')

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index d895693cc9..0013d49a1b 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -317,7 +317,7 @@ let tag_var = tag Tag.variable
             pr_sep_com spc (pr ltop) rhs))
 
   let begin_of_binder = function
-  CLocalDef((loc,_),_) -> fst (Loc.unloc loc)
+    | CLocalDef((loc,_),_,_) -> fst (Loc.unloc loc)
     | CLocalAssum((loc,_)::_,_,_) -> fst (Loc.unloc loc)
     | CLocalPattern(loc,_,_) -> fst (Loc.unloc loc)
     | _ -> assert false
@@ -362,12 +362,9 @@ let tag_var = tag Tag.variable
   let pr_binder_among_many pr_c = function
     | CLocalAssum (nal,k,t) ->
       pr_binder true pr_c (nal,k,t)
-    | CLocalDef (na,c) ->
-      let c,topt = match c with
-        | CCast(_,c, (CastConv t|CastVM t|CastNative t)) -> c, t
-        | _ -> c, CHole (Loc.ghost, None, Misctypes.IntroAnonymous, None) in
-      surround (pr_lname na ++ pr_opt_type pr_c topt ++
-                  str":=" ++ cut() ++ pr_c c)
+    | CLocalDef (na,c,topt) ->
+      surround (pr_lname na ++ str":=" ++ cut() ++ pr_c c ++
+                pr_opt_no_spc (fun t -> cut () ++ str ":" ++ pr_c t) topt)
     | CLocalPattern (loc,p,tyo) ->
       let p = pr_patt lsimplepatt p in
       match tyo with
@@ -468,7 +465,7 @@ let tag_var = tag Tag.variable
           | CStructRec ->
             let names_of_binder = function
               | CLocalAssum (nal,_,_) -> nal
-              | CLocalDef (_,_) -> []
+              | CLocalDef (_,_,_) -> []
               | CLocalPattern _ -> assert false
             in let ids = List.flatten (List.map names_of_binder bl) in
                if List.length ids > 1 then
@@ -588,7 +585,7 @@ let tag_var = tag Tag.variable
               pr_fun_sep ++ pr spc ltop a),
           llambda
         )
-      | CLetIn (_,(_,Name x),(CFix(_,(_,x'),[_])|CCoFix(_,(_,x'),[_]) as fx), b)
+      | CLetIn (_,(_,Name x),(CFix(_,(_,x'),[_])|CCoFix(_,(_,x'),[_]) as fx), t, b)
           when Id.equal x x' ->
         return (
           hv 0 (
@@ -598,11 +595,12 @@ let tag_var = tag Tag.variable
               pr spc ltop b),
           lletin
         )
-      | CLetIn (_,x,a,b) ->
+      | CLetIn (_,x,a,t,b) ->
         return (
           hv 0 (
             hov 2 (keyword "let" ++ spc () ++ pr_lname x ++ str " :="
                    ++ pr spc ltop a ++ spc ()
+                   ++ pr_opt_no_spc (fun t -> str ":" ++ ws 1 ++ pr mt ltop t ++ spc ()) t
                    ++ keyword "in") ++
               pr spc ltop b),
           lletin
-- 
cgit v1.2.3


From eec5145a5c6575d04b5ab442597fb52913daed29 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 4 Feb 2017 14:56:04 +0100
Subject: Applying same convention as in Definition for printing type in a let
 in.

Also adding spaces around ":=" and ":" when printed as "(x : t := c)".
Example:

Check fun y => let x : True := I in fun z => z+y=0.
(* λ (y : nat) (x : True := I) (z : nat), z + y = 0
     : nat → nat → Prop *)
---
 printing/ppconstr.ml | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

(limited to 'printing')

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 0013d49a1b..f36c8c1530 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -363,8 +363,9 @@ let tag_var = tag Tag.variable
     | CLocalAssum (nal,k,t) ->
       pr_binder true pr_c (nal,k,t)
     | CLocalDef (na,c,topt) ->
-      surround (pr_lname na ++ str":=" ++ cut() ++ pr_c c ++
-                pr_opt_no_spc (fun t -> cut () ++ str ":" ++ pr_c t) topt)
+      surround (pr_lname na ++
+                pr_opt_no_spc (fun t -> str " :" ++ ws 1 ++ pr_c t) topt ++
+                str" :=" ++ spc() ++ pr_c c)
     | CLocalPattern (loc,p,tyo) ->
       let p = pr_patt lsimplepatt p in
       match tyo with
@@ -598,9 +599,9 @@ let tag_var = tag Tag.variable
       | CLetIn (_,x,a,t,b) ->
         return (
           hv 0 (
-            hov 2 (keyword "let" ++ spc () ++ pr_lname x ++ str " :="
-                   ++ pr spc ltop a ++ spc ()
-                   ++ pr_opt_no_spc (fun t -> str ":" ++ ws 1 ++ pr mt ltop t ++ spc ()) t
+            hov 2 (keyword "let" ++ spc () ++ pr_lname x
+                   ++ pr_opt_no_spc (fun t -> str " :" ++ ws 1 ++ pr mt ltop t) t
+                   ++ str " :=" ++ pr spc ltop a ++ spc ()
                    ++ keyword "in") ++
               pr spc ltop b),
           lletin
-- 
cgit v1.2.3


From 584a832d4f681d34c7cbdd87d9ceb7a742b39959 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 22 Feb 2017 00:23:10 +0100
Subject: [stm] Remove some obsolete vernacs/classification.

This is the good parts of PR #360.

IIUC, these vernacular were meant mostly for debugging and they are
not supposed to be of any use these days.

Back and join are still there not to break the testing infrastructure,
but some day they should go away.
---
 printing/ppvernac.ml | 10 ----------
 1 file changed, 10 deletions(-)

(limited to 'printing')

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 78ef4d4bad..cfc2e48d11 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -534,18 +534,8 @@ open Decl_kinds
       (* Stm *)
       | VernacStm JoinDocument ->
         return (keyword "Stm JoinDocument")
-      | VernacStm PrintDag ->
-        return (keyword "Stm PrintDag")
-      | VernacStm Finish ->
-        return (keyword "Stm Finish")
       | VernacStm Wait ->
         return (keyword "Stm Wait")
-      | VernacStm (Observe id) ->
-        return (keyword "Stm Observe " ++ str(Stateid.to_string id))
-      | VernacStm (Command v) ->
-        return (keyword "Stm Command " ++ pr_vernac_body v)
-      | VernacStm (PGLast v) ->
-        return (keyword "Stm PGLast " ++ pr_vernac_body v)
 
       (* Proof management *)
       | VernacAbortAll ->
-- 
cgit v1.2.3


From 27ce382bcfefafa5efae3bc734e8c4c235fe0261 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 27 Mar 2017 23:17:50 +0200
Subject: Do so that "About" tells if a reference is a coercion.

---
 printing/prettyp.ml | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'printing')

diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 8fabb70536..5963d45ef9 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -203,6 +203,11 @@ let print_opacity ref =
           | TransparentMaybeOpacified Conv_oracle.Expand ->
               str "transparent (with minimal expansion weight)"]
 
+(*******************)
+
+let print_if_is_coercion ref =
+  if Classops.coercion_exists ref then [pr_global ref ++ str " is a coercion"] else []
+
 (*******************)
 (* *)
 
@@ -257,7 +262,8 @@ let print_name_infos ref =
   type_info_for_implicit @
   print_renames_list (mt()) renames @
   print_impargs_list (mt()) impls @
-  print_argument_scopes (mt()) scopes
+  print_argument_scopes (mt()) scopes @
+  print_if_is_coercion ref
 
 let print_id_args_data test pr id l =
   if List.exists test l then
-- 
cgit v1.2.3


From 3fe764dd8d6578adddb01b02bafc7f31d9cb776c Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Sun, 2 Apr 2017 11:20:21 +0200
Subject: Fix higher-order pattern variables not being printed as "@?" (bug
 #5431).

---
 printing/ppconstr.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'printing')

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index d92d832759..7f5adbfe49 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -703,7 +703,7 @@ let tag_var = tag Tag.variable
       | CEvar (_,n,l) ->
         return (pr_evar (pr mt) n l, latom)
       | CPatVar (_,p) ->
-        return (str "?" ++ pr_patvar p, latom)
+        return (str "@?" ++ pr_patvar p, latom)
       | CSort (_,s) ->
         return (pr_glob_sort s, latom)
       | CCast (_,a,b) ->
-- 
cgit v1.2.3