diff options
| author | herbelin | 2000-05-31 11:46:29 +0000 |
|---|---|---|
| committer | herbelin | 2000-05-31 11:46:29 +0000 |
| commit | 301d5af223390fa5c82da9ae9958f610493ba814 (patch) | |
| tree | 304f4b7b194ace4c6fac67af90a0bcdf3ff3537f /library | |
| parent | aca8a6bbb4fa372cd3b27680eee642082d1c2ad5 (diff) | |
Nettoyage de Generic
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@482 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library')
| -rw-r--r-- | library/indrec.ml | 10 |
1 files changed, 3 insertions, 7 deletions
diff --git a/library/indrec.ml b/library/indrec.ml index a8f708c459..f83138b3d0 100644 --- a/library/indrec.ml +++ b/library/indrec.ml @@ -253,12 +253,8 @@ let mis_make_indrec env sigma listdepkind mispec = let fixn = Array.of_list (List.rev ln) in let fixtyi = Array.of_list (List.rev ltyp) in let fixdef = Array.of_list (List.rev ldef) in - let makefixdef = - put_DLAMSV - (list_tabulate (fun _ -> Name(id_of_string "F")) nrec) fixdef - in - let fixspec = Array.append fixtyi [|makefixdef|] in - DOPN(Fix(fixn,p),fixspec) + let names = list_tabulate (fun _ -> Name(id_of_string "F")) nrec in + mkFix ((fixn,p),(fixtyi,names,fixdef)) in mrec 0 [] [] [] in @@ -442,7 +438,7 @@ let pred_case_ml_fail env sigma isrec (IndType (indf,realargs)) (i,ft) = let nbrec = if isrec then count_rec_arg j recargi else 0 in let nb_arg = List.length (recargs.(i-1)) + nbrec in let pred = concl_n env sigma nb_arg ft in - if noccur_bet 1 nb_arg pred then + if noccur_between 1 nb_arg pred then lift (-nb_arg) pred else failwith "Dependent" |