aboutsummaryrefslogtreecommitdiff
path: root/printing
AgeCommit message (Expand)Author
2014-05-22Removing useless use of metaids in tactic AST.Pierre-Marie Pédrot
2014-05-21Removing decompose record / sum from the tactic AST.Pierre-Marie Pédrot
2014-05-21Moving left & right tactics out of the AST.Pierre-Marie Pédrot
2014-05-20Moving (e)transitivity out of the AST.Pierre-Marie Pédrot
2014-05-20Tentative to add constr-using primitive tactics without grammar rules.Pierre-Marie Pédrot
2014-05-16Moving argument-free tactics out of the AST into a dedicatedPierre-Marie Pédrot
2014-05-16Slightly better printer for native ML tactics, in order to disambiguatePierre-Marie Pédrot
2014-05-06Print universes in module printingMatthieu Sozeau
2014-05-06- Fix bug preventing apply from unfolding Fixpoints.Matthieu Sozeau
2014-05-06Adapt universe polymorphic branch to new handling of futures for delayed proofs.Matthieu Sozeau
2014-05-06Adapt Y. Bertot's path on private inductives (now the keyword is "Private").Yves Bertot
2014-05-06Initial work on reintroducing old-style polymorphism for compatibility (the s...Matthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-04-23Better representation of evar filters: we represent the vacuous filters ofPierre-Marie Pédrot
2014-04-23Removing dead code, thanks to new OCaml warnings and a bit of scripting.Pierre-Marie Pédrot
2014-04-14Closing bug #3260Julien Forest
2014-03-31Removing the Change_evar refiner rule.Pierre-Marie Pédrot
2014-03-19Adding a Print Strategy vernacular command. It allows to check thePierre-Marie Pédrot
2014-03-05Remove some dead-code (thanks to ocaml warnings)Pierre Letouzey
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2014-03-02Grammar.cma with less deps (Glob_ops and Nameops) after moving minor codePierre Letouzey
2014-02-28Fix output test-suite 'simpl tactic' -> 'reduction tactics'Pierre Boutillier
2014-02-26Lazyconstr -> OpaqueproofEnrico Tassi
2014-02-26New compilation mode -vi2voEnrico Tassi
2014-02-24Simpl_behaviour becomes Reductionops.ReductionBehaviourPierre Boutillier
2014-02-02Removing the [Require "file"] syntax.Pierre-Marie Pédrot
2014-01-19Adding a default object to generic argument registering mechanism.Pierre-Marie Pédrot
2014-01-17Follow-up of bugfix for #3204: local definitions were not handled properly.Pierre-Marie Pédrot
2014-01-16Fixing bugs #1039: Hypotheses don't respect Barendregt conventionPierre-Marie Pédrot
2014-01-05Proof_using: new syntax + suggestionEnrico Tassi
2013-12-19Removing the useless pattern ident genarg.Pierre-Marie Pédrot
2013-12-19Printing function for Stdargs in debuggerPierre Boutillier
2013-12-16A few fixes to the build system (mostly for ocamlbuild)Pierre Letouzey
2013-12-01Removing RefArgType generic argument.Pierre-Marie Pédrot
2013-11-30Getting rid of casted_open_constr. It was only used by thePierre-Marie Pédrot
2013-11-27Adding generic solvers to term holes. For now, no resolution mechanism norPierre-Marie Pédrot
2013-11-13Synchronizing the printer of tactic notations.ppedrot
2013-11-10Removing the dependency of every level of tactic ATSs on glob_tactic_expr.ppedrot
2013-11-09Revert the previous commit. It broke Coq compilation.ppedrot
2013-11-09Removing the dependency of every level of tactic ATSs on glob_tactic_expr.ppedrot
2013-11-02Update comments.aspiwack
2013-11-02Adds a tactic give_up.aspiwack
2013-11-02Adds a shelve tactic.aspiwack
2013-11-02Adds an experimental exactly_once tactical.aspiwack
2013-11-02Adds a tactical once.aspiwack
2013-11-02Added the tactical "tac1 + tac2".aspiwack
2013-11-02Fixes parsing of all: followed by a typechecking/evaluation command.aspiwack
2013-11-02New option Default Goal Selector.aspiwack
2013-11-02Adds a new goal selector "all:".aspiwack
2013-10-31Conv_orable made functional and part of pre_envgareuselesinge
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-03 20:16:36 +0000