diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-12-28 19:03:04 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-12-28 19:03:04 +0000 |
| commit | f5eb06f0d2b28fe72db12fb57458b961b9ae9d85 (patch) | |
| tree | f989b726ca64f25d9830e0d563e4992fbede83cc /lib | |
| parent | 835f581b40183986e76e5e02a26fab05239609c9 (diff) | |
- Another bug in get_sort_family_of (sort-polymorphism of constants and
inductive types was not taken into account).
- Virtually extended tauto to
- support arbitrary-length disjunctions and conjunctions,
- support arbitrary complex forms of disjunctions and
conjunctions when in the contravariant of an implicative hypothesis,
- stick with the purely propositional fragment and not apply reflexivity.
This is virtual in the sense that it is not activated since it breaks
compatibility with the existing tauto.
- Modified the notion of conjunction and unit type used in hipattern in a
way that is closer to the intuitive meaning (forbid dependencies
between parameters in conjunction; forbid indices in unit types).
- Investigated how far "iff" could be turned into a direct inductive
definition; modified tauto.ml4 so that it works with the current and
the alternative definition.
- Fixed a bug in the error message from lookup_eliminator.
- Other minor changes.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11721 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/util.ml | 7 | ||||
| -rw-r--r-- | lib/util.mli | 1 |
2 files changed, 8 insertions, 0 deletions
diff --git a/lib/util.ml b/lib/util.ml index 3b04e2574..b7aa1fc0e 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -946,6 +946,13 @@ let array_for_all4 f v1 v2 v3 v4 = lv1 = Array.length v4 && allrec (pred lv1) +let array_for_all_i f i v = + let rec allrec i = function + | -1 -> true + | n -> (f i v.(n)) && (allrec (i-1) (n-1)) + in + allrec i ((Array.length v)-1) + let array_hd v = match Array.length v with | 0 -> failwith "array_hd" diff --git a/lib/util.mli b/lib/util.mli index dc6498b15..49e1fb4bd 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -196,6 +196,7 @@ val array_for_all3 : ('a -> 'b -> 'c -> bool) -> 'a array -> 'b array -> 'c array -> bool val array_for_all4 : ('a -> 'b -> 'c -> 'd -> bool) -> 'a array -> 'b array -> 'c array -> 'd array -> bool +val array_for_all_i : (int -> 'a -> bool) -> int -> 'a array -> bool val array_hd : 'a array -> 'a val array_tl : 'a array -> 'a array val array_last : 'a array -> 'a |