aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2015-10-26Pcoq entries are given a proper module.Pierre-Marie Pédrot
2015-10-25Getting rid of the Atactic entry.Pierre-Marie Pédrot
2015-10-25Getting rid of the Agram entry.Pierre-Marie Pédrot
2015-10-22Using GADTs in Xmlprotocol.Pierre-Marie Pédrot
2015-10-21Pcoq.prod_entry_key now uses a GADT to statically enforce typedness.Pierre-Marie Pédrot
2015-10-21Turn Pcoq into a regular ML file.Pierre-Marie Pédrot
2015-10-21Expanding the grammar extensions of Pcoq.Pierre-Marie Pédrot
2015-10-21Removing the dependencies of Pcoq in IFDEF macros.Pierre-Marie Pédrot
2015-10-21Expliciting some uses of Compat module.Pierre-Marie Pédrot
2015-10-21Removing test for bug #3956.Pierre-Marie Pédrot
2015-10-20Proofview.Goal.sigma returns an indexed evarmap.Pierre-Marie Pédrot
2015-10-20Indexing Proofview.goals with a stage.Pierre-Marie Pédrot
2015-10-20Boxing the Goal.enter primitive into a record type.Pierre-Marie Pédrot
2015-10-20Renaming Goal.enter field into s_enter.Pierre-Marie Pédrot
2015-10-19Expliciting the uses of the old Tacmach API in Tactics.Pierre-Marie Pédrot
2015-10-19Removing some unsafe uses of monotonicity.Pierre-Marie Pédrot
2015-10-19Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-19Type delayed_open_constr is now monotonic.Pierre-Marie Pédrot
2015-10-19Categorizing debug messages as such + NonLogical uses loggers.Pierre Courtieu
2015-10-19Test for #4372 (anomaly in inversion in the presence of fake dependency).Hugo Herbelin
2015-10-19More monotonicity in Tactics.Pierre-Marie Pédrot
2015-10-19Turning anomaly into error for #4372 (weakness of inversion in theHugo Herbelin
2015-10-19Removing tclEVARS in various places.Pierre-Marie Pédrot
2015-10-19Reducing the uses of tclEVARS in Tactics by using monotonous functions.Pierre-Marie Pédrot
2015-10-19Adding a monotonic variant of Goal.enter and Goal.nf_enter.Pierre-Marie Pédrot
2015-10-19Function debug mode more formatted.Pierre Courtieu
2015-10-19Partly fixes #3225. Removed some old experimental stuff in funind.Pierre Courtieu
2015-10-19Fixed #4274, bad formatting of messages in emacs mode.Pierre Courtieu
2015-10-19Documenting the option "Strict Universe Declaration" in CHANGES.Pierre-Marie Pédrot
2015-10-18Making Evarutil.new_evar monotonous.Pierre-Marie Pédrot
2015-10-18Constraining refine to monotonic functions.Pierre-Marie Pédrot
2015-10-18Miscellaneous typos, spacing, US spelling in comments or variable names.Hugo Herbelin
2015-10-18Using "__" rather than this unelegant arbitrary "A" for the name of variables...Hugo Herbelin
2015-10-18Reference Manual: Applying standard style recommendation about notHugo Herbelin
2015-10-18Fixing #4198 (continued): not matching within the inner lambdas/let-insHugo Herbelin
2015-10-18Using appropriate lambda decomposition function counting let-ins whenHugo Herbelin
2015-10-18Adding a function to mirror decompose_prod_n_assum in that it counts let-ins,Hugo Herbelin
2015-10-18Adding a notion of monotonous evarmap.Pierre-Marie Pédrot
2015-10-17Clarifying and documenting the UState API.Pierre-Marie Pédrot
2015-10-17Dedicated file for universe unification context manipulation.Pierre-Marie Pédrot
2015-10-17Lemmas accept the Local flag.Pierre-Marie Pédrot
2015-10-17Test for bug #4325.Pierre-Marie Pédrot
2015-10-16Generalize fix for auto from PMP to eauto and typeclasses eauto.Matthieu Sozeau
2015-10-16Merge branch 'v8.5' into trunkMaxime Dénès
2015-10-16Hashcons bytecode generated by the VM.Pierre-Marie Pédrot
2015-10-16Exporting a purely functional interface to bytecode patching.Pierre-Marie Pédrot
2015-10-16Remove left2right reference from the kernel.Maxime Dénès
2015-10-16Merge hint lists instead of appending them. (Fix bug #3199)Guillaume Melquiond
2015-10-15Avoid dependency of the pretyper on C code.Maxime Dénès
2015-10-15Test file for #4346: Set is no longer of type TypeMaxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-30 04:24:39 +0000