From bccaeb2d35db81451f8afea428820d634e78df40 Mon Sep 17 00:00:00 2001
From: pboutill
Date: Wed, 28 Nov 2012 14:48:10 +0000
Subject: Fix ocamldebug constr printer

In paterns, we do not try to put _ for params. (nb_params is found
using Global table that ocamldebug to not have)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16010 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/constrextern.ml | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

(limited to 'interp')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index ae4d54c055..34651e2cf2 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -269,6 +269,7 @@ let is_same_type c d =
 (* mapping patterns to cases_pattern_expr                                *)
 
 let add_patt_for_params ind l =
+  if !in_debugger then l else
     Util.List.addn (fst (Inductiveops.inductive_nargs ind)) (CPatAtom (Loc.ghost,None)) l
 
 let drop_implicits_in_patt cst nb_expl args =
@@ -405,7 +406,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
 	  let args = List.map (extern_cases_pattern_in_scope scopes vars) args in
 	  let p =
 	    try
-              if !in_debugger || !Flags.raw_print then raise Exit;
+              if !Flags.raw_print then raise Exit;
 	      let projs = Recordops.lookup_projections (fst cstrsp) in
 	      let rec ip projs args acc =
 		match projs with
@@ -795,7 +796,9 @@ let rec extern inctx scopes vars r =
       (sub_extern false scopes vars tm,
        (na',Option.map (fun (loc,ind,nal) ->
 	 let args = List.map (fun x -> PatVar (Loc.ghost, x)) nal in
-	 let fullargs = Notation_ops.add_patterns_for_params ind args in
+	 let fullargs =
+	   if !in_debugger then args else
+	     Notation_ops.add_patterns_for_params ind args in
 	 extern_ind_pattern_in_scope scopes vars ind fullargs
 	) x))) tml in
     let eqns = List.map (extern_eqn inctx scopes vars) eqns in
-- 
cgit v1.2.3