Use auxiliary function for externing record patterns.

Also apply the same conditions for printing constructors as record
instances in both terms and patterns.

2 files changed, 35 insertions, 21 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 7f5f03610b..c68a60fc93 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -403,6 +403,36 @@ let pattern_printable_in_both_syntax (ind,_ as c) =
       (List.for_all is_status_implicit params)&&(List.for_all (fun x -> not (is_status_implicit x)) args)
   ) impl_st
 
+let extern_record_pattern cstrsp args =
+  try
+    if !Flags.raw_print then raise Exit;
+    let projs = Recordops.lookup_projections (fst cstrsp) in
+    if PrintingRecord.active (fst cstrsp) then
+      ()
+    else if PrintingConstructor.active (fst cstrsp) then
+      raise Exit
+    else if not (get_record_print ()) then
+      raise Exit;
+    let rec ip projs args acc =
+      match projs, args with
+      | [], [] -> acc
+      | proj :: q, pat :: tail ->
+        let acc =
+          match proj, pat with
+          | _, { CAst.v = CPatAtom None } ->
+            (* we don't want to have 'x := _' in our patterns *)
+            acc
+          | Some c, _ ->
+            let loc = pat.CAst.loc in
+            (extern_reference ?loc Id.Set.empty (GlobRef.ConstRef c), pat) :: acc
+          | _ -> raise No_match in
+        ip q tail acc
+      | _ -> assert false
+    in
+    Some (List.rev (ip projs args []))
+  with
+    Not_found | No_match | Exit -> None
+
  (* Better to use extern_glob_constr composed with injection/retraction ?? *)
 let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat =
   try
@@ -437,27 +467,9 @@ let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat =
         | PatCstr(cstrsp,args,na) ->
           let args = List.map (extern_cases_pattern_in_scope allscopes vars) args in
           let p =
-            try
-              if !Flags.raw_print then raise Exit;
-              let projs = Recordops.lookup_projections (fst cstrsp) in
-              let rec ip projs args acc =
-                match projs, args with
-                  | [], [] -> acc
-                  | proj :: q, pat :: tail ->
-                     let acc =
-                       match proj, pat with
-                       | _, { CAst.v = CPatAtom None } ->
-                          (* we don't want to have 'x := _' in our patterns *)
-                          acc
-                       | Some c, _ ->
-                          ((extern_reference ?loc Id.Set.empty (GlobRef.ConstRef c), pat) :: acc)
-                       | _ -> raise No_match in
-                     ip q tail acc
-                  | _ -> assert false
-              in
-              CPatRecord(List.rev (ip projs args []))
-            with
-                Not_found | No_match | Exit ->
+            match extern_record_pattern cstrsp args with
+            | Some l -> CPatRecord l
+            | None ->
                   let c = extern_reference Id.Set.empty (GlobRef.ConstructRef cstrsp) in
                   if Constrintern.get_asymmetric_patterns () then
                     if pattern_printable_in_both_syntax cstrsp
diff --git a/test-suite/output/Record.v b/test-suite/output/Record.v
index d9a649fadc..71a8afa131 100644
--- a/test-suite/output/Record.v
+++ b/test-suite/output/Record.v
@@ -20,6 +20,8 @@ Check {| field := 5 |}.
 Check build_r 5.
 Check build_c 5.
 
+Set Printing Records.
+
 Record N := C { T : Type; _ : True }.
 Check fun x:N => let 'C _ p := x in p.
 Check fun x:N => let 'C T _ := x in T.