aboutsummaryrefslogtreecommitdiff
path: root/kernel/term_typing.mli
AgeCommit message (Expand)Author
2017-07-26Statically ensuring that inlined entries out of the kernel have no effects.Pierre-Marie Pédrot
2017-07-26Further simplication: do not recreate entries for side-effects.Pierre-Marie Pédrot
2017-07-26More precise type of entries capturing their lack of side-effects.Pierre-Marie Pédrot
2017-07-26More precise type for universe entries.Pierre-Marie Pédrot
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-03-23Documenting the API of side-effects.Pierre-Marie Pédrot
2017-03-23Making the side_effects type opaque.Pierre-Marie Pédrot
2017-01-20Do not add redundant side effects in tactic code.Pierre-Marie Pédrot
2016-06-18Moving the typing_flags to the environment.Pierre-Marie Pédrot
2016-06-16Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.Pierre-Marie Pédrot
2016-06-14Assume totality: dedicated type rather than boolArnaud Spiwack
2016-01-20Update copyright headers.Maxime Dénès
2015-10-29Cleanup API and comments of 908dcd613Enrico Tassi
2015-10-28Avoid type checking private_constants (side_eff) again during Qed (#4357).Enrico Tassi
2015-10-08Proof using: let-in policy, optional auto-clear, forward closure*Enrico Tassi
2015-09-25Add a field in `constant_body` to track constant whose well-foundedness is as...Arnaud Spiwack
2015-09-25Propagate `Guarded` flag from syntax to kernel.Arnaud Spiwack
2015-02-02Removing dead code.Pierre-Marie Pédrot
2015-01-12Update headers.Maxime Dénès
2014-11-20Exporting the function handling side-effects only applied to terms.Pierre-Marie Pédrot
2014-05-06- Fix bug preventing apply from unfolding Fixpoints.Matthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-02-26New compilation mode -vi2voEnrico Tassi
2014-01-05Proof_using: new syntax + suggestionEnrico Tassi
2013-08-08State Transaction Machinegareuselesinge
2013-05-09Use definition_entry to declare local definitionsgareuselesinge
2013-02-27Minor cleanup around Term_typingletouzey
2013-01-22New implementation of the conversion test, using normalization by evaluation tomdenes
2012-08-08Updating headers.herbelin
2011-12-12Proof using ...gareuselesinge
2011-04-03Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacksletouzey
2011-01-31A fine-grain control of inlining at functor application via priority levelsletouzey
2011-01-28Remove the "Boxed" syntaxes and the const_entry_boxed fieldletouzey
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-06-22New script dev/tools/change-header to automatically update Coq files headers.herbelin
2010-05-18Applicative commutative cuts in Fixpoint guard conditionpboutill
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-29Move from ocamlweb to ocamdoc to generate mli documentationpboutill
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2007-04-25New keyword "Inline" for Parameters and Axioms for automatic soubiran
2006-10-28Extension du polymorphisme de sorte au cas des définitions dans Type.herbelin
2006-10-27changement des _sym par _comm dans setoid_ringbgregoir
2004-10-20COMMITED BYTECODE COMPILERbarras
2004-07-16Nouvelle en-têteherbelin
2002-08-02Modules dans COQ\!\!\!\!coq
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 15:32:02 +0000