index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
printing
/
printer.ml
Commit message (
Expand
)
Author
Age
...
*
Printing function for [uconstr].
Arnaud Spiwack
2014-11-19
*
Removing the legacy intro tactic code.
Pierre-Marie Pédrot
2014-11-07
*
Removing the old rename tactic.
Pierre-Marie Pédrot
2014-11-04
*
Info: print a name for the primitive tactics in [Proofview].
Arnaud Spiwack
2014-11-01
*
Pushing Pierre's factorization of names in goal context printing from
Hugo Herbelin
2014-10-22
*
Experimental printing of the signature of open evars in Check.
Hugo Herbelin
2014-10-17
*
Goal: remove most of the API (make [Goal.goal] concrete).
Arnaud Spiwack
2014-10-16
*
Removing Convert_concl and Convert_hyp from Logic.
Hugo Herbelin
2014-10-09
*
Going back on granting wish #1039 in f5d7b2b1e so that apply with
Hugo Herbelin
2014-10-01
*
Fix a message.
Arnaud Spiwack
2014-09-24
*
coqtop -emacs: do not declare "still unfocused goals" as an "infomsg".
Arnaud Spiwack
2014-09-24
*
Revert specific syntax for primitive projections, avoiding ugly
Matthieu Sozeau
2014-09-17
*
Not printing goal name (reinstalled by mistake in a previous commit).
Hugo Herbelin
2014-09-15
*
Fixing bug #3619 in emacs mode.
Hugo Herbelin
2014-09-15
*
Prepare goal name printing but no not print them at the current time.
Hugo Herbelin
2014-09-13
*
Checking typability of evar instances. Using ";" to separate bindings
Hugo Herbelin
2014-09-13
*
Use evar name to print goal.
Hugo Herbelin
2014-09-12
*
Referring to evars by names. Added a parser for evars (but parsing of
Hugo Herbelin
2014-09-12
*
Removing the old implementation of clear_body.
Pierre-Marie Pédrot
2014-09-05
*
Revert the two previous commits. I was testing in the wrong branch.
Pierre-Marie Pédrot
2014-09-04
*
Removing the old implementation of clear_body.
Pierre-Marie Pédrot
2014-09-04
*
Inductive and CoInductive records are printed correctly.
Arnaud Spiwack
2014-09-04
*
Print [Variant] types with the keyword [Variant].
Arnaud Spiwack
2014-09-04
*
Coqide prints succesive hyps of the same type on 1 line
Pierre Boutillier
2014-09-01
*
Simplify even further the declaration of primitive projections,
Matthieu Sozeau
2014-08-30
*
Move to a representation of universe polymorphic constants using indices for ...
Matthieu Sozeau
2014-08-03
*
Feedback: LoadedFile + Goals
Enrico Tassi
2014-07-11
*
Removing dead code.
Pierre-Marie Pédrot
2014-06-17
*
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
*
Better representation of evar filters: we represent the vacuous filters of
Pierre-Marie Pédrot
2014-04-23
*
Removing dead code, thanks to new OCaml warnings and a bit of scripting.
Pierre-Marie Pédrot
2014-04-23
*
Removing the Change_evar refiner rule.
Pierre-Marie Pédrot
2014-03-31
*
Remove some dead-code (thanks to ocaml warnings)
Pierre Letouzey
2014-03-05
*
Remove many superfluous 'open' indicated by ocamlc -w +33
Pierre Letouzey
2014-03-05
*
Grammar.cma with less deps (Glob_ops and Nameops) after moving minor code
Pierre Letouzey
2014-03-02
*
Follow-up of bugfix for #3204: local definitions were not handled properly.
Pierre-Marie Pédrot
2014-01-17
*
Fixing bugs #1039: Hypotheses don't respect Barendregt convention
Pierre-Marie Pédrot
2014-01-16
*
Adds a tactic give_up.
aspiwack
2013-11-02
*
Adds a shelve tactic.
aspiwack
2013-11-02
*
Abstracting evar filter away. The API is not perfect, but better than nothing.
ppedrot
2013-10-27
*
Moving side effects into evar_map. There was no reason to keep another
ppedrot
2013-10-05
*
Get rid of the uses of deprecated OCaml elements (still remaining compatible ...
xclerc
2013-09-19
*
At least made the evar type opaque! There are still 5 remaining unsafe
ppedrot
2013-09-18
*
Partly replacing list-based access functions in Evd. This is still
ppedrot
2013-09-03
*
Some cleanup in Auto
ppedrot
2013-09-03
*
Nicer code concerning dirpaths and modpath around Lib
letouzey
2013-08-22
*
State Transaction Machine
gareuselesinge
2013-08-08
*
Removing useless uses of Gmap.
ppedrot
2013-05-14
*
Merging Context and Sign.
ppedrot
2013-04-29
[prev]
[next]