diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-09-28 15:38:33 +0200 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-09-28 15:38:47 +0200 |
| commit | 405acea72a67c31ec8554c1f76d51518a5df769a (patch) | |
| tree | 074fce4630bd752f59a32c2edeb76c0023eb6ab5 /pretyping | |
| parent | 2c4f3c2bcf93d023b53a9f2ec6b151d4df696c84 (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).
Diffstat (limited to 'pretyping')
| -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 4ccbc81b4..332d4e0b2 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) |