Merge branch 'trunk' into pr379

4 files changed, 39 insertions, 44 deletions

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index d92d832759..38eeda9b96 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)
-    | LocalPattern(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,13 @@ 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) ->
-      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)
-    | LocalPattern (loc,p,tyo) ->
+    | CLocalDef (na,c,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
         | None ->
@@ -382,9 +380,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 _ | LocalPattern _) :: _ as bdl ->
+      | (CLocalAssum _ | CLocalPattern _) :: _ as bdl ->
         kw n ++ pr_undelimited_binders sep pr_c bdl
       | _ -> assert false
 
@@ -395,33 +393,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
-      LocalPattern (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
-      LocalPattern (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 +448,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 +465,9 @@ let tag_var = tag Tag.variable
         match (ro : Constrexpr.recursion_order_expr) with
           | CStructRec ->
             let names_of_binder = function
-              | LocalRawAssum (nal,_,_) -> nal
-              | LocalRawDef (_,_) -> []
-              | LocalPattern _ -> 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"}"
@@ -588,7 +586,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 +596,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 ()
+            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
@@ -703,7 +702,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) ->
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
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 ->
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 2fc8bc82d1..aa422e36af 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -205,6 +205,11 @@ let print_opacity ref =
               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 []
+
+(*******************)
 (* *)
 
 let print_polymorphism ref =
@@ -258,7 +263,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