diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-09-10 20:37:37 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-09-10 20:37:37 +0000 |
| commit | e72024e2292a50684b7f280d6efb8fee090e2dbf (patch) | |
| tree | fdba2d8c55f0c74aee8800a0e8c9aec3d3b8a584 /library | |
| parent | 583992b6ce38655855f6625a26046ce84c53cdc1 (diff) | |
Suppression de Abst
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@593 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library')
| -rw-r--r-- | library/indrec.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/library/indrec.ml b/library/indrec.ml index c89578735..ddba73abe 100644 --- a/library/indrec.ml +++ b/library/indrec.ml @@ -56,10 +56,10 @@ let mis_make_case_com depopt env sigma mispec kind = it_lambda_name env' (lambda_create env' (build_dependent_inductive ind, - mkMutCaseA ci - (Rel (nbprod+nbargsprod)) - (Rel 1) - (rel_vect nbargsprod k))) + mkMutCase (ci, + Rel (nbprod+nbargsprod), + Rel 1, + rel_vect nbargsprod k))) lnamesar else let cs = lift_constructor (k+1) constrs.(k) in @@ -239,8 +239,8 @@ let mis_make_indrec env sigma listdepkind mispec = (lambda_create env (build_dependent_inductive (lift_inductive_family nrec indf), - mkMutCaseA (make_default_case_info mispeci) - (Rel (dect+j+1)) (Rel 1) branches)) + mkMutCase (make_default_case_info mispeci, + Rel (dect+j+1), Rel 1, branches))) (lift_context nrec lnames) in let typtyi = |