index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
lib
/
util.mli
Commit message (
Expand
)
Author
Age
...
*
- Fix treatment of globality flag for typeclass instance hints (they
msozeau
2011-02-14
*
Added multiple implicit arguments rules per name.
herbelin
2010-10-03
*
Fixed a bug introduced (r13316/r13329) in the printing of notations
herbelin
2010-07-29
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
Constrintern: unified push_name_env and push_loc_name_env; made
herbelin
2010-07-22
*
Move [delayed] to util and use [force_delayed] everywhere to force
msozeau
2010-06-30
*
New script dev/tools/change-header to automatically update Coq files headers.
herbelin
2010-06-22
*
Extraction: replace unicode characters in ident by ascii encodings (fix #2158...
letouzey
2010-06-21
*
Fixing spelling: pr_coma -> pr_comma
herbelin
2010-06-12
*
Fix treatment of {struct x} annotations in presence of generalized
msozeau
2010-06-08
*
Add (almost) compatibility with camlp4, without breaking support for camlp5
letouzey
2010-05-19
*
Nicer representation of tokens, more independant of camlp*
letouzey
2010-05-19
*
Various minor improvements of comments in mli for ocamldoc
letouzey
2010-04-29
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Move from ocamlweb to ocamdoc to generate mli documentation
pboutill
2010-04-29
*
Added a new exception for already declared Schemes,
vsiles
2010-04-27
*
Reduced the complexity of evar instantiations from O(n^3) to less than O(n^2).
herbelin
2010-04-19
*
Util: remove list_split_at which is a clone of list_chop
letouzey
2010-04-16
*
Fix [Existing Class] impl and add documentation. Fix computation of the
msozeau
2010-02-10
*
Experiment propagation of implicit arguments and arguments scope for
herbelin
2009-11-12
*
Integrate a few improvements on typeclasses and Program from the equations br...
msozeau
2009-10-28
*
Fixed a hole in glob_tactic that allowed some Ltac code to refer to
herbelin
2009-09-26
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
Generalized the possibility to refer to a global name by a notation
herbelin
2009-09-11
*
- Cleaning phase of the interfaces of libnames.ml and nametab.ml
herbelin
2009-08-06
*
- Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalence
herbelin
2009-05-09
*
comparison functions on lists and arrays
barras
2009-04-16
*
Timeout message was not always displayed
barras
2009-03-04
*
Heavy modifications on the widget and edition tab creation mechanism.
vgross
2009-03-02
*
memoized is_ground_env
barras
2009-02-09
*
Petit nettoyage faisant suite au commit #11847 .
aspiwack
2009-01-23
*
Remove trailing newlines in outputs of X -where
glondu
2009-01-08
*
Made the debugger work again:
herbelin
2009-01-02
*
- Another bug in get_sort_family_of (sort-polymorphism of constants and
herbelin
2008-12-28
*
- coq_makefile: target install now respects the original tree structure
herbelin
2008-12-24
*
- Fixed many "Theorem with" bugs.
herbelin
2008-10-27
*
Affichage des notations récursives:
herbelin
2008-10-22
*
Évolutions diverses et variées.
herbelin
2008-08-04
*
Suite commit 11236
notin
2008-07-24
*
Quelques modifications autour du filtrage Ltac:
herbelin
2008-07-16
*
Fixes in handling of implicit arguments:
msozeau
2008-07-04
*
- Correction de la version simplifiée (filtrage sur deux sig
herbelin
2008-06-09
*
- Extension de "generalize" en "generalize c as id at occs".
herbelin
2008-06-08
*
Correction terminologie et ajout plage unicode 1D400-1D7FF (mathematical
herbelin
2008-06-06
*
Ajout de la possibilité d'utiliser fix/cofix dans les notations.
herbelin
2008-05-24
*
- Prise en compte de l'unicode dans la fonction hdchar (elle fournissait des
herbelin
2008-05-10
*
Bugs, nettoyage, et améliorations diverses
herbelin
2008-04-13
*
improved the implementation of rtree
barras
2008-03-18
*
Merge with lmamane's private branch:
lmamane
2008-02-22
*
Add list_iter3
msozeau
2008-01-30
[prev]
[next]