From 30cc3ba051dba9ab256ff6c7b61f81807604fd82 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 6 Jan 2015 16:27:54 +0100
Subject: Reverting the tentative try to restore the use of second-order
 typed-based matching: it provokes a stack overflow in contrib
 ClassicalRealisability. To be investigated later on. (See
 893a02f643858ba0b0172648e77af9ccb65f03df.)

---
 pretyping/evarconv.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index f541698e98..dd1ba54003 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -1060,11 +1060,15 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
   with TypingFailed evd -> evd, false
 
 let second_order_matching_with_args ts env evd ev l t =
-  let evd,ev = evar_absorb_arguments env evd ev (Array.to_list l) in
+(*
+  let evd,ev = evar_absorb_arguments env evd ev l in
   let argoccs = Array.map_to_list (fun _ -> None) (snd ev) in
   let evd, b = second_order_matching ts env evd ev argoccs t in
   if b then Success evd
   else UnifFailure (evd, ConversionFailed (env,mkApp(mkEvar ev,l),t))
+  if b then Success evd else
+*)
+  UnifFailure (evd, ConversionFailed (env,mkApp(mkEvar ev,l),t))
 
 let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
   let t1 = apprec_nohdbeta ts env evd (whd_head_evar evd t1) in
-- 
cgit v1.2.3