diff options
| author |  aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-07-07 14:56:02 +0000 |
|---|---|---|
| committer | aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-07-07 14:56:02 +0000 |
| commit | cd2cec34d3508e147a636a040321ac73f3273011 (patch) | |
| tree | c004d879593c5eb22bb91e9af2515e7c8bea746d /tactics/rewrite.ml4 | |
| parent | 8c1884146772bdcf505f9efe820c440bafe75acf (diff) | |
Jolification : tentative de supprimer les "( evd)" et associés qui
traînaient un peu partout dans le code depuis la fusion d'evar_map et
evar_defs. Début du travail d'uniformisation des noms donnés aux
evar_defs à travers le code.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12224 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/rewrite.ml4')
| -rw-r--r-- | tactics/rewrite.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index ed873ce76..6da110139 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -150,7 +150,7 @@ let is_applied_setoid_relation t = else (try let evd, evar = Evarutil.new_evar Evd.empty (Global.env()) (new_Type ()) in let inst = mkApp (Lazy.force setoid_relation, [| evar; c |]) in - ignore(Typeclasses.resolve_one_typeclass (Global.env()) ( evd) inst); + ignore(Typeclasses.resolve_one_typeclass (Global.env()) evd inst); true with _ -> false) | _ -> false @@ -339,7 +339,7 @@ let unify_eqn env sigma hypinfo t = in let evd' = Typeclasses.resolve_typeclasses ~fail:true env'.env env'.evd in let env' = { env' with evd = evd' } in - let nf c = Evarutil.nf_evar ( evd') (Clenv.clenv_nf_meta env' c) in + let nf c = Evarutil.nf_evar evd' (Clenv.clenv_nf_meta env' c) in let c1 = nf c1 and c2 = nf c2 and car = nf car and rel = nf rel and prf = nf (Clenv.clenv_value env') in |