index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
interp
/
notation.ml
Commit message (
Expand
)
Author
Age
...
*
Internalization of pattern is done in two phases.
pboutill
2012-06-14
*
Replacing some str with strbrk
ppedrot
2012-06-04
*
global_reference migrated from Libnames to new Globnames, less deps in gramma...
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
*
Notations are back in the "in" clause of pattern matching.
pboutill
2012-05-15
*
Slight change in the semantics of arguments scopes: scopes can no
herbelin
2012-03-26
*
Continuing r15045-15046 and r15055 (fixing bug #2732 about atomic
herbelin
2012-03-20
*
Noise for nothing
pboutill
2012-03-02
*
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
*
Add type annotations around all calls to Libobject.declare_object
letouzey
2011-11-02
*
Did that adding a rule for printing applications as "f(x)" works.
herbelin
2011-03-31
*
Added a table for using reserved names for binding names to types
herbelin
2011-03-05
*
fix last commit about modules (subst_cl_typ may raise Not_found)
letouzey
2011-02-12
*
An automatic substitution of scope at functor application
letouzey
2011-02-11
*
Annotations at functor applications:
letouzey
2011-02-11
*
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
*
Partial review of removed dead code (r13460)
herbelin
2010-09-24
*
Some dead code removal, thanks to Oug analyzer
letouzey
2010-09-24
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
Extension of the recursive notations mechanism
herbelin
2010-07-22
*
Fixed wrong spelling in a warning.
herbelin
2010-06-08
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Optimized need for delimiters when disjoint scopes for strings and
herbelin
2010-04-10
*
Several bug-fixes and improvements of coqdoc
herbelin
2010-03-29
*
list, length, app are migrated from List to Datatypes
letouzey
2009-11-02
*
Local/Global revision 12418 continued
herbelin
2009-10-26
*
New cleaning phase of the Local/Global option management
herbelin
2009-10-26
*
Improved the treatment of Local/Global options (noneffective Local on
herbelin
2009-10-25
*
This big commit addresses two problems:
soubiran
2009-10-21
*
Remove useless Liboject.export_function field
glondu
2009-09-17
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
Generalized the possibility to refer to a global name by a notation
herbelin
2009-09-11
*
Death of "survive_module" and "survive_section" (the first one was
herbelin
2009-08-13
*
- Cleaning phase of the interfaces of libnames.ml and nametab.ml
herbelin
2009-08-06
*
Fix a small notation/scope bug:
vsiles
2009-04-30
*
pushed evar reduction in kernel
barras
2009-02-06
*
Affichage des notations récursives:
herbelin
2008-10-22
*
Backporting 11445 from 8.2 to trunk (negative conditions in
herbelin
2008-10-11
*
Correct implementation of discharging of implicit arguments and add new
msozeau
2008-07-22
*
Uniformisation du format des messages d'erreur (commencent par une
herbelin
2008-07-17
*
Documentation Prop<=Set et Arguments Scope Global
herbelin
2008-07-01
*
Mises à jour test-suite + amélioration message d'erreur pour non-bug #1757
herbelin
2008-05-07
*
Add the ability to specify the implicit status of section variables and
msozeau
2008-04-02
[prev]
[next]