aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
Commit message (Expand)AuthorAge
* Dead code.Gravatar Hugo Herbelin2014-06-06
* Making those proofs which depend on names generated for the argumentsGravatar Hugo Herbelin2014-06-01
* poly: remove unused attribute to STM nodes and vernac classificaitonGravatar Enrico Tassi2014-05-15
* Now parsing rules of ML-declared tactics are only made available after theGravatar Pierre-Marie Pédrot2014-05-12
* Reuse universe level substitutions for template polymorphism, fixing performanceGravatar Matthieu Sozeau2014-05-09
* Renaming new_induct -> induction; new_destruct -> destruct.Gravatar Hugo Herbelin2014-05-08
* Fix extraction taking a type in the wrong environment.Gravatar Matthieu Sozeau2014-05-06
* Fix Field_tac to get fast reification again, with the fix on template univers...Gravatar Matthieu Sozeau2014-05-06
* Try a new way of handling template universe levelsGravatar Matthieu Sozeau2014-05-06
* Fix funind w.r.t. universesGravatar Matthieu Sozeau2014-05-06
* Fix a pervasive equality use.Gravatar Matthieu Sozeau2014-05-06
* Fix derive plugin to properly treat universesGravatar Matthieu Sozeau2014-05-06
* - 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
* - Fix abstract forgetting about new constraints.Gravatar Matthieu Sozeau2014-05-06
* - Rename eq to equal in Univ, document new modules, set interfaces.Gravatar Matthieu Sozeau2014-05-06
* Initial work on reintroducing old-style polymorphism for compatibility (the s...Gravatar Matthieu Sozeau2014-05-06
* Correct rebase on STM code. Thanks to E. Tassi for help on dealing withGravatar Matthieu Sozeau2014-05-06
* Rework handling of universes on top of the STM, allowing for delayedGravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Eta contractions to please cbnGravatar Pierre Boutillier2014-05-02
* Fixing ml-doc.Gravatar Pierre-Marie Pédrot2014-05-01
* Remove unused lookup table.Gravatar Guillaume Melquiond2014-04-28
* Removing useless try-with clauses in Goal.enter variants.Gravatar Pierre-Marie Pédrot2014-04-25
* closing bug 3037Gravatar Julien Forest2014-04-05
* Using HMaps in global references.Gravatar Pierre-Marie Pédrot2014-03-08
* 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
* Fixing some generic equalities in Micromega.Gravatar Pierre-Marie Pédrot2014-03-03
* Fixing Pervasives.equality in extraction.Gravatar Pierre-Marie Pédrot2014-03-03
* Getting rid of generic hashes in cc plugin.Gravatar Pierre-Marie Pédrot2014-03-03
* Matching --> ConstrMatching (was clashing with OCaml's compiler-libs)Gravatar Pierre Letouzey2014-03-02
* Grammar.cma with less deps (Glob_ops and Nameops) after moving minor codeGravatar Pierre Letouzey2014-03-02
* Removing generic equality in Syntax plugin.Gravatar Pierre-Marie Pédrot2014-03-02
* Fixing pervasive comparisonsGravatar Pierre-Marie Pédrot2014-03-01
* Proofview.Notations: Now that (>>=) is free, use it for tclBIND.Gravatar Arnaud Spiwack2014-02-27
* Lazyconstr -> OpaqueproofGravatar Enrico Tassi2014-02-26
* New compilation mode -vi2voGravatar Enrico Tassi2014-02-26
* Stack operations of Reductionops in Reductionops.StackGravatar Pierre Boutillier2014-02-24
* Removing non-marshallable data from the Agram constructor. Instead ofGravatar Pierre-Marie Pédrot2014-02-16
* fast correction of bug #3234Gravatar Julien Forest2014-02-14
* Less dependencies in Omega.Gravatar Pierre-Marie Pédrot2014-02-08
* Relaunch all Unix.waitpid when they ended with EINTRGravatar Pierre Letouzey2014-01-30
* bug correction in proving principles of functionGravatar jforest2014-01-20
* Omega: avoiding distinct proof-terms on repeated identical runsGravatar Pierre Letouzey2014-01-10
* Qed: feedback when type checking is doneGravatar Enrico Tassi2013-12-24
* micromega: removal of spurious Export; addition of Lia.v encapsulating lia an...Gravatar Frédéric Besson2013-12-20
* Removing the need of evarmaps in constr internalization.Gravatar Pierre-Marie Pédrot2013-12-17
* Fix g_derive.ml4.Gravatar Arnaud Spiwack2013-12-04
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-13 20:13:01 +0000