aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2002-10-12 14:28:58 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2002-10-12 14:28:58 +0000
commit72fb50ce5d3e802aadff66495a0e90065f2fab42 (patch)
tree37845f12bca4327b0cf0251c2696babe791fed70 /library
parent4d89c31ff0a60e93e2a301f32d1e02f035eafaa2 (diff)
Nettoyage
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3116 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library')
-rw-r--r--library/impargs.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/library/impargs.ml b/library/impargs.ml
index 14a93123b..86535370a 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -250,7 +250,7 @@ let var_table = ref Idmap.empty
let compute_var_implicits id =
let env = Global.env () in
let (_,_,ty) = lookup_named id env in
- auto_implicits env (body_of_type ty)
+ auto_implicits env ty
let cache_var_implicits (_,(id,imps)) =
var_table := Idmap.add id imps !var_table