aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2014-06-11In generalized rewrite, avoid retyping completely and constantly the conclusi...Matthieu Sozeau
2014-06-11fix handling of side effects in abstract (fixes QArithSternBrocot)Enrico Tassi
2014-06-10Fixing Sorting Universes in a world where le and lt constraints may bePierre-Marie Pédrot
2014-06-10Compute the trace of a universe inconsistency only when explicitly requiredPierre-Marie Pédrot
2014-06-10Made explanations for universe inconsistencies optional. They are only usedPierre-Marie Pédrot
2014-06-10Specialize the type of [Univ.compare_neq] so that it is clear it is only usedPierre-Marie Pédrot
2014-06-10Removing dead code in checker/univ.ml.Pierre-Marie Pédrot
2014-06-10Removing explanations of universe inconsistencies from the checker. TheyPierre-Marie Pédrot
2014-06-10Imperatively check touched universes in compare_neq functions. This ensuresPierre-Marie Pédrot
2014-06-10Providing the checker with its own version of the Univ file.Pierre-Marie Pédrot
2014-06-10- Fix substitution of universes which needlessly hashconsed existing universes.Matthieu Sozeau
2014-06-10Oops, one refactoring was not compiled.Matthieu Sozeau
2014-06-10More cleanup/reorganizing of univ.ml to separate constraint/universe handling...Matthieu Sozeau
2014-06-10Fix module order in printers.mllibMatthieu Sozeau
2014-06-10Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un...Matthieu Sozeau
2014-06-10Remove unused function in univMatthieu Sozeau
2014-06-10Merge branch 'hott-test-suite-progress' of https://github.com/JasonGross/coq ...Matthieu Sozeau
2014-06-09Flattening Level module structure in Univ.Pierre-Marie Pédrot
2014-06-08Mark some progress in the HoTT/coq test-suiteJason Gross
2014-06-08Adding a toplevel option allowing to deactivate the term sharing in kernelPierre-Marie Pédrot
2014-06-08Moving hook code from Future to Lemmas. This seemed to disrupt compilation ofPierre-Marie Pédrot
2014-06-08Fix canonical structure resolution in unification (bug found in Ssreflect).Matthieu Sozeau
2014-06-08Timeout implementation for Windows based on threads.Pierre-Marie Pédrot
2014-06-08Enforce a correct exception handling in declaration_hooksEnrico Tassi
2014-06-08ind_tables: always declare side effects (Closes: HOTT#110)Enrico Tassi
2014-06-08STM: handle "Time Abort" correctly (Closes: 3332)Enrico Tassi
2014-06-08Function in Univ uselessly exported.Pierre-Marie Pédrot
2014-06-07Removing 'open Univ' from checker.Pierre-Marie Pédrot
2014-06-07Moving a Thread.yield in check_interrupt.Pierre-Marie Pédrot
2014-06-07Adding a new Control file centralizing the control options of Coq.Pierre-Marie Pédrot
2014-06-06Preserve compatibility on examples such as "intros []." on goals suchHugo Herbelin
2014-06-06Dead code.Hugo Herbelin
2014-06-06Fixes the lost evars when interpreting a change with pattern tactic.Arnaud Spiwack
2014-06-06Remove the syntax [Vernac1. Vernac2. … Vernacn. ].Arnaud Spiwack
2014-06-06Make kernel reduction code parametric over the handling of universes,Matthieu Sozeau
2014-06-06Moving the [split] tactic out of the AST.Pierre-Marie Pédrot
2014-06-05Dedicated map module for type universes. It uses hashmaps, which arePierre-Marie Pédrot
2014-06-05Removing dead code from Univ.Pierre-Marie Pédrot
2014-06-04Make standard library independent of the names generated byHugo Herbelin
2014-06-04Make standard library independent of the names generated byHugo Herbelin
2014-06-04Collecting in Namegen those conventional default names that are used in diffe...Hugo Herbelin
2014-06-04Small lemma about Relations.Hugo Herbelin
2014-06-04Remove spurious Show in script.Matthieu Sozeau
2014-06-04- Better parsing and printing of named universes: Type{ident} and foo@{(ident...Matthieu Sozeau
2014-06-04Fix canonical structure resolution (makes test-suite files go through again).Matthieu Sozeau
2014-06-04- Allow parsing of @const@{instance} for specifying universe instances of pol...Matthieu Sozeau
2014-06-04- Force every universe level to be >= Prop, so one cannot "go under" it anymore.Matthieu Sozeau
2014-06-04- Fix hashing of levels to get the "right" order in universe contexts etc...Matthieu Sozeau
2014-06-04Fix handling of anonymous Type in template universe polymorphic inductivesMatthieu Sozeau
2014-06-04- Keep all <= constraints during refinement, otherwise we might miss collapse...Matthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 22:55:21 +0000