diff options
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/extraction/extraction.ml | 2 | ||||
| -rw-r--r-- | contrib/extraction/ocaml.ml | 2 |
2 files changed, 3 insertions, 1 deletions
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml index 247bd137b5..26a263942a 100644 --- a/contrib/extraction/extraction.ml +++ b/contrib/extraction/extraction.ml @@ -351,6 +351,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *) in let n = nb_default_params env mip0.mind_nf_arity in let projs = try List.map out_some projs with _ -> raise (I Standard) in + (* avoid constant projections (records fields defined with [:=]) *) let is_true_proj kn = let (_,body) = Sign.decompose_lam_assum (constant_value env kn) in match kind_of_term body with @@ -366,6 +367,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *) if type_eq (mlt_env env) Tdummy typ then l1,l2 else let r = ConstRef kn in + (* avoid dummy arguments for projectors *) if List.mem false (type_to_sign (mlt_env env) typ) then r :: l1, l2 else r :: l1, r :: l2 diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml index 0498987b32..f4daa5a7aa 100644 --- a/contrib/extraction/ocaml.ml +++ b/contrib/extraction/ocaml.ml @@ -421,8 +421,8 @@ let pp_singleton kn packet = pr_id packet.ip_consnames.(0))) let pp_record kn packet = - let l = List.combine (find_projections kn) packet.ip_types.(0) in let projs = find_projections kn in + let l = List.combine projs packet.ip_types.(0) in let pl = rename_tvars keywords packet.ip_vars in str "type " ++ pp_parameters pl ++ pp_global (IndRef (kn,0)) ++ str " = { "++ hov 0 (prlist_with_sep (fun () -> str ";" ++ spc ()) |