diff options
| author | jforest | 2006-05-23 15:29:49 +0000 |
|---|---|---|
| committer | jforest | 2006-05-23 15:29:49 +0000 |
| commit | bab93b9eda03f1ca13e7ff2a0b83bf43eea1874b (patch) | |
| tree | a3c9a5b3bb40abefa7ebad0b878ddbbb0c5c9b27 | |
| parent | 29e1c97ab17b852f1eba69dc1d9463f59930eef2 (diff) | |
Correcting a bug with ocaml <= 3.08.3 (Map.fold changing)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8849 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | contrib/funind/functional_principles_proofs.ml | 18 |
1 files changed, 14 insertions, 4 deletions
diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml index a8ecdfd0e6..06f8673d06 100644 --- a/contrib/funind/functional_principles_proofs.ml +++ b/contrib/funind/functional_principles_proofs.ml @@ -233,12 +233,22 @@ let change_eq env sigma hyp_id (context:Sign.rel_context) x t end_of_type = in let sub = compute_substitution Intmap.empty t1 t2 in let end_of_type_with_pop = pop end_of_type in (*the equation will be removed *) - let new_end_of_type = - Intmap.fold - (fun i t end_of_type -> lift 1 (substnl [t] (i-1) end_of_type)) - sub + let new_end_of_type = + (* Ugly hack to prevent Map.fold order change between ocaml-3.08.3 and ocaml-3.08.4 + Can be safely replaced by the next comment for Ocaml >= 3.08.4 + *) + let sub' = Intmap.fold (fun i t acc = (i,t)::acc) sub [] in + let sub'' = List.sort (fun (x,_) (y,_) -> Pervasives.compare x y) sub' in + List.fold_left (fun end_of_type (i,t) -> lift 1 (substnl [t] (i-1) end_of_type)) end_of_type_with_pop + sub in + (* let new_end_of_type = *) + (* Intmap.fold *) + (* (fun i t end_of_type -> lift 1 (substnl [t] (i-1) end_of_type)) *) + (* sub *) + (* end_of_type_with_pop *) + (* in *) let old_context_length = List.length context + 1 in let witness_fun = mkLetIn(Anonymous,make_refl_eq t1_typ t1,t, |