diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-05-13 22:18:16 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-05-13 22:18:16 +0000 |
| commit | 90eea6b18bd76e840a5bf364230049700575d042 (patch) | |
| tree | 34f7ec2be776115632c19e4928bf2d3f2d5fc10a /pretyping | |
| parent | e2f323f0d4e012618933d5fdb099ee44e4c0e7ac (diff) | |
Rien d'important
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4009 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/pretyping.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index cb224fac2..e4714468a 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -185,7 +185,7 @@ let make_dep_of_undep env (IndType (indf,realargs)) pj = (*************************************************************************) (* Main pretyping function *) -let pretype_ref isevars env lvar ref = +let pretype_ref isevars env ref = let c = constr_of_reference ref in make_judge c (Retyping.get_type_of env Evd.empty c) @@ -200,7 +200,7 @@ let rec pretype tycon env isevars lvar lmeta = function | RRef (loc,ref) -> inh_conv_coerce_to_tycon loc env isevars - (pretype_ref isevars env lvar ref) + (pretype_ref isevars env ref) tycon | RVar (loc, id) -> |