1 files changed, 25 insertions, 34 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index f6da10c961..d254520e0e 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -288,17 +288,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
-    | { loc; v = PatCstr(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
-      CAst.make ?loc @@ CPatCstr (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
@@ -307,7 +298,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
 	insert_pat_alias ?loc (insert_pat_delimiters ?loc (CAst.make ?loc @@ CPatPrim 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 ->
@@ -321,21 +312,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
-
-
-
-
-
-	| { CAst.v = 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
+		       | _, { CAst.v = 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(List.rev (ip projs args []))
 	    with
@@ -663,9 +652,11 @@ let rec extern inctx scopes vars r =
   | GEvar (n,l) ->
       extern_evar n (List.map (on_snd (extern false scopes vars)) l)
 
-  | GPatVar (b,n) ->
+  | GPatVar kind ->
       if !print_meta_as_hole then CHole (None, Misctypes.IntroAnonymous, None) else
-        if b then CPatVar n else CEvar (n,[])
+       (match kind with
+         | Evar_kinds.SecondOrderPatVar n -> CPatVar n
+         | Evar_kinds.FirstOrderPatVar n -> CEvar (n,[]))
 
   | GApp (f,args) ->
       (match f with
@@ -698,7 +689,7 @@ let rec extern inctx scopes vars r =
 		     | None :: q -> raise No_match
 		     | Some c :: q ->
 		         match locs with
-			   | [] -> anomaly (Pp.str "projections corruption [Constrextern.extern]")
+			   | [] -> anomaly (Pp.str "projections corruption [Constrextern.extern].")
 			   | (_, false) :: locs' ->
 			       (* we don't want to print locals *)
 			       ip q locs' args acc
@@ -1033,17 +1024,17 @@ let rec glob_of_pat env sigma pat = CAst.make @@ match pat with
       let id = try match lookup_name_of_rel n env with
 	| Name id   -> id
 	| Anonymous ->
-	    anomaly ~label:"glob_constr_of_pattern" (Pp.str "index to an anonymous variable")
+	    anomaly ~label:"glob_constr_of_pattern" (Pp.str "index to an anonymous variable.")
       with Not_found -> Id.of_string ("_UNBOUND_REL_"^(string_of_int n)) in
       GVar id
   | PMeta None -> GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous,None)
-  | PMeta (Some n) -> GPatVar (false,n)
+  | PMeta (Some n) -> GPatVar (Evar_kinds.FirstOrderPatVar n)
   | PProj (p,c) -> GApp (CAst.make @@ GRef (ConstRef (Projection.constant p),None),
 			 [glob_of_pat env sigma c])
   | PApp (f,args) ->
       GApp (glob_of_pat env sigma f,Array.map_to_list (glob_of_pat env sigma) args)
   | PSoApp (n,args) ->
-      GApp (CAst.make @@ GPatVar (true,n),
+      GApp (CAst.make @@ GPatVar (Evar_kinds.SecondOrderPatVar n),
         List.map (glob_of_pat env sigma) args)
   | PProd (na,t,c) ->
       GProd (na,Explicit,glob_of_pat env sigma t,glob_of_pat (na::env) sigma c)
@@ -1064,7 +1055,7 @@ let rec glob_of_pat env sigma pat = CAst.make @@ match pat with
 	| _, Some ind ->
 	  let bl' = List.map (fun (i,n,c) -> (i,n,glob_of_pat env sigma c)) bl in
 	  simple_cases_matrix_of_branches ind bl'
-	| _, None -> anomaly (Pp.str "PCase with some branches but unknown inductive")
+	| _, None -> anomaly (Pp.str "PCase with some branches but unknown inductive.")
       in
       let mat = if info.cip_extensible then mat @ [any_any_branch] else mat
       in
@@ -1072,7 +1063,7 @@ let rec glob_of_pat env sigma pat = CAst.make @@ match pat with
 	| PMeta None, _, _ -> (Anonymous,None),None
 	| _, Some ind, Some nargs ->
 	  return_type_of_predicate ind nargs (glob_of_pat env sigma p)
-	| _ -> anomaly (Pp.str "PCase with non-trivial predicate but unknown inductive")
+	| _ -> anomaly (Pp.str "PCase with non-trivial predicate but unknown inductive.")
       in
       GCases (RegularStyle,rtn,[glob_of_pat env sigma tm,indnames],mat)
   | PFix f -> (Detyping.detype_names false [] env (Global.env()) sigma (EConstr.of_constr (mkFix f))).v (** FIXME bad env *)