diff options
| author | Hugo Herbelin | 2015-01-06 16:27:54 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-01-07 18:40:44 +0100 |
| commit | 30cc3ba051dba9ab256ff6c7b61f81807604fd82 (patch) | |
| tree | 5ada2e8d38703691fe46ab5db6fbe510d1a87e84 | |
| parent | b185f9917a8b6fcea775925147f24839f81288a7 (diff) | |
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.)
| -rw-r--r-- | pretyping/evarconv.ml | 6 |
1 files changed, 5 insertions, 1 deletions
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 |