diff options
| author | herbelin | 2005-11-08 17:14:52 +0000 |
|---|---|---|
| committer | herbelin | 2005-11-08 17:14:52 +0000 |
| commit | 4a7555cd875b0921368737deed4a271450277a04 (patch) | |
| tree | ea296e097117b2af5606e7365111f5694d40ad9a /proofs | |
| parent | 8d94b3c7f4c51c5f78e6438b7b3e39f375ce9979 (diff) | |
Nettoyage suite à la détection par défaut des variables inutilisées par ocaml 3.09
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7538 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/evar_refiner.ml | 1 | ||||
| -rw-r--r-- | proofs/redexpr.ml | 2 | ||||
| -rw-r--r-- | proofs/tacmach.ml | 2 |
3 files changed, 2 insertions, 3 deletions
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index 3033381431..3db11ce390 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -30,7 +30,6 @@ let w_refine env ev rawc evd = let sigma,typed_c = Pretyping.understand_gen_tcc (evars_of evd) env [] (Some e_info.evar_concl) rawc in - let inst_info = {e_info with evar_body = Evar_defined typed_c } in evar_define ev typed_c (evars_reset_evd sigma evd) (* vernac command Existential *) diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 6da2c8c2fd..8e02a7b27d 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -79,7 +79,7 @@ let make_flag f = in red let is_reference c = - try let r = global_of_constr c in true with _ -> false + try let _ref = global_of_constr c in true with _ -> false let red_expr_tab = ref Stringmap.empty diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 37dc016c93..816fdf932f 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -217,7 +217,7 @@ let mutual_cofix f others gl = with_check (refiner (Prim (Cofix (f,others)))) gl let rename_bound_var_goal gls = - let { evar_hyps = sign; evar_concl = cl } as gl = sig_it gls in + let { evar_hyps = sign; evar_concl = cl } = sig_it gls in let ids = ids_of_named_context sign in convert_concl_no_check (rename_bound_var (Global.env()) ids cl) gls |