diff options
| author | herbelin | 2006-07-03 16:40:20 +0000 |
|---|---|---|
| committer | herbelin | 2006-07-03 16:40:20 +0000 |
| commit | 1e69c6a499757b05180205e84ed2bf6f1cbf7b2f (patch) | |
| tree | 0b6c57991e1bd849593f846ae8b91ce18d9f9194 /interp/constrextern.ml | |
| parent | b7c3f0f2f57bcd0cc768c869d707b70f78c5bbfd (diff) | |
Extension des motifs disjonctifs au cas de disjonction de motifs multiples
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8997 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/constrextern.ml')
| -rw-r--r-- | interp/constrextern.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index a81ca599c8..44f4baee60 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -186,7 +186,7 @@ let rec check_same_type ty1 ty2 = | CCases(_,_,a1,brl1), CCases(_,_,a2,brl2) -> List.iter2 (fun (tm1,_) (tm2,_) -> check_same_type tm1 tm2) a1 a2; List.iter2 (fun (_,pl1,r1) (_,pl2,r2) -> - List.iter2 check_same_pattern pl1 pl2; + List.iter2 (List.iter2 check_same_pattern) pl1 pl2; check_same_type r1 r2) brl1 brl2 | CHole _, CHole _ -> () | CPatVar(_,i1), CPatVar(_,i2) when i1=i2 -> () @@ -797,7 +797,7 @@ and extern_local_binder scopes vars = function LocalRawAssum([(dummy_loc,na)],ty) :: l)) and extern_eqn inctx scopes vars (loc,ids,pl,c) = - (loc,List.map (extern_cases_pattern_in_scope scopes vars) pl, + (loc,[List.map (extern_cases_pattern_in_scope scopes vars) pl], extern inctx scopes vars c) and extern_symbol (tmp_scope,scopes as allscopes) vars t = function |