aboutsummaryrefslogtreecommitdiff
path: root/printing
AgeCommit message (Expand)Author
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
2013-10-27Abstracting evar filter away. The API is not perfect, but better than nothing.ppedrot
2013-10-24More monomorphic List.mem + List.assoc + ...letouzey
2013-10-24Turn many List.assoc into List.assoc_fletouzey
2013-10-23cList: set-as-list functions are now with an explicit comparisonletouzey
2013-10-10STM: add "Stm Wait" to wait for the slaves to complete their jobsgareuselesinge
2013-10-07STM: new command "Stm PrintDag" to force printing the dag to /tmpgareuselesinge
2013-10-05Moving side effects into evar_map. There was no reason to keep anotherppedrot
2013-09-19Prettyp: avoid useless "let module"letouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 10:50:41 +0000