diff options
| author | barras | 2001-05-23 15:13:07 +0000 |
|---|---|---|
| committer | barras | 2001-05-23 15:13:07 +0000 |
| commit | dc2e676c9cdedea43805c21a4b3203832a985f95 (patch) | |
| tree | 849760ef13d1460d603ce9436c244922e13a6080 /kernel/indtypes.ml | |
| parent | a023ff2e48aaf7ebfb15e10dc7cdb80ab2991e8e (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/indtypes.ml')
| -rw-r--r-- | kernel/indtypes.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index e67aff0021..344ca87fbe 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -165,7 +165,7 @@ let abstract_mind_lc env ntyps npars lc = list_tabulate (function i -> lambda_implicit_lift npars (mkRel (i+1))) ntyps in - Array.map (compose (nf_beta env Evd.empty) (substl make_abs)) lc + Array.map (compose nf_beta (substl make_abs)) lc let listrec_mconstr env ntypes hyps nparams i indlc = let nhyps = List.length hyps in |