diff options
| author | barras | 2001-10-09 16:40:03 +0000 |
|---|---|---|
| committer | barras | 2001-10-09 16:40:03 +0000 |
| commit | f1778f0e830c50aaec250916f14e202d95960414 (patch) | |
| tree | ae220556180dfa55d6b638467deb7edf58d4c17b /kernel/reduction.ml | |
| parent | 8dbab7f463cabfc2913ab8615973c96ac98bf371 (diff) | |
Suppression des arguments sur les constantes, inductifs et constructeurs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2106 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/reduction.ml')
| -rw-r--r-- | kernel/reduction.ml | 15 |
1 files changed, 6 insertions, 9 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 5c0a4fa634..734187a9c7 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -201,7 +201,7 @@ let contract_cofix (bodynum,(types,names,bodies as typedbodies)) = let reduce_mind_case mia = match kind_of_term mia.mconstr with - | IsMutConstruct (ind_sp,i as cstr_sp, args) -> + | IsMutConstruct (ind_sp,i as cstr_sp) -> (* let ncargs = (fst mia.mci).(i-1) in*) let real_cargs = snd (list_chop (fst mia.mci) mia.mcargs) in applist (mia.mlf.(i-1),real_cargs) @@ -574,17 +574,14 @@ and eqappr cv_pb infos appr1 appr2 cuniv = let u3 = convert_vect infos el1 el2 cl1 cl2 u2 in convert_stacks infos lft1 lft2 v1 v2 u3 - | (FInd (op1,cl1), FInd(op2,cl2)) -> - if op1 = op2 then - let u1 = convert_vect infos el1 el2 cl1 cl2 cuniv in - convert_stacks infos lft1 lft2 v1 v2 u1 + | (FInd op1, FInd op2) -> + if op1 = op2 + then convert_stacks infos lft1 lft2 v1 v2 cuniv else raise NotConvertible - | (FConstruct (op1,cl1), FConstruct(op2,cl2)) -> + | (FConstruct op1, FConstruct op2) -> if op1 = op2 - then - let u1 = convert_vect infos el1 el2 cl1 cl2 cuniv in - convert_stacks infos lft1 lft2 v1 v2 u1 + then convert_stacks infos lft1 lft2 v1 v2 cuniv else raise NotConvertible | (FFix (op1,(_,tys1,cl1),_,_), FFix(op2,(_,tys2,cl2),_,_)) -> |