index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
toplevel
/
command.ml
Commit message (
Expand
)
Author
Age
*
Use more consistent resolution parameters in Program and regular typing
msozeau
2009-06-18
*
Fix implicit args code so that declarations are added for all
msozeau
2009-05-27
*
Fix to my last notation patch: now fixpoint are correctly handled
vsiles
2009-05-13
*
Fix a small notation/scope bug:
vsiles
2009-04-30
*
- Cleaning (unification of ML names, removal of obsolete code,
herbelin
2009-04-27
*
Backporting 12080 (fixing bug #2091 on bad rollback in the "where"
herbelin
2009-04-24
*
Fix bug #2089: correctly dealing with parameters and real arguments in
msozeau
2009-04-16
*
Some dead code removal + cleanups
letouzey
2009-04-08
*
- Fixing bug #2084 (unification not checking sort constraints), hoping
herbelin
2009-04-08
*
- Backport of 12053 (fixing parsing segfault bug #2087) and 12058 (fixing
herbelin
2009-04-08
*
On remplace evar_map par evar_defs (seul evar_defs est désormais exporté
aspiwack
2009-02-19
*
Petit nettoyage faisant suite au commit #11847 .
aspiwack
2009-01-23
*
DISCLAIMER
puech
2009-01-17
*
Bug dans commit 11743
herbelin
2009-01-04
*
Fixed bugs #2001 (search_guard was overwriting the guard index given
herbelin
2009-01-04
*
Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->
herbelin
2008-12-31
*
More factorization of inductive/record and typeclasses: move class
msozeau
2008-11-09
*
Slight change of the semantics of user-given casts: they don't really
msozeau
2008-11-07
*
11511 continued (bug in set.out + incohérence dans "Theorem with"
herbelin
2008-10-28
*
- Fixed many "Theorem with" bugs.
herbelin
2008-10-27
*
Affichage des notations récursives:
herbelin
2008-10-22
*
- Export de pattern_ident vers les ARGUMENT EXTEND and co.
herbelin
2008-10-19
*
In manual implicit arguments mode, do not enrich implicits
msozeau
2008-09-14
*
Add enough information to correctly globalize recursive calls in inductive and
msozeau
2008-09-11
*
Various fixes w.r.t typeclasses and subtac: resolve tcs properly inside
msozeau
2008-08-21
*
Report des commits 11297 et 11299 (nom Unnamed_theorem local caché par
herbelin
2008-08-04
*
Fixed bug #1904 (instances of evars were no longer substituted since
herbelin
2008-07-25
*
Uniformisation du format des messages d'erreur (commencent par une
herbelin
2008-07-17
*
- Improve [Context] vernacular to allow arbitrary binders, not just
msozeau
2008-07-07
*
Fixes in handling of implicit arguments:
msozeau
2008-07-04
*
Catch a Not_found exception in the Combined Scheme mechanism to hide an ugly
vsiles
2008-06-24
*
Fixes incorrect handling of existing existentials variables in
msozeau
2008-06-03
*
Improvements on coqdoc by adding more information into .glob
msozeau
2008-05-30
*
- Fix bug #1858, Hint Unfold calling the wrong locate function.
msozeau
2008-05-23
*
- Fix bug related to indices of fixpoints.
msozeau
2008-05-13
*
Postpone the search for the recursive argument index from the user given
msozeau
2008-05-06
*
Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuve
herbelin
2008-04-25
*
Fix bug #1844, generalize implementation to handle and combination of
msozeau
2008-04-24
*
Prise en compte des coercions dans les clauses "with" même si le type
herbelin
2008-04-23
*
Add the ability to specify the implicit status of section variables and
msozeau
2008-04-02
*
Ajout d'abbréviations/notations paramétriques
herbelin
2008-03-30
*
Finish fix in command where we still lost information on what was a type
msozeau
2008-03-24
*
Correct bug introduced in r10589, where we lost information that
msozeau
2008-03-21
*
* Small change in the make_eq_decidability call : the functions does not (yet)
vsiles
2008-03-18
*
* Factorizing code : context_chop was used in several files (even as chop_con...
vsiles
2008-03-17
*
Do a second pass on the treatment of user-given implicit arguments. Now
msozeau
2008-03-15
*
fix the 'decreasing on Xth' message
letouzey
2008-03-13
*
* Catching a Not_found exception when trying to use Scheme Equality
vsiles
2008-03-12
*
Proper implicit arguments handling for assumptions
msozeau
2008-02-26
*
Merge with lmamane's private branch:
lmamane
2008-02-22
[next]