aboutsummaryrefslogtreecommitdiff
path: root/plugins/cc/ccalgo.ml
AgeCommit message (Expand)Author
2019-03-20Stop accessing proof env via Pfedit in printersMaxime Dénès
2019-03-14Add relevance marks on binders.Gaëtan Gilbert
2018-11-23s/let _ =/let () =/ in some places (mostly goptions related)Gaëtan Gilbert
2018-11-07[CC plugin] Remove dead codeVincent Laporte
2018-09-26[print] Restrict use of "debug" Termops printer.Emilio Jesus Gallego Arias
2018-07-24Projections use index representationGaëtan Gilbert
2018-06-26Remove Sorts.contentsGaëtan Gilbert
2018-05-23Collecting Array.smart_* functions into a module Array.Smart.Hugo Herbelin
2018-03-27Congruence: Fixing a bug with native projections.Hugo Herbelin
2018-03-27Congruence: typography in a comment.Hugo Herbelin
2018-03-27Congruence: getting rid of a detour by the compatibility layer of proof engine.Hugo Herbelin
2018-02-27Update headers following #6543.Théo Zimmermann
2017-11-22[api] Deprecate Term destructors, move to ConstrEmilio Jesus Gallego Arias
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
2017-07-17[API] Remove `open API` in ml files in favor of `-open API` flag.Emilio Jesus Gallego Arias
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-16Removing Proof_type from the API.Pierre-Marie Pédrot
2017-06-10Remove (useless) aliases from the API.Matej Košík
2017-06-07Put all plugins behind an "API".Matej Kosik
2017-06-02Drop '.' from CErrors.anomaly, insert it in argsJason Gross
2017-05-24[option] Remove support for non-synchronous options.Emilio Jesus Gallego Arias
2017-02-14Merge branch 'master'.Pierre-Marie Pédrot
2017-02-14Removing various compatibility layers of tactics.Pierre-Marie Pédrot
2017-02-14Ltac now uses evar-based constrs.Pierre-Marie Pédrot
2017-02-14Tacmach API using EConstr.Pierre-Marie Pédrot
2016-12-12Extend Fast_typeops to be a replacement for TypeopsGaetan Gilbert
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-05-31Feedback cleanupEmilio Jesus Gallego Arias
2016-05-08Removing dead code and unused opens.Pierre-Marie Pédrot
2016-04-09Merge branch 'v8.5'Pierre-Marie Pédrot
2016-04-08Fixing a source of inefficiency and an artificial dependency in theDaniel de Rauglaudre
2016-02-09CLEANUP: Context.{Rel,Named}.Declaration.tMatej Kosik
2016-01-20Update copyright headers.Maxime Dénès
2015-10-02Univs: fix an evar leak in congruenceMatthieu Sozeau
2015-05-13Safer typing primitives.Pierre-Marie Pédrot
2015-01-12Update headers.Maxime Dénès
2014-12-16fix bug #2447 in congruencePierre Corbineau
2014-09-27Add a boolean to indicate the unfolding state of a primitive projection,Matthieu Sozeau
2014-06-07Adding a new Control file centralizing the control options of Coq.Pierre-Marie Pédrot
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-03-03Getting rid of generic hashes in cc plugin.Pierre-Marie Pédrot
2014-03-01Fixing pervasive comparisonsPierre-Marie Pédrot
2013-10-14Avoid polymorphic comparison (plugins/cc).xclerc
2013-09-27Removing a bunch of generic equalities.ppedrot
2013-08-25Added a more efficient way to recover the domain of a map.ppedrot
2013-07-29Tentative fix for #3054: we refresh universes in a term generatedppedrot
2013-04-29Splitting Term into five unrelated interfaces:ppedrot
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 9)letouzey
2013-01-29Fixed synchronicity of filter with evar context in new_goal_with.herbelin
2013-01-28Uniformization of the "anomaly" command.ppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:45:00 +0000