index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
plugins
/
subtac
/
subtac_classes.ml
Commit message (
Expand
)
Author
Age
*
Final part of moving Program code inside the main code. Adapted add_definitio...
msozeau
2012-03-14
*
Second step of integration of Program:
msozeau
2012-03-14
*
Noise for nothing
pboutill
2012-03-02
*
Correct application of head reduction.
msozeau
2012-02-20
*
Fix for Program Instance not separately checking the resolution of evars of t...
msozeau
2012-01-23
*
Merge subinstances branch by me and Tom Prince.
msozeau
2011-11-17
*
Fix bug #2557 and an issue with Propers for complement
msozeau
2011-10-07
*
Fix bug 2269, program typechecker not used in Instance conclusions
msozeau
2011-06-17
*
Revert "Add [Polymorphic] flag for defs"
msozeau
2011-04-13
*
Add [Polymorphic] flag for defs
msozeau
2011-04-13
*
- Add modulo_delta_types flag for unification to allow full
msozeau
2011-03-13
*
Keep information on which fields are subclasses in class declarations,
msozeau
2011-03-11
*
Interp a definition with the implicit arguments of its local context
pboutill
2011-02-10
*
Data structure telling implicits of local variables is a map in the
pboutill
2011-02-10
*
Remove the "Boxed" syntaxes and the const_entry_boxed field
letouzey
2011-01-28
*
Rename rawterm.ml into glob_term.ml
glondu
2010-12-23
*
Cleaning the use of parentheses around evd and evdref (cosmetic commit).
herbelin
2010-10-31
*
Fix bug# 2392
msozeau
2010-10-07
*
Added multiple implicit arguments rules per name.
herbelin
2010-10-03
*
Fix bug #2321, allowing "_" named projections in classes. Not realizing
msozeau
2010-09-28
*
Remove some occurrences of "open Termops"
glondu
2010-09-28
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
Simplified the way internalization_data (i.e. bindings of bound vars
herbelin
2010-07-22
*
Made tclABSTRACT normalize evars before saying it does not support
herbelin
2010-06-29
*
Remove compile-command pragmas for emacs
letouzey
2010-05-19
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Backport fixes in Instance declarations to Program Instance.
msozeau
2010-01-28
*
Promote evar_defs to evar_map (in Evd)
glondu
2009-11-11
*
A bit of cleaning around name generation + creation of dedicated file namegen.ml
herbelin
2009-11-09
*
Restructuration of command.ml + generic infrastructure for inductive schemes
herbelin
2009-11-08
*
Fixed record syntax "{|x=...; y=...|}" so that it works with qualified names.
gmelquio
2009-11-04
*
Integrate a few improvements on typeclasses and Program from the equations br...
msozeau
2009-10-28
*
Fix bug #2162 and a name clashing bug in generalized binders.
msozeau
2009-10-09
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
Support for definition hooks in subtac.
msozeau
2009-05-16
*
Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...
letouzey
2009-03-20