aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Expand)Author
2014-05-06Proper calculation of constructor levels, forgetting the level of lets.Matthieu Sozeau
2014-05-06Retype application of fix_proto to get the right universes in ProgramMatthieu Sozeau
2014-05-06Fix restrict_universe_context removing some universes that do appear in the t...Matthieu Sozeau
2014-05-06Fix declarations of monomorphic assumptionsMatthieu Sozeau
2014-05-06Allow records whose sort is defined by a constant.Matthieu Sozeau
2014-05-06- Fix RecTutorial, and mutual induction schemes getting the wrong names.Matthieu Sozeau
2014-05-06Fix program Fixpoint not taking care of universes.Matthieu Sozeau
2014-05-06- Fix eq_constr_universes restricted to Sorts.equalMatthieu Sozeau
2014-05-06- Fix bug preventing apply from unfolding Fixpoints.Matthieu Sozeau
2014-05-06Adapt universe polymorphic branch to new handling of futures for delayed proofs.Matthieu Sozeau
2014-05-06Fix context forgetting universes (temporary, the fix is not exactly right).Matthieu Sozeau
2014-05-06Adapt Y. Bertot's path on private inductives (now the keyword is "Private").Yves Bertot
2014-05-06- Fix handling of polymorphic inductive elimination schemes.Matthieu Sozeau
2014-05-06Various fixes of universe polymorphism and projections when they're set.Matthieu Sozeau
2014-05-06- Fix Check to use the constraints inferred during type inference.Matthieu Sozeau
2014-05-06- Rename eq to equal in Univ, document new modules, set interfaces.Matthieu Sozeau
2014-05-06Initial work on reintroducing old-style polymorphism for compatibility (the s...Matthieu Sozeau
2014-05-06Correct rebase on STM code. Thanks to E. Tassi for help on dealing withMatthieu Sozeau
2014-05-06Rework handling of universes on top of the STM, allowing for delayedMatthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-05-01Allowing the "Declare Instance" command anywhere. This was artificiallyPierre-Marie Pédrot
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-04-25Removing useless try-with clauses in Goal.enter variants.Pierre-Marie Pédrot
2014-04-25Fixing various backtrace recordings.Pierre-Marie Pédrot
2014-04-23Removing dead code, thanks to new OCaml warnings and a bit of scripting.Pierre-Marie Pédrot
2014-04-10Have the feedback bus as a backend for dumping globs.Carst Tankink
2014-04-09Revert "Revert part of eba6b75 as coq_makefile ignores -I if it overlaps with...Pierre Boutillier
2014-04-08Add an option -Q (tentative name).Guillaume Melquiond
2014-04-07Revert part of eba6b75 as coq_makefile ignores -I if it overlaps with -R. (Fi...Guillaume Melquiond
2014-04-06Change handling of loadpath and mlpath.Guillaume Melquiond
2014-04-02STM: be more resilient to explicit Back + Sideff commands (closes: 3251)Enrico Tassi
2014-03-31Removing dead code in Tactics.Pierre-Marie Pédrot
2014-03-26Adding a tclEFFECTS primitive allowing to push STM side-effects in tactics.Pierre-Marie Pédrot
2014-03-26STM: when an error occurs in a worker send back a bunch of statesEnrico Tassi
2014-03-19Adding a Print Strategy vernacular command. It allows to check thePierre-Marie Pédrot
2014-03-18STM: make the slave start from the most recent known stateEnrico Tassi
2014-03-18STM: make -async-proofs on work from coqc tooEnrico Tassi
2014-03-13fix compilation with ocaml < 4Enrico Tassi
2014-03-13STM: perspective (tell the scheduler what the user sees)Enrico Tassi
2014-03-13STM: move out a couple of submodulesEnrico Tassi
2014-03-12Stm: smarter delegation policyEnrico Tassi
2014-03-11vi2vo: universes handling finally fixedEnrico Tassi
2014-03-07Using Hashmaps by default in constant and inductive maps. This changes fold andPierre-Marie Pédrot
2014-03-06Lets coqtop use a slashVirgile Prevosto
2014-03-05Using HMaps in Safe_env.environments, hopefully improving performances.Pierre-Marie Pédrot
2014-03-05Remove some dead-code (thanks to ocaml warnings)Pierre Letouzey
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2014-03-04STM: fix Show ScriptEnrico Tassi
2014-03-04STM: when finish a task hcons universe constraintsEnrico Tassi
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 00:50:42 +0000