| Commit message (Expand) | Author | Age |
* | Adding a printer for hints. | Hugo Herbelin | 2014-10-07 |
* | Fixing nice printing of error reporting with ml tactics bound to ltac names. | Hugo Herbelin | 2014-10-01 |
* | Fixing use of arguments renaming in apply which was broken after | Hugo Herbelin | 2014-10-01 |
* | Index keys instead of simply global references. | Matthieu Sozeau | 2014-09-27 |
* | STM: encapsulate Pp.message in Feedback.feedback | Carst Tankink | 2014-08-04 |
* | Moved code for finding subterms (pattern, induction, set, generalize, ...) | Hugo Herbelin | 2014-06-28 |
* | Made the subterm finding function make_abstraction independent of the | Hugo Herbelin | 2014-06-28 |
* | all coqide specific files moved into ide/ | Enrico Tassi | 2014-06-25 |
* | Fix module order in printers.mllib | Matthieu Sozeau | 2014-06-10 |
* | Moving a Thread.yield in check_interrupt. | Pierre-Marie Pédrot | 2014-06-07 |
* | Adding a new Control file centralizing the control options of Coq. | Pierre-Marie Pédrot | 2014-06-07 |
* | - Fix in kernel conversion not folding the universe constraints | Matthieu Sozeau | 2014-05-26 |
* | Moving Dnet-related code to tactics/. | Pierre-Marie Pédrot | 2014-05-08 |
* | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau | 2014-05-06 |
* | Machine arithmetic operations for native compiler. | Maxime Dénès | 2014-04-09 |
* | Had to split Nativelambda in two files because of Retroknowledge | Maxime Dénès | 2014-04-09 |
* | Uint31 support. | Maxime Dénès | 2014-04-09 |
* | Adding a canary library. This canary is imperfect. It allows serialization | Pierre-Marie Pédrot | 2014-03-05 |
* | Added a new module HMap. It works (almost) like Map, except that it expects | Pierre-Marie Pédrot | 2014-03-05 |
* | Adding a CSet module in Coq lib. | Pierre-Marie Pédrot | 2014-03-05 |
* | Matching --> ConstrMatching (was clashing with OCaml's compiler-libs) | Pierre Letouzey | 2014-03-02 |
* | Grammar.cma with less deps (Glob_ops and Nameops) after moving minor code | Pierre Letouzey | 2014-03-02 |
* | Code refactoring thanks to the new Monad module. | Arnaud Spiwack | 2014-02-27 |
* | Remove unsafe code (Obj.magic) in Tacinterp. | Arnaud Spiwack | 2014-02-27 |
* | Lazyconstr -> Opaqueproof | Enrico Tassi | 2014-02-26 |
* | Aux_file: cache information at compile time for later (re)use | Enrico Tassi | 2014-01-04 |
* | Support for evars and metas in native compiler. | Maxime Dénès | 2013-12-30 |
* | Notations now accept the $(...)$ tactic-in-term syntax. They are resolved at | Pierre-Marie Pédrot | 2013-12-22 |
* | Adding generic solvers to term holes. For now, no resolution mechanism nor | Pierre-Marie Pédrot | 2013-11-27 |
* | Replaced monads.ml by an essentially equivalent proofview_gen.ml generated by... | aspiwack | 2013-11-02 |
* | Conv_orable made functional and part of pre_env | gareuselesinge | 2013-10-31 |
* | Ephemeron: marshaling friendly keys | gareuselesinge | 2013-10-18 |
* | At least made the evar type opaque! There are still 5 remaining unsafe | ppedrot | 2013-09-18 |
* | Moving Searchstack to CStack, and normalizing names a bit. | ppedrot | 2013-09-06 |
* | Added a more efficient way to recover the domain of a map. | ppedrot | 2013-08-25 |
* | Fix compilation of dev/printres.cma | gareuselesinge | 2013-08-20 |
* | State Transaction Machine | gareuselesinge | 2013-08-08 |
* | Future library to represent pure computations | gareuselesinge | 2013-08-08 |
* | Removing the use of leveled tactics wit_tacticn. It is now handled | ppedrot | 2013-07-02 |
* | Splitted up Genarg in four different levels: | ppedrot | 2013-06-21 |
* | Cutting the dependency of Genarg in constr_expr, glob_constr | ppedrot | 2013-06-21 |
* | Proof-of-concept: moved four easy-to-handle generic arguments to | ppedrot | 2013-06-18 |
* | Adding a persistent stream data structure. | ppedrot | 2013-05-28 |
* | Gmap is now useless, hail to Map! | ppedrot | 2013-05-14 |
* | Removing Fmap from libraries, it is not used anymore. | ppedrot | 2013-05-14 |
* | Removing Fset, since it is not used anymore. | ppedrot | 2013-05-12 |
* | Added a generic notion of hook. Hooks are functions to be set | ppedrot | 2013-05-12 |
* | Getting rid of module Gmapl. | ppedrot | 2013-05-09 |
* | add Loadpath to printers.mllib | gareuselesinge | 2013-05-09 |
* | Merging Context and Sign. | ppedrot | 2013-04-29 |