index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
interp
/
constrextern.ml
Commit message (
Expand
)
Author
Age
*
As r15801: putting everything from Util.array_* to CArray.*.
ppedrot
2012-09-14
*
Moving Utils.list_* to a proper CList module, which includes stdlib
ppedrot
2012-09-14
*
This patch removes unused "open" (automatically generated from
regisgia
2012-09-14
*
Fixed bug #2895
ppedrot
2012-09-09
*
Updating headers.
herbelin
2012-08-08
*
Fixing bug #2835 (the rationale for printing notations was not
herbelin
2012-07-21
*
Fixup implicits in patterns & notations
pboutill
2012-07-20
*
Bug 2838: ExplApp in mutual inductive parameters
pboutill
2012-07-12
*
ZArith + other : favor the use of modern names instead of compat notations
letouzey
2012-07-05
*
Added an indirection with respect to Loc in Compat. As many [open Compat]
ppedrot
2012-06-22
*
Fixing printing of @f with no arguments
herbelin
2012-06-19
*
Constrextern is allow to use partially applied notations
pboutill
2012-06-14
*
Internalization of pattern is done in two phases.
pboutill
2012-06-14
*
No more Univ in grammar.cma
letouzey
2012-05-29
*
global_reference migrated from Libnames to new Globnames, less deps in gramma...
letouzey
2012-05-29
*
Basic stuff about constr_expr migrated from topconstr to constrexpr_ops
letouzey
2012-05-29
*
Stuff about notation_constr (ex-aconstr) now in notation_ops.ml
letouzey
2012-05-29
*
New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr
letouzey
2012-05-29
*
Glob_term now mli-only, operations now in Glob_ops
letouzey
2012-05-29
*
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
*
"A -> B" is a notation for "forall _ : A, B".
pboutill
2012-04-12
*
Fixing deactivation of scope at printing time in the body of a
herbelin
2012-03-26
*
Fixing alpha-conversion bug #2723 introduced in r12485-12486.
herbelin
2012-03-20
*
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
*
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 new command "Set Parsing Explicit" for deactivating parsing (and
herbelin
2012-01-20
*
Boolean Option Patterns Compatibility
pboutill
2012-01-19
*
Parameters in pattern first step.
pboutill
2012-01-16
*
Allow "|_=>_" in "match" in patterns, no more forced enumeration of constructors
letouzey
2011-11-07
*
Remove dynamic stuff from constr_expr and glob_constr
glondu
2011-10-28
*
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
*
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
*
Rather quick hack to avoid using notations involving "Type" when
herbelin
2011-06-12
*
Yet another bug in printing fix with let-in binders
herbelin
2011-04-24
*
Fixing multiple printing bugs with "Notation f x := ..."
herbelin
2011-04-08
*
Did that adding a rule for printing applications as "f(x)" works.
herbelin
2011-03-31
*
More {raw => glob} changes for consistency
glondu
2010-12-24
*
Rename rawterm.ml into glob_term.ml
glondu
2010-12-23
*
Change of nomenclature: rawconstr -> glob_constr
glondu
2010-12-23
*
Added multiple implicit arguments rules per name.
herbelin
2010-10-03
*
Fix function applications without labels (OCaml warning 6)
glondu
2010-09-28
[next]