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 /library | |
| 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 'library')
| -rw-r--r-- | library/indrec.ml | 13 | ||||
| -rw-r--r-- | library/indrec.mli | 2 |
2 files changed, 8 insertions, 7 deletions
diff --git a/library/indrec.ml b/library/indrec.ml index 36c9f884f3..251656c600 100644 --- a/library/indrec.ml +++ b/library/indrec.ml @@ -470,11 +470,12 @@ let build_indrec env sigma mispec = (* To interpret the Match operator *) (* TODO: check that we can drop universe constraints ? *) -let type_mutind_rec env sigma (IndType (indf,realargs) as ind) pt p c = +let type_mutind_rec env sigma (IndType (indf,realargs) as ind) pj c = + let p = pj.uj_val in let (mispec,params) = dest_ind_family indf in let tyi = mis_index mispec in if mis_is_recursive_subset [tyi] mispec then - let (dep,_) = find_case_dep_nparams env sigma (c,p) indf pt in + let (dep,_) = find_case_dep_nparams env sigma (c,pj) indf in let init_depPvec i = if i = tyi then Some(dep,p) else None in let depPvec = Array.init (mis_ntypes mispec) init_depPvec in let vargs = Array.of_list params in @@ -486,13 +487,13 @@ let type_mutind_rec env sigma (IndType (indf,realargs) as ind) pt p c = if dep then applist(p,realargs@[c]) else applist(p,realargs) ) else - let (p,ra,_) = type_case_branches env sigma ind pt p c in + let (p,ra,_) = type_case_branches env sigma ind pj c in (p,ra) -let type_rec_branches recursive env sigma ind pt p c = +let type_rec_branches recursive env sigma ind pj c = if recursive then - type_mutind_rec env sigma ind pt p c + type_mutind_rec env sigma ind pj c else - let (p,ra,_) = type_case_branches env sigma ind pt p c in + let (p,ra,_) = type_case_branches env sigma ind pj c in (p,ra) diff --git a/library/indrec.mli b/library/indrec.mli index 4f3cd5ee7e..e50766348b 100644 --- a/library/indrec.mli +++ b/library/indrec.mli @@ -39,7 +39,7 @@ val build_mutual_indrec : (* These are for old Case/Match typing *) val type_rec_branches : bool -> env -> 'c evar_map -> inductive_type - -> constr -> constr -> constr -> constr array * constr + -> unsafe_judgment -> constr -> constr array * constr val make_rec_branch_arg : env -> 'a evar_map -> int * ('b * constr) option array * int -> |