Suppression argument pattern_source du case_info (code jamais utilisé)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9707 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 3 insertions, 3 deletions

diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml
index e53dad265..990ee115f 100644
--- a/contrib/subtac/subtac_pretyping_F.ml
+++ b/contrib/subtac/subtac_pretyping_F.ml
@@ -397,7 +397,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 		     let f = it_mkLambda_or_LetIn fj.uj_val fsign in
 		     let v =
 		       let mis,_ = dest_ind_family indf in
-		       let ci = make_default_case_info env LetStyle mis in
+		       let ci = make_case_info env mis LetStyle in
 			 mkCase (ci, p, cj.uj_val,[|f|]) in 
 		       { uj_val = v; uj_type = substl (realargs@[cj.uj_val]) ccl }
 
@@ -415,7 +415,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 		     let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in
 		     let v =
 		       let mis,_ = dest_ind_family indf in
-		       let ci = make_default_case_info env LetStyle mis in
+		       let ci = make_case_info env mis LetStyle in
 			 mkCase (ci, p, cj.uj_val,[|f|] ) 
 		     in
 		       { uj_val = v; uj_type = ccl })
@@ -485,7 +485,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	  let b2 = f cstrs.(1) b2 in
 	  let v =
 	    let mis,_ = dest_ind_family indf in
-	    let ci = make_default_case_info env IfStyle mis in
+	    let ci = make_case_info env mis IfStyle in
 	      mkCase (ci, pred, cj.uj_val, [|b1;b2|])
 	  in
 	    { uj_val = v; uj_type = p }