diff options
| author | filliatr | 1999-08-26 09:58:19 +0000 |
|---|---|---|
| committer | filliatr | 1999-08-26 09:58:19 +0000 |
| commit | d410804226ddeb15ab05af5298502ef29efbd0d8 (patch) | |
| tree | 98ad9f8c69d3d1ead1547e173fd071a23bf2deb3 /kernel/sign.ml | |
| parent | ab00c680d097bb067f135b0ab149b224db0787a7 (diff) | |
- abstraction
- univers fonctionnels
- erreurs de typage maintenant sous forme d'exception,
déclarées dans Type_errors
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@24 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/sign.ml')
| -rw-r--r-- | kernel/sign.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/sign.ml b/kernel/sign.ml index 661f64042c..c0e8658120 100644 --- a/kernel/sign.ml +++ b/kernel/sign.ml @@ -24,7 +24,7 @@ let rev_sign (idl,tyl) = (List.rev idl, List.rev tyl) let map_sign_typ f (idl,tyl) = (idl, List.map f tyl) let concat_sign (idl1,tyl1) (idl2,tyl2) = (idl1@idl2, tyl1@tyl2) let diff_sign (idl1,tyl1) (idl2,tyl2) = - (subtract idl1 idl2, subtract tyl1 tyl2) + (list_subtract idl1 idl2, list_subtract tyl1 tyl2) let nth_sign (idl,tyl) n = (List.nth idl (n-1), List.nth tyl (n-1)) let map_sign_graph f (ids,tys) = List.map2 f ids tys @@ -134,7 +134,7 @@ let add_sign_replacing whereid (id,t) sign = are distinct. *) let prepend_sign gamma1 gamma2 = - if [] = intersect (ids_of_sign gamma1) (ids_of_sign gamma2) then + if [] = list_intersect (ids_of_sign gamma1) (ids_of_sign gamma2) then let (ids1,vals1) = gamma1 and (ids2,vals2) = gamma2 in (ids1@ids2, vals1@vals2) |