From 80d5779409bf33fbe5043275b96775a5f04a3b2c Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Wed, 28 Sep 2016 15:38:33 +0200
Subject: Remove incorrect assertion in cbn (bug #4822).

This assertion checked that two arguments in the same position were equal,
but in fact, since one might have already been reduced, they are only
convertible (which is too costly to check in an assertion).
---
 pretyping/reductionops.ml | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

(limited to 'pretyping/reductionops.ml')

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 7c7b31395e..9e654d29a1 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -153,9 +153,6 @@ module Cst_stack = struct
   let empty = []
   let is_empty = CList.is_empty
 
-  let sanity x y =
-    assert(Term.eq_constr x y)
-
   let drop_useless = function
     | _ :: ((_,_,[])::_ as q) -> q
     | l -> l
@@ -164,9 +161,9 @@ module Cst_stack = struct
     let append2cst = function
       | (c,params,[]) -> (c, h::params, [])
       | (c,params,((i,t)::q)) when i = pred (Array.length t) ->
-	 let () = sanity h t.(i) in (c, params, q)
+	(c, params, q)
       | (c,params,(i,t)::q) ->
-	let () = sanity h t.(i) in (c, params, (succ i,t)::q)
+	(c, params, (succ i,t)::q)
     in
       drop_useless (List.map append2cst cst_l)
 
-- 
cgit v1.2.3