diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-03-21 18:16:19 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-03-21 18:16:19 +0000 |
| commit | 9a913a2aa1834704908ec829d5326d214fd68e88 (patch) | |
| tree | 446368bfbd7223a1fc0cd7e0d608865a06e96f75 /pretyping | |
| parent | 1269a0b06f4b23f7183b8c649a6aa3cd114a6b77 (diff) | |
Modification de type_of_case, type_case_branches, etc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@352 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/pretyping.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 3af306fe4..29d02b013 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -82,7 +82,7 @@ let transform_rec loc env sigma cl (ct,pt) = if Array.length lf <> expn then error_number_branches_loc loc CCI env c ct expn; if is_recursive [mispec.mis_tyi] recargs then - let (dep,_) = find_case_dep_nparams env sigma (c,p) appmind pt in + let dep = find_case_dep_nparams env sigma (c,p) appmind pt in let ntypes = mis_ntypes mispec (* was mis_nconstr !?! *) and tyi = mispec.mis_tyi and nparams = mis_nparams mispec in @@ -414,7 +414,7 @@ match cstr with (* Où teste-t-on que le résultat doit satisfaire tycon ? *) let evalct = nf_ise1 !isevars cj.uj_type and evalPt = nf_ise1 !isevars pj.uj_type in - let (_,bty,rsty) = + let (bty,rsty) = Indrec.type_rec_branches isrec env !isevars evalct evalPt pj.uj_val cj.uj_val in if Array.length bty <> Array.length lf then wrong_number_of_cases_message loc env isevars (cj.uj_val,evalct) |