diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/extraction/extract_env.ml | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 62473855aa..73062328b1 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -137,6 +137,11 @@ let check_fix env cb i = | _ -> raise Impossible) | Undef _ | OpaqueDef _ -> raise Impossible +let prec_declaration_equal (na1, ca1, ta1) (na2, ca2, ta2) = + na1 = na2 && + array_equal eq_constr ca1 ca2 && + array_equal eq_constr ta1 ta2 + let factor_fix env l cb msb = let _,recd as check = check_fix env cb 0 in let n = Array.length (let fi,_,_ = recd in fi) in @@ -149,7 +154,8 @@ let factor_fix env l cb msb = (fun j -> function | (l,SFBconst cb') -> - if check <> check_fix env cb' (j+1) then raise Impossible; + let check' = check_fix env cb' (j+1) in + if not (fst check = fst check' && prec_declaration_equal (snd check) (snd check')) then raise Impossible; labels.(j+1) <- l; | _ -> raise Impossible) msb'; labels, recd, msb'' |