index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
toplevel
/
vernacentries.ml
Commit message (
Expand
)
Author
Age
*
Actually adding backtrace handling.
ppedrot
2013-01-28
*
Uniformization of the "anomaly" command.
ppedrot
2013-01-28
*
Modulification of name
ppedrot
2012-12-18
*
Modulification of Label
ppedrot
2012-12-18
*
Modulification of dir_path
ppedrot
2012-12-14
*
Modulification of identifier
ppedrot
2012-12-14
*
Monomorphization (toplevel)
ppedrot
2012-11-26
*
Print Assumptions: restore a final \n
letouzey
2012-11-17
*
Monomorphized a lot of equalities over OCaml integers, thanks to
ppedrot
2012-11-08
*
Fixed #2926:
ppedrot
2012-10-29
*
Split Tacinterp in 3 files : Tacsubst, Tacintern and Tacinterp
letouzey
2012-10-16
*
Fixing #2865.
ppedrot
2012-09-25
*
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
*
Assumption commands are now displayed as unsafe in Coqide.
aspiwack
2012-08-24
*
Do not forget to build the unicode libraries, necessary to compile and launch...
msozeau
2012-08-22
*
Added support for option Local (at module level) in Tactic Notation.
herbelin
2012-08-11
*
Updating headers.
herbelin
2012-08-08
*
Vecnacentries.dump_global silently ignores exceptions
pboutill
2012-08-06
*
Dump references in reduction tactics
pboutill
2012-08-05
*
Dump references in Reset
pboutill
2012-08-05
*
Fixing test-suite
pboutill
2012-07-20
*
Various minor fixes to coqdoc from A. Chlipala.
msozeau
2012-07-18
*
A new status Unsafe in Interface. Meant for commands such as Admitted.
aspiwack
2012-07-12
*
Vernacentries: minor code cleanup
letouzey
2012-07-12
*
Also allow Reset in Load'ed files
letouzey
2012-07-11
*
Re-allow Reset in compiled files
letouzey
2012-07-11
*
Fixes bug 2841 ([Focus 0] gives anomaly).
aspiwack
2012-07-10
*
Restore an indentation of Show Script
letouzey
2012-07-07
*
A prototype implementation of a Print Namespace command.
aspiwack
2012-07-06
*
Backtrack: add support for the "Proof c." syntax (fix #2832)
letouzey
2012-07-06
*
Added an indirection with respect to Loc in Compat. As many [open Compat]
ppedrot
2012-06-22
*
I forgot a line in previous commit.
aspiwack
2012-06-22
*
A call to the command Proof (and its variants) now prints the subgoals.
aspiwack
2012-06-22
*
Getting rid of Pcoq remains.
ppedrot
2012-06-12
*
Separated notice vs info messages, and cleaned up the interface a bit.
ppedrot
2012-06-04
*
More cleaning
ppedrot
2012-06-01
*
Cleaning Pp.ppnl use
ppedrot
2012-06-01
*
Getting rid of Pp.msgnl and Pp.message.
ppedrot
2012-06-01
*
Getting rid of Pp.msg
ppedrot
2012-05-30
*
More uniformisation in Pp.warn functions.
ppedrot
2012-05-30
*
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
*
locus.mli for occurrences+clauses, misctypes.mli for various little things
letouzey
2012-05-29
*
Decl_kinds becomes a pure mli file, remaining ops in new file kindops.ml
letouzey
2012-05-29
*
Vernacexpr is now a mli-only file, locality stuff now in locality.ml
letouzey
2012-05-29
*
Program: avoid staying in program mode after a failed Program command
letouzey
2012-04-26
*
correct abort in Function when a proof of inversion fails
letouzey
2012-04-23
[next]