index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
library
/
impargs.ml
Commit message (
Expand
)
Author
Age
*
More standard naming for the Imparg.with_implicits function.
Pierre-Marie Pédrot
2016-08-20
*
Removing dead code in Impargs.
Pierre-Marie Pédrot
2016-08-19
*
errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...
Pierre Letouzey
2016-07-03
*
Separate flags for fix/cofix/match reduction and clean reduction function names.
Maxime Dénès
2016-07-01
*
Exporting section_segment_of_reference.
Hugo Herbelin
2016-06-29
*
CLEANUP: Context.{Rel,Named}.Declaration.t
Matej Kosik
2016-02-09
*
Update copyright headers.
Maxime Dénès
2016-01-20
*
Fix some typos.
Guillaume Melquiond
2015-10-13
*
Remove almost all the uses of string concatenation when building error messages.
Guillaume Melquiond
2015-04-23
*
Update headers.
Maxime Dénès
2015-01-12
*
Getting rid of Exninfo hacks.
Pierre-Marie Pédrot
2014-12-16
*
Reverting the following block of three commits:
Hugo Herbelin
2014-11-27
*
Registering strict implicit arguments systematically.
Hugo Herbelin
2014-11-26
*
Keyed unification option, compiling the whole standard library
Matthieu Sozeau
2014-09-27
*
Parsing and printing of primitive projections, fix buggy behavior when
Matthieu Sozeau
2014-09-10
*
- Fix printing and parsing of primitive projections, including the Set
Matthieu Sozeau
2014-09-09
*
Move to a representation of universe polymorphic constants using indices for ...
Matthieu Sozeau
2014-08-03
*
Removing dead code.
Pierre-Marie Pédrot
2014-06-17
*
- Fix the de Bruijn problem in check_projection for good :)
Matthieu Sozeau
2014-06-17
*
Fix printing of projections with implicits.
Matthieu Sozeau
2014-05-06
*
Initial work on reintroducing old-style polymorphism for compatibility (the s...
Matthieu Sozeau
2014-05-06
*
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-05-06
*
Fix Bug 3217
Pierre Boutillier
2014-04-02
*
Fixing pervasive comparisons
Pierre-Marie Pédrot
2014-03-01
*
Turn many List.assoc into List.assoc_f
letouzey
2013-10-24
*
Get rid of the uses of deprecated OCaml elements (still remaining compatible ...
xclerc
2013-09-19
*
code simplifications concerning Summary
letouzey
2013-04-22
*
Restrict (try...with...) to avoid catching critical exn (part 8)
letouzey
2013-03-13
*
Actually adding backtrace handling.
ppedrot
2013-01-28
*
Uniformization of the "anomaly" command.
ppedrot
2013-01-28
*
Modulification of identifier
ppedrot
2012-12-14
*
Monomorphization (library)
ppedrot
2012-11-22
*
Remove some more "open" and dead code thanks to OCaml4 warnings
letouzey
2012-10-02
*
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
*
The new ocaml compiler (4.00) has a lot of very cool warnings,
regisgia
2012-09-14
*
Updating headers.
herbelin
2012-08-08
*
global_reference migrated from Libnames to new Globnames, less deps in gramma...
letouzey
2012-05-29
*
New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr
letouzey
2012-05-29
*
locus.mli for occurrences+clauses, misctypes.mli for various little things
letouzey
2012-05-29
*
Fixing alpha-conversion bug #2723 introduced in r12485-12486.
herbelin
2012-03-20
*
Noise for nothing
pboutill
2012-03-02
*
Fixed a Not_found bug when declaring in a section some implicit
herbelin
2011-12-18
*
Minor fixes to Arguments
gareuselesinge
2011-12-06
*
Renamig support added to "Arguments"
gareuselesinge
2011-11-21
*
New Arguments vernacular
gareuselesinge
2011-11-21
*
Add type annotations around all calls to Libobject.declare_object
letouzey
2011-11-02
*
Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacks
letouzey
2011-04-03
*
More comments and less doublons in some mli
pboutill
2011-02-10
[next]