diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-04-05 17:15:26 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-04-05 17:15:26 +0000 |
| commit | 29f960a540fbdb78b74308f2ae01c1f820067f62 (patch) | |
| tree | 6ab2f58ec8a502c9de97b8968619fbf303677d18 /tactics/rewrite.ml4 | |
| parent | 9952f1a90566f4ad5ba029a082e758b9a0bc8ee4 (diff) | |
Added a function in typing.ml to solve evars of a constr w/o going back down to rawconstr
Also cleaned a bit typing.ml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12902 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/rewrite.ml4')
| -rw-r--r-- | tactics/rewrite.ml4 | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index 95b34b8d9..e08e5e9ed 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -268,7 +268,7 @@ let decompose_applied_relation env sigma c left2right = | _ -> error "The term provided is not an applied relation." in let others,(c1,c2) = split_last_two args in let ty1, ty2 = - Typing.mtype_of env eqclause.evd c1, Typing.mtype_of env eqclause.evd c2 + Typing.type_of env eqclause.evd c1, Typing.type_of env eqclause.evd c2 in if not (evd_convertible env eqclause.evd ty1 ty2) then None else @@ -352,8 +352,8 @@ let unify_eqn env sigma hypinfo t = let c1 = nf c1 and c2 = nf c2 and car = nf car and rel = nf rel and prf = nf (Clenv.clenv_value env') in - let ty1 = Typing.mtype_of env'.env env'.evd c1 - and ty2 = Typing.mtype_of env'.env env'.evd c2 + let ty1 = Typing.type_of env'.env env'.evd c1 + and ty2 = Typing.type_of env'.env env'.evd c2 in if convertible env env'.evd ty1 ty2 then ( if occur_meta prf then |