diff options
| author | puech | 2011-07-29 14:29:53 +0000 |
|---|---|---|
| committer | puech | 2011-07-29 14:29:53 +0000 |
| commit | 0daf358a71aff4aded2b822fc18b7a8b49cdbd04 (patch) | |
| tree | c73925b7a8a9c21c023a3c823f493945924bc10d /plugins | |
| parent | fed48031aad31420f5ffae4b26b0324390191504 (diff) | |
Extract_env: generic = on prec_declaration replaced by prec_declaration_equal
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14369 85f007b7-540e-0410-9357-904b9bb8a0f7
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'' |