From 9b27bd598d56f6560b56653dd1346889a9a06d40 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 30 Sep 2020 15:20:49 +0200
Subject: Fix retyping anomaly in rewrite

Fix #13045

Also make sure future anomalies won't be fed to tclzero.

Instead of retyping with lax:true we may question why we produce an
ill-typed term in decompose_app_rel: in the

    | App (f, [|arg|]) ->

case we produce `fun x y : T => bla x y` but we have no assurance that
the second argument of `bla` should have type `T`.
---
 plugins/ltac/rewrite.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index a1dbf9a439..75517818cb 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -498,7 +498,7 @@ let rec decompose_app_rel env evd t =
 
 let decompose_app_rel env evd t =
   let (rel, t1, t2) = decompose_app_rel env evd t in
-  let ty = Retyping.get_type_of env evd rel in
+  let ty = try Retyping.get_type_of ~lax:true env evd rel with Retyping.RetypeError _ -> error_no_relation () in
   let () = if not (Reductionops.is_arity env evd ty) then error_no_relation () in
   (rel, t1, t2)
 
@@ -2144,7 +2144,7 @@ let setoid_proof ty fn fallback =
           let car = snd (List.hd (fst (Reductionops.splay_prod env sigma t))) in
             (try init_relation_classes () with _ -> raise Not_found);
             fn env sigma car rel
-        with e ->
+        with e when CErrors.noncritical e ->
           (* XXX what is the right test here as to whether e can be converted ? *)
           let e, info = Exninfo.capture e in
           Proofview.tclZERO ~info e
-- 
cgit v1.2.3