aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing
Commit message (Expand)AuthorAge
* - Fix bug preventing apply from unfolding Fixpoints.Gravatar Matthieu Sozeau2014-05-06
* Adapt universe polymorphic branch to new handling of futures for delayed proofs.Gravatar Matthieu Sozeau2014-05-06
* Adapt Y. Bertot's path on private inductives (now the keyword is "Private").Gravatar Yves Bertot2014-05-06
* Initial work on reintroducing old-style polymorphism for compatibility (the s...Gravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Better representation of evar filters: we represent the vacuous filters ofGravatar Pierre-Marie Pédrot2014-04-23
* Removing dead code, thanks to new OCaml warnings and a bit of scripting.Gravatar Pierre-Marie Pédrot2014-04-23
* Closing bug #3260Gravatar Julien Forest2014-04-14
* Removing the Change_evar refiner rule.Gravatar Pierre-Marie Pédrot2014-03-31
* Adding a Print Strategy vernacular command. It allows to check theGravatar Pierre-Marie Pédrot2014-03-19
* Remove some dead-code (thanks to ocaml warnings)Gravatar Pierre Letouzey2014-03-05
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Grammar.cma with less deps (Glob_ops and Nameops) after moving minor codeGravatar Pierre Letouzey2014-03-02
* Fix output test-suite 'simpl tactic' -> 'reduction tactics'Gravatar Pierre Boutillier2014-02-28
* Lazyconstr -> OpaqueproofGravatar Enrico Tassi2014-02-26
* New compilation mode -vi2voGravatar Enrico Tassi2014-02-26
* Simpl_behaviour becomes Reductionops.ReductionBehaviourGravatar Pierre Boutillier2014-02-24
* Removing the [Require "file"] syntax.Gravatar Pierre-Marie Pédrot2014-02-02
* Adding a default object to generic argument registering mechanism.Gravatar Pierre-Marie Pédrot2014-01-19
* Follow-up of bugfix for #3204: local definitions were not handled properly.Gravatar Pierre-Marie Pédrot2014-01-17
* Fixing bugs #1039: Hypotheses don't respect Barendregt conventionGravatar Pierre-Marie Pédrot2014-01-16
* Proof_using: new syntax + suggestionGravatar Enrico Tassi2014-01-05
* Removing the useless pattern ident genarg.Gravatar Pierre-Marie Pédrot2013-12-19
* Printing function for Stdargs in debuggerGravatar Pierre Boutillier2013-12-19
* A few fixes to the build system (mostly for ocamlbuild)Gravatar Pierre Letouzey2013-12-16
* Removing RefArgType generic argument.Gravatar Pierre-Marie Pédrot2013-12-01
* Getting rid of casted_open_constr. It was only used by theGravatar Pierre-Marie Pédrot2013-11-30
* Adding generic solvers to term holes. For now, no resolution mechanism norGravatar Pierre-Marie Pédrot2013-11-27
* Synchronizing the printer of tactic notations.Gravatar ppedrot2013-11-13
* Removing the dependency of every level of tactic ATSs on glob_tactic_expr.Gravatar ppedrot2013-11-10
* Revert the previous commit. It broke Coq compilation.Gravatar ppedrot2013-11-09
* Removing the dependency of every level of tactic ATSs on glob_tactic_expr.Gravatar ppedrot2013-11-09
* Update comments.Gravatar aspiwack2013-11-02
* Adds a tactic give_up.Gravatar aspiwack2013-11-02
* Adds a shelve tactic.Gravatar aspiwack2013-11-02
* Adds an experimental exactly_once tactical.Gravatar aspiwack2013-11-02
* Adds a tactical once.Gravatar aspiwack2013-11-02
* Added the tactical "tac1 + tac2".Gravatar aspiwack2013-11-02
* Fixes parsing of all: followed by a typechecking/evaluation command.Gravatar aspiwack2013-11-02
* New option Default Goal Selector.Gravatar aspiwack2013-11-02
* Adds a new goal selector "all:".Gravatar aspiwack2013-11-02
* Conv_orable made functional and part of pre_envGravatar gareuselesinge2013-10-31
* Abstracting evar filter away. The API is not perfect, but better than nothing.Gravatar ppedrot2013-10-27
* More monomorphic List.mem + List.assoc + ...Gravatar letouzey2013-10-24
* Turn many List.assoc into List.assoc_fGravatar letouzey2013-10-24
* cList: set-as-list functions are now with an explicit comparisonGravatar letouzey2013-10-23
* STM: add "Stm Wait" to wait for the slaves to complete their jobsGravatar gareuselesinge2013-10-10
* STM: new command "Stm PrintDag" to force printing the dag to /tmpGravatar gareuselesinge2013-10-07
* Moving side effects into evar_map. There was no reason to keep anotherGravatar ppedrot2013-10-05
* Prettyp: avoid useless "let module"Gravatar letouzey2013-09-19