index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
interp
Commit message (
Expand
)
Author
Age
*
locus.mli for occurrences+clauses, misctypes.mli for various little things
letouzey
2012-05-29
*
Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evd
letouzey
2012-05-29
*
Notations are back in the "in" clause of pattern matching.
pboutill
2012-05-15
*
Impossible branches inference fixup (bug 2761)
pboutill
2012-05-11
*
"A -> B" is a notation for "forall _ : A, B".
pboutill
2012-04-12
*
Fixing the "capture" check newly introduced in r15122 when
herbelin
2012-04-07
*
Unifying the different procedures for interning binders.
herbelin
2012-04-06
*
Fixing a few bugs (see #2571) related to interpretation of multiple binders
herbelin
2012-04-06
*
Slight change in the semantics of arguments scopes: scopes can no
herbelin
2012-03-26
*
Fixing deactivation of scope at printing time in the body of a
herbelin
2012-03-26
*
Fixing bug #2724 (using notations with binders in cases patterns
herbelin
2012-03-20
*
Fixing alpha-conversion bug #2723 introduced in r12485-12486.
herbelin
2012-03-20
*
Continuing r15045-15046 and r15055 (fixing bug #2732 about atomic
herbelin
2012-03-20
*
Fixing bug #2732 (anomaly when using the tolerance for writing
herbelin
2012-03-18
*
Second step of integration of Program:
msozeau
2012-03-14
*
Glob_term.predicate_pattern: No number of parameters with letins.
pboutill
2012-03-02
*
"Let in" in pattern hell, one more iteration
pboutill
2012-03-02
*
Noise for nothing
pboutill
2012-03-02
*
Fix compilation of Constrintern...
pboutill
2012-02-29
*
RefMan update about match syntax.
pboutill
2012-02-29
*
In the syntax of pattern matching, the arguments of the inductive in the "in"
pboutill
2012-02-29
*
In the syntax of pattern matching, "in" clauses are patterns.
pboutill
2012-02-29
*
Debugger vs tracer: Two different behaviors wrt printing: The debugger
herbelin
2012-02-01
*
Printing bugs with match patterns:
herbelin
2012-01-27
*
Added documentation for "Set Parsing Explicit" + fixed mistakenly
herbelin
2012-01-20
*
Added new command "Set Parsing Explicit" for deactivating parsing (and
herbelin
2012-01-20
*
Notations with binders: Accepting using notations for functional terms
herbelin
2012-01-20
*
Boolean Option Patterns Compatibility
pboutill
2012-01-19
*
Parameters in pattern first step.
pboutill
2012-01-16
*
Backtracking on r14876 (fix for bug #2267): extra scopes might be
herbelin
2012-01-05
*
Fixing Arguments Scope bug when too many scopes are given (bug #2667).
herbelin
2012-01-04
*
Fixing bug #2634 (unscoped notations were disturbing the
herbelin
2011-12-18
*
A pass on warning printings. Made systematic the use of msg_warning so
herbelin
2011-12-17
*
Fixing amazing loop when using eta-expansion in pattern-matching for
herbelin
2011-12-16
*
Renamig support added to "Arguments"
gareuselesinge
2011-11-21
*
New Arguments vernacular
gareuselesinge
2011-11-21
*
Fixing association of wrong "as"-pattern name when expanding
herbelin
2011-11-16
*
Allow "|_=>_" in "match" in patterns, no more forced enumeration of constructors
letouzey
2011-11-07
*
Add type annotations around all calls to Libobject.declare_object
letouzey
2011-11-02
*
Fixed broken globalization of identifiers containing utf8 letters
herbelin
2011-10-29
*
Added checksums to glob files and warned about possibly missing
herbelin
2011-10-29
*
Remove dynamic stuff from constr_expr and glob_constr
glondu
2011-10-28
*
Fixing failing printer when the type of a binder name with implicit
herbelin
2011-10-24
*
Quick improvement of some error messages related to module application
herbelin
2011-08-30
*
Fixing printing bug with last trailing non-maximally implicit
herbelin
2011-08-10
*
Partial revert of r14292
pboutill
2011-07-26
*
Add a syntax entry for fully applied constructor pattern
pboutill
2011-07-22
*
Internalization of pattern carries a full intern_env
pboutill
2011-07-22
*
This adds two option tables 'Printing Record' and 'Printing Constructor'
herbelin
2011-07-16
*
This option disables the use of the '{| field := ... |}' notation
herbelin
2011-07-16
[next]