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_command.ml
Commit message (
Expand
)
Author
Age
*
Revert "Add [Polymorphic] flag for defs"
msozeau
2011-04-13
*
Add [Polymorphic] flag for defs
msozeau
2011-04-13
*
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
*
Change of nomenclature: rawconstr -> glob_constr
glondu
2010-12-23
*
Add information of localisation when an error involving an "implicit
herbelin
2010-11-07
*
Cleaning the use of parentheses around evd and evdref (cosmetic commit).
herbelin
2010-10-31
*
Fix bug #2393: allow let-ins inside telescopes (only fails when there's
msozeau
2010-10-12
*
Added multiple implicit arguments rules per name.
herbelin
2010-10-03
*
Remove some occurrences of "open Termops"
glondu
2010-09-28
*
Simplified the way internalization_data (i.e. bindings of bound vars
herbelin
2010-07-22
*
Move [delayed] to util and use [force_delayed] everywhere to force
msozeau
2010-06-30
*
Made tclABSTRACT normalize evars before saying it does not support
herbelin
2010-06-29
*
Fix treatment of {struct x} annotations in presence of generalized
msozeau
2010-06-08
*
fixed confusion between number of cstr arguments and number of pattern variab...
barras
2010-03-12
*
Consider OccurCheck a catchable exception.
msozeau
2010-03-08
*
Fix treatment of remaining unification constraints: raise a more
msozeau
2010-03-07
*
Few misc. updates.
herbelin
2010-01-04
*
Added support for definition of fixpoints using tactics.
herbelin
2009-11-27
*
Oops, nf_evar_defs just changed to nf_evar_map.
msozeau
2009-11-12
*
Don't forget to normalize everything w.r.t. evars (fixes bug #2103).
msozeau
2009-11-12
*
Promote evar_defs to evar_map (in Evd)
glondu
2009-11-11
*
Added support for multiple where-clauses in Inductive and co (see wish #2163).
herbelin
2009-11-11
*
Restructuration of command.ml + generic infrastructure for inductive schemes
herbelin
2009-11-08
*
Integrate a few improvements on typeclasses and Program from the equations br...
msozeau
2009-10-28
*
Make usage of Dyn explicit
glondu
2009-10-28
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
- Resolve type class constraints before trying to find unresolved
msozeau
2009-09-11
*
Fallback on not using [fix_proto] if the right imports aren't there, the
msozeau
2009-06-17
*
More efficient handling of evars in Program Fixpoint commands.
msozeau
2009-04-28
*
Backporting 12080 (fixing bug #2091 on bad rollback in the "where"
herbelin
2009-04-24
*
- New cleaning phase for the entry points of pretyping.ml
herbelin
2009-04-24
*
Experimental support for automatic destruction of recursive calls and
msozeau
2009-04-08
*
Fix bug #2083 for good: verify that the measure and relation are
msozeau
2009-04-08
*
Rewrite of Program Fixpoint to overcome the previous limitations:
msozeau
2009-03-28
*
Fixes in Program well-founded definitions:
msozeau
2009-03-26
*
Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...
letouzey
2009-03-20