aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Expand)Author
2015-03-25Correcting a bug introduced by universes polymorphismjforest
2015-03-25correcting a bug with aliased when using Functional Schemeforest
2015-03-21Avoid segfault from code extracted to ghc. (Fix for bug #1257)Guillaume Melquiond
2015-03-21Properly capitalize filenames when extracting to Haskell. (Fix for bug #3221)Guillaume Melquiond
2015-03-21Do not revert parameter lists when extracting singleton types to Haskell. (Fi...Guillaume Melquiond
2015-03-13Declarative mode: make it so that unfocussing can only be done for closed sub...Arnaud Spiwack
2015-03-13Declarative mode: remove dead code.Arnaud Spiwack
2015-03-13Declarative mode: remove a superfluous [set_proof_mode].Arnaud Spiwack
2015-03-13Declarative mode: fix the focus behaviour.Arnaud Spiwack
2015-03-13rewiring Czar printers that were disabledPierre Corbineau
2015-03-11Fix double print in decl_mode.Enrico Tassi
2015-03-11admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Enrico Tassi
2015-03-03Fix bug #3732: firstorder was using detyping to build existentialMatthieu Sozeau
2015-03-03Fix bug #3590, keeping evars that are not turned into named metas byMatthieu Sozeau
2015-02-27Removing the unused field ltacrecvars of tactic internalization.Pierre-Marie Pédrot
2015-02-24Calling coq references lazily in plugin cc so as to support static linking of...Hugo Herbelin
2015-02-23Fix some typos in comments.Guillaume Melquiond
2015-02-14Fixing OCaml 3.12 compilation.Pierre-Marie Pédrot
2015-02-14Abstract: "Qed export ident, .., ident" to preserve v8.4 behaviorEnrico Tassi
2015-02-12Univs: fix bug #3978: carry around the universe context used toMatthieu Sozeau
2015-02-12Revert "Capital letter in plugins." (Sorry, was not intended to be pushed)Hugo Herbelin
2015-02-12Capital letter in plugins.Hugo Herbelin
2015-02-02Removing dead code.Pierre-Marie Pédrot
2015-01-23Fix previous commit on extraction.Maxime Dénès
2015-01-23Extraction: fix #3629.Maxime Dénès
2015-01-12Derive -> derive occurencesPierre Boutillier
2015-01-12Update headers.Maxime Dénès
2015-01-11Extraction: discard code unnecessary to fulfill a module signaturePierre Letouzey
2015-01-11Declarations.mli refactoring: module_type_body = module_bodyPierre Letouzey
2015-01-11Extraction: discard unnecessary code inside modules without signaturesPierre Letouzey
2015-01-11Extraction: no more ascii blob in type variables (fix #3227)Pierre Letouzey
2015-01-11Extraction : some more support functions for a future "Extraction Compute"Pierre Letouzey
2015-01-11Extraction: minor tweaks to ease ongoing experiments about LambdaPierre Letouzey
2015-01-08Avoiding introducing yet another convention in naming files.Hugo Herbelin
2015-01-05kernel/ind Change interface of declare_mind and declare_mutualMatthieu Sozeau
2014-12-16fix bug #2447 in congruencePierre Corbineau
2014-12-16fix bug #2447 in congruencePierre Corbineau
2014-12-16Getting rid of Exninfo hacks.Pierre-Marie Pédrot
2014-12-11handling Functional Scheme for required but not imported modulesJulien Forest
2014-12-09Switch the few remaining iso-latin-1 files to utf8Pierre Letouzey
2014-12-08Closing bug 3837Julien Forest
2014-12-07Moving change_in_concl, change_in_hyp, change_concl to Proofview.tactic.Hugo Herbelin
2014-11-25Fix order of arguments in Extract Constant for Pos.compare_cont.Maxime Dénès
2014-11-21Writing Tactics.keep in the new monad.Pierre-Marie Pédrot
2014-11-16Fixing side bug in db37c9f3f32ae7 delaying interpretation of theHugo Herbelin
2014-11-07Fixing Functional Induction when applied to an alias (reference manualHugo Herbelin
2014-11-07Removing the legacy intro tactic code.Pierre-Marie Pédrot
2014-11-05Writing the raw introduction tactic in the new monad.Pierre-Marie Pédrot
2014-11-03Writing rename_hyps in the new monad.Pierre-Marie Pédrot
2014-11-01Don't raise an error when printing intro-patterns in [functional induction].Arnaud Spiwack
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-08 12:08:07 +0000