diff options
author | 2005-07-15 21:57:22 +0000 | |
---|---|---|
committer | 2005-07-15 21:57:22 +0000 | |
commit | 4b0da48602bad97f4f5238eccac9fa3a0bdecda4 (patch) | |
tree | 88212405b23d90dfbf0af93a1e13b2ccad106cbc /contrib/subtac/sutils.ml | |
parent | 2db7263c70fbf401422fe4797e86659c4d7c4310 (diff) |
Subtac: traitement correct des existentielles et de la récursion.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7237 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/subtac/sutils.ml')
-rw-r--r-- | contrib/subtac/sutils.ml | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/contrib/subtac/sutils.ml b/contrib/subtac/sutils.ml new file mode 100644 index 000000000..64365b676 --- /dev/null +++ b/contrib/subtac/sutils.ml @@ -0,0 +1,11 @@ +let list_index x l = + let rec aux i = function + y :: tl -> if x = y then i else aux (succ i) tl + | [] -> raise Not_found + in aux 0 l + +let list_assoc_index x l = + let rec aux i = function + (y, _) :: tl -> if x = y then i else aux (succ i) tl + | [] -> raise Not_found + in aux 0 l |