aboutsummaryrefslogtreecommitdiff
path: root/kernel/safe_typing.ml
diff options
context:
space:
mode:
authorbarras2001-05-23 15:13:07 +0000
committerbarras2001-05-23 15:13:07 +0000
commitdc2e676c9cdedea43805c21a4b3203832a985f95 (patch)
tree849760ef13d1460d603ce9436c244922e13a6080 /kernel/safe_typing.ml
parenta023ff2e48aaf7ebfb15e10dc7cdb80ab2991e8e (diff)
amelioration des messages d'erreurs vis a vis des evars
ajout automatique des chemins vers les sources au moment du Drop git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1761 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/safe_typing.ml')
-rw-r--r--kernel/safe_typing.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 7df4258946..d2887cce8d 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -90,7 +90,7 @@ let rec execute env cstr cu =
(cast_rel env Evd.empty cj tj)
| IsRel n ->
- (relative env Evd.empty n, cu)
+ (relative env n, cu)
| IsVar id ->
(make_judge cstr (lookup_named_type id env), cu)