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
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-03-05
|
\
|
*
Fixing bug #4105: poor escaping in the protocol between CoqIDE and coqtop.
Pierre-Marie Pédrot
2016-03-03
*
|
Printing notations: Cleaning in anticipation of fixing #4592.
Hugo Herbelin
2016-02-28
|
/
*
Update copyright headers.
Maxime Dénès
2016-01-20
*
Make sure that scope classes are displayed by Print Scopes. (Fix bug #4262)
Guillaume Melquiond
2015-07-08
*
Introduction of a "Undelimit Scope" command, undoing "Delimit Scope"
Lionel Rieg
2015-06-26
*
Remove almost all the uses of string concatenation when building error messages.
Guillaume Melquiond
2015-04-23
*
Normalize scope names before storing them in vo files. (Fix for bug #4162)
Guillaume Melquiond
2015-03-27
*
Fixing equality of notation_constrs. Fixes bug #4136.
Pierre-Marie Pédrot
2015-03-24
*
Revert "Useless check when loading notations through import."
Pierre-Marie Pédrot
2015-03-24
*
Update headers.
Maxime Dénès
2015-01-12
*
Getting rid of Exninfo hacks.
Pierre-Marie Pédrot
2014-12-16
*
Add syntax for naming new goals in refine: writing ?[id] instead of _
Hugo Herbelin
2014-09-30
*
Notation: option to attach extra pretty printing rules to notations
Enrico Tassi
2014-09-29
*
Add a boolean to indicate the unfolding state of a primitive projection,
Matthieu Sozeau
2014-09-27
*
Fix HoTT bug #84, binding scopes to projections.
Matthieu Sozeau
2014-06-17
*
Removing dead code.
Pierre-Marie Pédrot
2014-06-17
*
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-05-06
*
Fixing generic hashes and replacing them with proper ones.
Pierre-Marie Pédrot
2014-03-03
*
Grammar.cma with less deps (Glob_ops and Nameops) after moving minor code
Pierre Letouzey
2014-03-02
*
Fixing pervasive comparisons
Pierre-Marie Pédrot
2014-03-01
*
Useless check when loading notations through import.
Pierre-Marie Pédrot
2014-03-01
*
Reverting the old LIFO behaviour of the notation finding algorithm.
ppedrot
2013-11-08
*
Do not generate useless argument arrays in whd_* functions.
ppedrot
2013-10-29
*
More monomorphic List.mem + List.assoc + ...
letouzey
2013-10-24
*
cList: set-as-list functions are now with an explicit comparison
letouzey
2013-10-23
*
Some more hand-written comparison functions to avoid polymorphic comparison.
xclerc
2013-10-14
*
Get rid of the uses of deprecated OCaml elements (still remaining compatible ...
xclerc
2013-09-19
*
Actually using the domain function for maps.
ppedrot
2013-08-25
*
More dynamic argument scopes
letouzey
2013-07-17
*
Removing useless uses of Gmap.
ppedrot
2013-05-14
*
Getting rid of module Gmapl.
ppedrot
2013-05-09
*
Removing Gmap from Notations.
ppedrot
2013-05-09
*
Uniformizing the [if_warn] flag used for warning printing and put
ppedrot
2013-05-08
*
States: frozen states can hold closures
gareuselesinge
2013-05-06
*
code simplifications concerning Summary
letouzey
2013-04-22
*
Restrict (try...with...) to avoid catching critical exn (part 8)
letouzey
2013-03-13
*
Dir_path --> DirPath
letouzey
2013-02-19
*
Actually adding backtrace handling.
ppedrot
2013-01-28
*
Uniformization of the "anomaly" command.
ppedrot
2013-01-28
*
Modulification of dir_path
ppedrot
2012-12-14
*
Modulification of identifier
ppedrot
2012-12-14
*
Renamed Option.Misc.compare to the more uniform Option.equal.
ppedrot
2012-12-13
*
Monomorphization (interp)
ppedrot
2012-11-25
*
More equality functions
ppedrot
2012-11-25
*
Taking into account the type of a definition (if it exists), and the
herbelin
2012-11-17
*
Added a CString module.
ppedrot
2012-11-13
*
Remove some more "open" and dead code thanks to OCaml4 warnings
letouzey
2012-10-02
*
Moving Utils.list_* to a proper CList module, which includes stdlib
ppedrot
2012-09-14
*
The new ocaml compiler (4.00) has a lot of very cool warnings,
regisgia
2012-09-14
[next]