index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
toplevel
Commit message (
Expand
)
Author
Age
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-03-20
|
\
*
|
Moving Tacintern to Hightactics.
Pierre-Marie Pédrot
2016-03-20
*
|
Moving the Ltac definition command to an EXTEND based command.
Pierre-Marie Pédrot
2016-03-20
*
|
Moving the tactic related code from Metasyntax to a new file.
Pierre-Marie Pédrot
2016-03-20
*
|
Moving Print Ltac to an EXTEND based command.
Pierre-Marie Pédrot
2016-03-20
*
|
Moving Tactic Notation to an EXTEND based command.
Pierre-Marie Pédrot
2016-03-20
*
|
Moving Tacinterp to Hightactics.
Pierre-Marie Pédrot
2016-03-20
*
|
Moving the use of Tactic_option from Obligations to G_obligations.
Pierre-Marie Pédrot
2016-03-19
*
|
Moving VernacSolve to an EXTEND-based definition.
Pierre-Marie Pédrot
2016-03-19
*
|
Replacing the interpretation of Proof using ... with a proper code.
Pierre-Marie Pédrot
2016-03-19
*
|
Removing dead code in Pcoq.
Pierre-Marie Pédrot
2016-03-18
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-03-18
|
\
\
*
|
|
Removing the special status of generic arguments defined by Coq itself.
Pierre-Marie Pédrot
2016-03-17
*
|
|
Removing the special status of generic entries defined by Coq itself.
Pierre-Marie Pédrot
2016-03-17
|
|
*
Fix bug #4627: records with no declared arity can be template polymorphic.
Matthieu Sozeau
2016-03-17
|
|
/
*
|
Adding a universe argument to Pcoq.create_generic_entry.
Pierre-Marie Pédrot
2016-03-17
*
|
Removing the registering of default values for generic arguments.
Pierre-Marie Pédrot
2016-03-17
*
|
Relying on parsing rules rather than genarg to check if an argument is empty.
Pierre-Marie Pédrot
2016-03-17
|
*
Fix bug when a sort is ascribed to a Record
Matthieu Sozeau
2016-03-15
*
|
Typeclasses: respect Declare Instance priority
Matthieu Sozeau
2016-03-14
*
|
Removing OCaml deprecated function names from the Lazy module.
Pierre-Marie Pédrot
2016-03-10
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-03-09
|
\
|
|
*
Adding backtraces to scheme error messages.
Pierre-Marie Pédrot
2016-03-07
*
|
Moving Autorewrite to Hightatctic.
Pierre-Marie Pédrot
2016-03-06
*
|
Removing dependency of Himsg in tactic files.
Pierre-Marie Pédrot
2016-03-06
*
|
Moving Tactic_debug to tactics/ folder.
Pierre-Marie Pédrot
2016-03-06
*
|
Moving Ltac traces to Tacexpr and Tacinterp.
Pierre-Marie Pédrot
2016-03-06
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-03-05
|
\
|
|
*
Rename Ephemeron -> CEphemeron.
Maxime Dénès
2016-03-04
*
|
Moving the "clear" tactic to TACTIC EXTEND.
Pierre-Marie Pédrot
2016-02-29
*
|
Printing notations: Cleaning in anticipation of fixing #4592.
Hugo Herbelin
2016-02-28
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-02-21
|
\
|
|
*
Fixing bug #4580: [Set Refine Instance Mode] also used for Program Instance.
Pierre-Marie Pédrot
2016-02-19
*
|
Renaming variants of Entries.local_entry
Matej Kosik
2016-02-16
*
|
merging conflicts with the original "trunk__CLEANUP__Context__2" branch
Matej Kosik
2016-02-15
|
\
\
*
|
|
Using monotonic types for conversion functions.
Pierre-Marie Pédrot
2016-02-15
*
|
|
Moving conversion functions to the new tactic API.
Pierre-Marie Pédrot
2016-02-15
*
|
|
Renaming functions in Typing to stick to the standard e_* scheme.
Pierre-Marie Pédrot
2016-02-15
*
|
|
Monotonizing the Evarutil module.
Pierre-Marie Pédrot
2016-02-15
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-02-13
|
\
\
\
|
|
|
/
|
|
/
|
|
|
*
CLEANUP: Context.{Rel,Named}.Declaration.t
Matej Kosik
2016-02-09
|
|
/
|
/
|
|
*
Improving error message with missing patterns in the presence of
Hugo Herbelin
2016-02-08
*
|
Infering atomic ML entries from their grammar.
Pierre-Marie Pédrot
2016-02-01
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-29
|
\
|
|
*
Fixing bug #3826: "Incompatible module types" is uninformative.
Pierre-Marie Pédrot
2016-01-24
|
*
Fixing bug #4495: Failed assertion in metasyntax.ml.
Pierre-Marie Pédrot
2016-01-24
|
*
Implement support for universe binder lists in Instance and Program Fixpoint/...
Matthieu Sozeau
2016-01-23
|
*
Restore warnings produced by the interpretation of the command line
Hugo Herbelin
2016-01-22
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-21
|
\
|
*
|
Stronger invariants on the use of the introduction pattern (pat1,...,patn).
Hugo Herbelin
2016-01-21
[next]