diff options
| author | Guillaume Melquiond | 2016-09-28 15:38:33 +0200 |
|---|---|---|
| committer | Guillaume Melquiond | 2016-10-22 11:57:58 +0200 |
| commit | 80d5779409bf33fbe5043275b96775a5f04a3b2c (patch) | |
| tree | 7e38bd03ccf57a9c24971441bfa57d0a792edfbe | |
| parent | cc2778c3310a75585c00f0eb659ddde7aee2944a (diff) | |
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).
| -rw-r--r-- | pretyping/reductionops.ml | 7 |
1 files changed, 2 insertions, 5 deletions
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) |