From 405acea72a67c31ec8554c1f76d51518a5df769a 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(-)

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 4ccbc81b47..332d4e0b26 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -166,9 +166,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
@@ -177,9 +174,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