Coq: track changes elsewhere

- more hex_bits functions, add decimal_string_of_bits
- extra tuple unfolding in constructors
- note that variables can be redundant wildcard clauses
- update RISC-V patch

2 files changed, 11 insertions, 1 deletions

diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 45efa798..655e12e2 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -689,6 +689,7 @@ let rec doc_pat ctxt apat_needed exists_as_pairs (P_aux (p,(l,annot)) as pat, ty
            to persuade the type checker to output these somehow. *)
        let (typq, ctor_typ) = Env.get_val_spec id env in
        let untuple (Typ_aux (typ_aux, _) as typ) = match typ_aux with
+         | Typ_tup [Typ_aux (Typ_tup typs,_)] -> typs
          | Typ_tup typs -> typs
          | _ -> [typ]
        in
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 99b96f61..9c26e69a 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -4282,7 +4282,9 @@ let make_cstr_mappings env ids m =
     (fun id ->
       let _,ty = Env.get_val_spec id env in
       let args = match ty with
-        | Typ_aux (Typ_fn (Typ_aux (Typ_tup tys,_),_,_),_) -> List.map (fun _ -> RP_any) tys
+        | Typ_aux (Typ_fn (Typ_aux (Typ_tup [Typ_aux (Typ_tup tys,_)],_),_,_),_)
+        | Typ_aux (Typ_fn (Typ_aux (Typ_tup tys,_),_,_),_)
+          -> List.map (fun _ -> RP_any) tys
         | _ -> [RP_any]
       in RP_app (id,args)) ids in
   let rec aux ids acc l =
@@ -4431,8 +4433,15 @@ let check_cases process is_wild loc_of cases =
   let cases, rps = aux [RP_any] [] cases in
   List.rev cases, rps
 
+let not_enum env id =
+  match Env.lookup_id id env with
+  | Enum _ -> false
+  | _ -> true
+
 let pexp_is_wild = function
   | (Pat_aux (Pat_exp (P_aux (P_wild,_),_),_)) -> true
+  | (Pat_aux (Pat_exp (P_aux (P_id id,ann),_),_))
+       when not_enum (env_of_annot ann) id -> true
   | _ -> false
 
 let pexp_loc = function