aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
Commit message (Expand)AuthorAge
* Declarative mode: fix proof modes.Gravatar Arnaud Spiwack2015-03-31
* Declarative mode: fix vernac classification.Gravatar Arnaud Spiwack2015-03-31
* Declarative mode: plug the specialised printers back.Gravatar Arnaud Spiwack2015-03-31
* Correcting a bug introduced by universes polymorphismGravatar jforest2015-03-25
* correcting a bug with aliased when using Functional SchemeGravatar forest2015-03-25
* Avoid segfault from code extracted to ghc. (Fix for bug #1257)Gravatar Guillaume Melquiond2015-03-21
* Properly capitalize filenames when extracting to Haskell. (Fix for bug #3221)Gravatar Guillaume Melquiond2015-03-21
* Do not revert parameter lists when extracting singleton types to Haskell. (Fi...Gravatar Guillaume Melquiond2015-03-21
* Declarative mode: make it so that unfocussing can only be done for closed sub...Gravatar Arnaud Spiwack2015-03-13
* Declarative mode: remove dead code.Gravatar Arnaud Spiwack2015-03-13
* Declarative mode: remove a superfluous [set_proof_mode].Gravatar Arnaud Spiwack2015-03-13
* Declarative mode: fix the focus behaviour.Gravatar Arnaud Spiwack2015-03-13
* rewiring Czar printers that were disabledGravatar Pierre Corbineau2015-03-13
* Fix double print in decl_mode.Gravatar Enrico Tassi2015-03-11
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-12 14:05:59 +0000