From 495bccc436cfe72af9955b4b9d8564a8831850b9 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 16 Feb 2017 23:23:53 +0100
Subject: Fixing #4499 (not using unnamed record field in {| |} notation).

---
 interp/constrextern.ml | 23 +++++++++++++----------
 1 file changed, 13 insertions(+), 10 deletions(-)

(limited to 'interp/constrextern.ml')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index dd8a48b85e..0ba056a878 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -307,16 +307,19 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
               if !Flags.raw_print then raise Exit;
 	      let projs = Recordops.lookup_projections (fst cstrsp) in
 	      let rec ip projs args acc =
-		match projs with
-		  | [] -> acc
-		  | None :: q -> ip q args acc
-		  | Some c :: q ->
-		    match args with
-		      | [] -> raise No_match
-		      | CPatAtom(_, None) :: tail -> ip q tail acc
-		    (* we don't want to have 'x = _' in our patterns *)
-		      | head :: tail -> ip q tail
-		        ((extern_reference loc Id.Set.empty (ConstRef c), head) :: acc)
+		match projs, args with
+		  | [], [] -> acc
+		  | proj :: q, pat :: tail ->
+                     let acc =
+                       match proj, pat with
+		       | _, CPatAtom(_, None) ->
+		          (* we don't want to have 'x := _' in our patterns *)
+                          acc
+		       | Some c, _ ->
+		          ((extern_reference loc Id.Set.empty (ConstRef c), pat) :: acc)
+                       | _ -> raise No_match in
+                     ip q tail acc
+	          | _ -> assert false
 	      in
 	      CPatRecord(loc, List.rev (ip projs args []))
 	    with
-- 
cgit v1.2.3


From f7cf2bccd813994e3cd98e97fe9c1c8b5cbde3cf Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 16 Feb 2017 23:59:04 +0100
Subject: Better support for printing constructors with let-ins.

This allows e.g. to use the record notations even when there are
defined fields.

A priori fixed also missing parameters when interpreting primitive
tokens.
---
 interp/constrextern.ml | 13 ++-----------
 1 file changed, 2 insertions(+), 11 deletions(-)

(limited to 'interp/constrextern.ml')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 0ba056a878..74504e36d4 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -274,17 +274,8 @@ let pattern_printable_in_both_syntax (ind,_ as c) =
 
  (* Better to use extern_glob_constr composed with injection/retraction ?? *)
 let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
-  (* pboutill: There are letins in pat which is incompatible with notations and
-     not explicit application. *)
-  match pat with
-    | PatCstr(loc,cstrsp,args,na)
-	when !Flags.in_debugger||Inductiveops.constructor_has_local_defs cstrsp ->
-      let c = extern_reference loc Id.Set.empty (ConstructRef cstrsp) in
-      let args = List.map (extern_cases_pattern_in_scope scopes vars) args in
-      CPatCstr (loc, c, Some (add_patt_for_params (fst cstrsp) args), [])
-    | _ ->
   try
-    if !Flags.raw_print || !print_no_symbol then raise No_match;
+    if !Flags.in_debugger || !Flags.raw_print || !print_no_symbol then raise No_match;
     let (na,sc,p) = uninterp_prim_token_cases_pattern pat in
     match availability_of_prim_token p sc scopes with
       | None -> raise No_match
@@ -293,7 +284,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
 	insert_pat_alias loc (insert_pat_delimiters loc (CPatPrim(loc,p)) key) na
   with No_match ->
     try
-      if !Flags.raw_print || !print_no_symbol then raise No_match;
+      if !Flags.in_debugger || !Flags.raw_print || !print_no_symbol then raise No_match;
       extern_notation_pattern scopes vars pat
 	(uninterp_cases_pattern_notations pat)
     with No_match ->
-- 
cgit v1.2.3