diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-08-01 16:46:43 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-08-01 16:46:43 +0200 |
| commit | a8d440fcb2a5f5768874012e72c3e092eb82eff1 (patch) | |
| tree | f5ac08f2498975917f9de01aad47b1aa66f96e4d /plugins/micromega | |
| parent | bbf3682aa80bb86502e29018465e3602f0d9bb3e (diff) | |
Compatibility for compilation with ocaml 3.12 (at least).
Diffstat (limited to 'plugins/micromega')
| -rw-r--r-- | plugins/micromega/coq_micromega.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 36eee9828..a6d2cf75c 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -1385,7 +1385,7 @@ let rcst_domain_spec = lazy { let micromega_order_change spec cert cert_typ env ff : Tacmach.tactic = - let ids = List.mapi (fun i _ -> (Names.Id.of_string ("__z"^(string_of_int i)))) env in + let ids = Util.List.map_i (fun i _ -> (Names.Id.of_string ("__z"^(string_of_int i)))) 0 env in let formula_typ = (Term.mkApp (Lazy.force coq_Cstr,[|spec.coeff|])) in let ff = dump_formula formula_typ (dump_cstr spec.coeff spec.dump_coeff) ff in let vm = dump_varmap (spec.typ) env in |