aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
Commit message (Expand)AuthorAge
* admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Gravatar Enrico Tassi2015-03-11
* Fix bug #3732: firstorder was using detyping to build existentialGravatar Matthieu Sozeau2015-03-03
* Fix bug #3590, keeping evars that are not turned into named metas byGravatar Matthieu Sozeau2015-03-03
* Removing the unused field ltacrecvars of tactic internalization.Gravatar Pierre-Marie Pédrot2015-02-27
* Calling coq references lazily in plugin cc so as to support static linking of...Gravatar Hugo Herbelin2015-02-24
* Fix some typos in comments.Gravatar Guillaume Melquiond2015-02-23
* Fixing OCaml 3.12 compilation.Gravatar Pierre-Marie Pédrot2015-02-14
* Abstract: "Qed export ident, .., ident" to preserve v8.4 behaviorGravatar Enrico Tassi2015-02-14
* Univs: fix bug #3978: carry around the universe context used toGravatar Matthieu Sozeau2015-02-12
* Revert "Capital letter in plugins." (Sorry, was not intended to be pushed)Gravatar Hugo Herbelin2015-02-12
* Capital letter in plugins.Gravatar Hugo Herbelin2015-02-12
* Removing dead code.Gravatar Pierre-Marie Pédrot2015-02-02
* Fix previous commit on extraction.Gravatar Maxime Dénès2015-01-23
* Extraction: fix #3629.Gravatar Maxime Dénès2015-01-23
* Derive -> derive occurencesGravatar Pierre Boutillier2015-01-12
* Update headers.Gravatar Maxime Dénès2015-01-12
* Extraction: discard code unnecessary to fulfill a module signatureGravatar Pierre Letouzey2015-01-11
* Declarations.mli refactoring: module_type_body = module_bodyGravatar Pierre Letouzey2015-01-11
* Extraction: discard unnecessary code inside modules without signaturesGravatar Pierre Letouzey2015-01-11
* Extraction: no more ascii blob in type variables (fix #3227)Gravatar Pierre Letouzey2015-01-11
* Extraction : some more support functions for a future "Extraction Compute"Gravatar Pierre Letouzey2015-01-11
* Extraction: minor tweaks to ease ongoing experiments about LambdaGravatar Pierre Letouzey2015-01-11
* Avoiding introducing yet another convention in naming files.Gravatar Hugo Herbelin2015-01-08
* kernel/ind Change interface of declare_mind and declare_mutualGravatar Matthieu Sozeau2015-01-05
* fix bug #2447 in congruenceGravatar Pierre Corbineau2014-12-16
|\
* | fix bug #2447 in congruenceGravatar Pierre Corbineau2014-12-16
| * Getting rid of Exninfo hacks.Gravatar Pierre-Marie Pédrot2014-12-16
|/
* handling Functional Scheme for required but not imported modulesGravatar Julien Forest2014-12-11
* Switch the few remaining iso-latin-1 files to utf8Gravatar Pierre Letouzey2014-12-09
* Closing bug 3837Gravatar Julien Forest2014-12-08
* Moving change_in_concl, change_in_hyp, change_concl to Proofview.tactic.Gravatar Hugo Herbelin2014-12-07
* Fix order of arguments in Extract Constant for Pos.compare_cont.Gravatar Maxime Dénès2014-11-25
* Writing Tactics.keep in the new monad.Gravatar Pierre-Marie Pédrot2014-11-21
* Fixing side bug in db37c9f3f32ae7 delaying interpretation of theGravatar Hugo Herbelin2014-11-16
* Fixing Functional Induction when applied to an alias (reference manualGravatar Hugo Herbelin2014-11-07
* Removing the legacy intro tactic code.Gravatar Pierre-Marie Pédrot2014-11-07
* Writing the raw introduction tactic in the new monad.Gravatar Pierre-Marie Pédrot2014-11-05
* Writing rename_hyps in the new monad.Gravatar Pierre-Marie Pédrot2014-11-03
* Don't raise an error when printing intro-patterns in [functional induction].Gravatar Arnaud Spiwack2014-11-01
* Feedback message: hold extra info to help routingGravatar Enrico Tassi2014-10-31
* Haskell extraction: use explicit -XMagicHash instead of -fglasgow-extsGravatar Nickolai Zeldovich2014-10-28
* Haskell extraction: put unsafeCoerce type declaration laterGravatar Nickolai Zeldovich2014-10-28
* Removing an Evd.merge in Newring.Gravatar Pierre-Marie Pédrot2014-10-27
* Fix some typos in comments.Gravatar Guillaume Melquiond2014-10-27
* This commit introduces changes in induction and destruct.Gravatar Hugo Herbelin2014-10-25
* Change reduction_of_red_expr to return an e_reduction_function returningGravatar Matthieu Sozeau2014-10-24
* Bugfix 3604 : more robust Unix.lockfGravatar Frédéric Besson2014-10-22
* Proofview: split [V82] module into [Unsafe] and [V82].Gravatar Arnaud Spiwack2014-10-22
* Remove the deprecated open-constr based refine.Gravatar Arnaud Spiwack2014-10-22
* Lemmas/Pfedit: use full evar_map instead of universe contexts to start proofs.Gravatar Arnaud Spiwack2014-10-22
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-02 19:16:51 +0000