diff options
| author | herbelin | 2000-05-26 15:57:50 +0000 |
|---|---|---|
| committer | herbelin | 2000-05-26 15:57:50 +0000 |
| commit | 2372cbdcabec698e5deb5abfc393ed3e6909995f (patch) | |
| tree | 57021a056665c433ca41aee125825bbeb7bc6d58 /kernel/typeops.ml | |
| parent | b726fcfd1de249ab4fb5bb82f64fa349d2c17a0f (diff) | |
Modification messages d'erreurs, possibilité de n'importe quel constr dans les instances de références
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@478 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/typeops.ml')
| -rw-r--r-- | kernel/typeops.ml | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 6c7e1bbe5e..1a6c1d885f 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -317,7 +317,7 @@ let cast_rel env sigma cj tj = (* Type of an application. *) let apply_rel_list env sigma nocheck argjl funj = - let rec apply_rec typ cst = function + let rec apply_rec n typ cst = function | [] -> { uj_val = applist (j_val_only funj, List.map j_val_only argjl); uj_type = typ; @@ -327,18 +327,19 @@ let apply_rel_list env sigma nocheck argjl funj = match whd_betadeltaiota env sigma typ with | DOP2(Prod,c1,DLAM(_,c2)) -> if nocheck then - apply_rec (subst1 hj.uj_val c2) cst restjl + apply_rec (n+1) (subst1 hj.uj_val c2) cst restjl else (try let c = conv_leq env sigma hj.uj_type c1 in let cst' = Constraint.union cst c in - apply_rec (subst1 hj.uj_val c2) cst' restjl + apply_rec (n+1) (subst1 hj.uj_val c2) cst' restjl with NotConvertible -> - error_cant_apply CCI env "Type Error" funj argjl) + error_cant_apply_bad_type CCI env (n,hj.uj_type,c1) + funj argjl) | _ -> - error_cant_apply CCI env "Non-functional construction" funj argjl + error_cant_apply_not_functional CCI env funj argjl in - apply_rec funj.uj_type Constraint.empty argjl + apply_rec 1 funj.uj_type Constraint.empty argjl (* Fixpoints. *) |