aboutsummaryrefslogtreecommitdiff
path: root/printing
AgeCommit message (Expand)Author
2014-07-01Add toplevel commands to declare global universes and constraints.Matthieu Sozeau
2014-06-17Removing dead code.Pierre-Marie Pédrot
2014-06-16- Add "Show Universes" to print information about universes during a proof.Matthieu Sozeau
2014-06-11Fix bug #3289Matthieu Sozeau
2014-06-10Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un...Matthieu Sozeau
2014-06-06Remove the syntax [Vernac1. Vernac2. … Vernacn. ].Arnaud Spiwack
2014-06-06Moving the [split] tactic out of the AST.Pierre-Marie Pédrot
2014-06-04- Better parsing and printing of named universes: Type{ident} and foo@{(ident...Matthieu Sozeau
2014-06-04- Allow parsing of @const@{instance} for specifying universe instances of pol...Matthieu Sozeau
2014-06-04- Fix hashing of levels to get the "right" order in universe contexts etc...Matthieu Sozeau
2014-05-22Moving the "specialize" tactic out of the AST. Also removed an obsoletePierre-Marie Pédrot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-19 00:41:19 +0000