diff options
| author | herbelin | 2000-06-01 20:51:48 +0000 |
|---|---|---|
| committer | herbelin | 2000-06-01 20:51:48 +0000 |
| commit | 08e2c28ee98c6a5d235cc9b84bc5690dd9a22666 (patch) | |
| tree | ad7198fd4aa7a08e220fe911e577d6da725aaaff /library/impargs.ml | |
| parent | 5139432d6087f49ef549d8375a1a61db56f86dd1 (diff) | |
Mise en place d'un choix constr/typed_type en remplacement de certains Cast
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@485 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/impargs.ml')
| -rw-r--r-- | library/impargs.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/library/impargs.ml b/library/impargs.ml index b334092b92..5b52f19760 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -68,7 +68,7 @@ let declare_inductive_implicits sp = let mib = Global.lookup_mind sp in let imps_one_inductive mip = (auto_implicits (body_of_type mip.mind_arity), - Array.map auto_implicits mip.mind_lc) + Array.map (fun c -> auto_implicits (body_of_type c)) mip.mind_lc) in let imps = Array.map imps_one_inductive mib.mind_packets in inductives_table := Spmap.add sp imps !inductives_table |