diff options
| -rw-r--r-- | contrib/extraction/common.ml | 1 | ||||
| -rw-r--r-- | contrib/extraction/extraction.ml | 3 | ||||
| -rw-r--r-- | contrib/extraction/mlutil.ml | 4 | ||||
| -rw-r--r-- | contrib/extraction/modutil.ml | 2 | ||||
| -rw-r--r-- | contrib/extraction/ocaml.ml | 3 |
5 files changed, 5 insertions, 8 deletions
diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml index 359257c88..750729660 100644 --- a/contrib/extraction/common.ml +++ b/contrib/extraction/common.ml @@ -310,7 +310,6 @@ module StdParams = struct (*i TODO: clash possible i*) list_firstn ((mp_length mp)-(mp_length pref)) ls with Not_found -> (* [mp] is othogonal with every element of [mp]. *) - let base = base_mp mp in if !modular && (at_toplevel mp) then snd (list_sep_last ls) else ls diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml index 55ad52ee2..16d85a3f9 100644 --- a/contrib/extraction/extraction.ml +++ b/contrib/extraction/extraction.ml @@ -230,7 +230,7 @@ let rec extract_type env db j c args = (* We try to reduce. *) let newc = applist (Declarations.force lbody, args) in extract_type env db j newc [])) - | Ind ((kn,i) as ip) -> + | Ind (kn,i) -> let s = (extract_ind env kn).ind_packets.(i).ip_sign in extract_type_app env db (IndRef (kn,i),s) args | Case _ | Fix _ | CoFix _ -> Tunknown @@ -676,7 +676,6 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt = end else let mi = extract_ind env kn in - let params_nb = mi.ind_nparams in let oi = mi.ind_packets.(i) in let metas = Array.init (List.length oi.ip_vars) new_meta in (* The extraction of the head. *) diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml index 5c842f159..b909eead5 100644 --- a/contrib/extraction/mlutil.ml +++ b/contrib/extraction/mlutil.ml @@ -256,7 +256,7 @@ type abbrev_map = global_reference -> ml_type option let type_expand env t = let rec expand = function | Tmeta {contents = Some t} -> expand t - | Tglob (r,l) as t -> + | Tglob (r,l) -> (match env r with | Some mlt -> expand (type_subst_list l mlt) | None -> Tglob (r, List.map expand l)) @@ -378,7 +378,7 @@ let ast_iter f = function | MLapp (a,l) -> f a; List.iter f l | MLcons (_,c,l) -> List.iter f l | MLmagic a -> f a - | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLaxiom as a -> () + | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLaxiom -> () (*S Operations concerning De Bruijn indices. *) diff --git a/contrib/extraction/modutil.ml b/contrib/extraction/modutil.ml index 673c8e929..6dcfaf2a1 100644 --- a/contrib/extraction/modutil.ml +++ b/contrib/extraction/modutil.ml @@ -185,7 +185,7 @@ let ast_iter_references do_term do_cons do_type a = | MLcons (i,r,_) -> if lang () = Ocaml then record_iter_references do_term i; do_cons r - | MLcase (i,_,v) as a -> + | MLcase (i,_,v) -> if lang () = Ocaml then record_iter_references do_term i; Array.iter (fun (r,_,_) -> do_cons r) v | _ -> () diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml index f9b91d226..ee53bd49a 100644 --- a/contrib/extraction/ocaml.ml +++ b/contrib/extraction/ocaml.ml @@ -264,7 +264,6 @@ let rec pp_expr par env args = let tuple = pp_tuple (pp_expr true env []) args' in pp_par par (pp_global r ++ spc () ++ tuple) | MLcase (i, t, pv) -> - let r,_,_ = pv.(0) in let expr = if i = Coinductive then (str "Lazy.force" ++ spc () ++ pp_expr true env [] t) else @@ -480,7 +479,7 @@ let pp_mind kn i = let pp_decl mpl = local_mpl := mpl; function - | Dind (kn,i) as d -> pp_mind kn i + | Dind (kn,i) -> pp_mind kn i | Dtype (r, l, t) -> if is_inline_custom r then failwith "empty phrase" else |