Make constrMatching and detyping more robust with respect to

expand_projection failing if an innapropriate sigma is given.

2 files changed, 28 insertions, 18 deletions

diff --git a/pretyping/constrMatching.ml b/pretyping/constrMatching.ml
index 270d274778..ad4c678cbd 100644
--- a/pretyping/constrMatching.ml
+++ b/pretyping/constrMatching.ml
@@ -221,8 +221,9 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels pat c =
           else (* Might be a projection on the right *)
 	    match kind_of_term c2 with
 	    | Proj (pr, c) when not (Projection.unfolded pr) ->
-	      let term = Retyping.expand_projection env sigma pr c (Array.to_list args2) in
-		sorec stk env subst p term
+	      (try let term = Retyping.expand_projection env sigma pr c (Array.to_list args2) in
+		     sorec stk env subst p term
+	       with Retyping.RetypeError _ -> raise PatternMatchingFailure)
 	    | _ -> raise PatternMatchingFailure)
 	   
       | PApp (c1,arg1), App (c2,arg2) ->
@@ -236,8 +237,9 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels pat c =
 	    with Invalid_argument _ -> raise PatternMatchingFailure
 	  else raise PatternMatchingFailure
 	| _, Proj (pr,c) when not (Projection.unfolded pr) ->
-	  let term = Retyping.expand_projection env sigma pr c (Array.to_list arg2) in
-	    sorec stk env subst p term
+	  (try let term = Retyping.expand_projection env sigma pr c (Array.to_list arg2) in
+		 sorec stk env subst p term
+	   with Retyping.RetypeError _ -> raise PatternMatchingFailure)	    
 	| _, _ ->
           try Array.fold_left2 (sorec stk env) (sorec stk env subst c1 c2) arg1 arg2
           with Invalid_argument _ -> raise PatternMatchingFailure)
@@ -247,8 +249,9 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels pat c =
 	raise PatternMatchingFailure
 	
       | PApp (c, args), Proj (pr, c2) ->
-	let term = Retyping.expand_projection env sigma pr c2 [] in
-	  sorec stk env subst p term
+	(try let term = Retyping.expand_projection env sigma pr c2 [] in
+	       sorec stk env subst p term
+	 with Retyping.RetypeError _ -> raise PatternMatchingFailure)
 
       | PProj (p1,c1), Proj (p2,c2) when Projection.equal p1 p2 ->
           sorec stk env subst c1 c2
@@ -435,8 +438,10 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c =
     let next_mk_ctx le = mk_ctx (mkProj (p,List.hd le)) in
     let next () = 
       if partial_app then
-	let term = Retyping.expand_projection env sigma p c' [] in
-	  aux env term mk_ctx next
+	try 
+	  let term = Retyping.expand_projection env sigma p c' [] in
+	    aux env term mk_ctx next
+	with Retyping.RetypeError _ -> raise PatternMatchingFailure
       else
 	try_aux [env] [c'] next_mk_ctx next in
       authorized_occ env sigma partial_app closed pat c mk_ctx next
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 205c5a208b..1119293f5b 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -450,17 +450,22 @@ let rec detype flags avoid env sigma t =
       else 
 	if Projection.unfolded p then
 	  (** Print the compatibility match version *)
-	  let pb = Environ.lookup_projection p (snd env) in
-	  let body = pb.Declarations.proj_body in
-	  let ty = Retyping.get_type_of (snd env) sigma c in
-	  let (ind, args) = Inductive.find_rectype (snd env) ty in
-	  let body' = strip_lam_assum body in
-	    detype flags avoid env sigma (substl (c :: List.rev args) body')
+	  let c' = 
+	    try 
+	      let pb = Environ.lookup_projection p (snd env) in
+	      let body = pb.Declarations.proj_body in
+	      let ty = Retyping.get_type_of (snd env) sigma c in
+	      let (ind, args) = Inductiveops.find_mrectype (snd env) sigma ty in
+	      let body' = strip_lam_assum body in
+		substl (c :: List.rev args) body'
+	    with Retyping.RetypeError _ | Not_found -> 
+	      anomaly (str"Cannot detype an unfolded primitive projection.")
+	  in detype flags avoid env sigma c'
 	else
-	  let ty = Retyping.get_type_of (snd env) sigma c in
-	  let (ind, args) = Inductive.find_rectype (snd env) ty in
-	    GApp (dl, GRef (dl, ConstRef (Projection.constant p), None), 
-		  List.map (detype flags avoid env sigma) (args @ [c]))
+	  let c = 
+	    try Retyping.expand_projection (snd env) sigma p c [] 
+	    with Retyping.RetypeError _ -> anomaly (str"Cannot detype a primitive projection")
+	  in detype flags avoid env sigma c
     | Evar (evk,cl) ->
       let id,l =
         try Evd.evar_ident evk sigma,