aboutsummaryrefslogtreecommitdiff
path: root/toplevel/lemmas.ml
AgeCommit message (Expand)Author
2014-04-25Adding a stm/ folder, as asked during last workgroup. It was essentially movingPierre-Marie Pédrot
2014-04-25Removing Autoinstance once and for all.Pierre-Marie Pédrot
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2014-01-04Lemmas: export standard proof terminatorEnrico Tassi
2014-01-04Proof_global: Simpler API for proof_terminatorEnrico Tassi
2013-12-24STM: capture type checking error (Closes: 3195)Enrico Tassi
2013-12-24Qed: feedback when type checking is doneEnrico Tassi
2013-12-04Fix Admitted.Arnaud Spiwack
2013-12-04Factoring(continued).Arnaud Spiwack
2013-12-04Refactoring: storing more information in the terminator closure.Arnaud Spiwack
2013-12-04The commands that initiate proofs are now in charge of what happens when proo...Arnaud Spiwack
2013-11-25Remove the Hiddentac module.Arnaud Spiwack
2013-11-02Makes the new Proofview.tactic the basic type of Ltac.aspiwack
2013-10-31Future: better doc + restore ~pure optimizationgareuselesinge
2013-10-23cList: a few alternative to hashtbl-based uniquize, distinct, subsetletouzey
2013-10-18declaration_hooks use Ephemerongareuselesinge
2013-10-18Future: ported to Ephemeron + exception enhancinggareuselesinge
2013-09-27Removing a bunch of generic equalities.ppedrot
2013-08-28Fixing bug #3083.ppedrot
2013-08-08get rid of closures in global/proof stategareuselesinge
2013-08-08State Transaction Machinegareuselesinge
2013-05-09Use definition_entry to declare local definitionsgareuselesinge
2013-05-09A uniformization step around understand_* and interp_* functions.herbelin
2013-04-29Merging Context and Sign.ppedrot
2013-04-02Revised infrastructure for lazy loading of opaque proofsletouzey
2013-03-11Added a Local Definition vernacular command. This type of definitionppedrot
2013-02-26kernel/declarations becomes a pure mliletouzey
2013-02-20Corrects bug #2959 (error during Qed leads to assertion failure).aspiwack
2013-01-28Uniformization of the "anomaly" command.ppedrot
2013-01-22New implementation of the conversion test, using normalization by evaluation tomdenes
2012-12-14Modulification of identifierppedrot
2012-11-26Monomorphization (toplevel)ppedrot
2012-11-08Monomorphized a lot of equalities over OCaml integers, thanks toppedrot
2012-10-06remove useless hidden_flag in TacMutual(Co)Fixletouzey
2012-09-18Cleaning interface of Util.ppedrot
2012-09-14Moving Utils.list_* to a proper CList module, which includes stdlibppedrot
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
2012-08-08Updating headers.herbelin
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
2012-06-01Getting rid of Pp.msgnl and Pp.message.ppedrot
2012-05-29global_reference migrated from Libnames to new Globnames, less deps in gramma...letouzey
2012-05-29New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstrletouzey
2012-05-29Decl_kinds becomes a pure mli file, remaining ops in new file kindops.mlletouzey
2012-03-02Noise for nothingpboutill
2011-12-17A pass on warning printings. Made systematic the use of msg_warning soherbelin
2011-12-12Proof using ...gareuselesinge
2011-10-05Fixing Implicit Tactic mode damaged by commit r14496 (see also bug #2612).herbelin
2011-04-13Revert "Add [Polymorphic] flag for defs"msozeau
2011-04-13- Remove create_evar_defsmsozeau
2011-04-13Add [Polymorphic] flag for defsmsozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-10 21:23:36 +0000