| Age | Commit message (Expand) | Author |
|---|
| 2014-10-20 | A patch for printing "match" when constructors are defined with let-in | Hugo Herbelin |
| 2014-10-11 | Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different name | Matthieu Sozeau |
| 2014-09-13 | Providing a -type-in-type option for collapsing the universe hierarchy. | Hugo Herbelin |
| 2014-09-04 | Print [Variant] types with the keyword [Variant]. | Arnaud Spiwack |
| 2014-08-28 | Change the way primitive projections are declared to the kernel. | Matthieu Sozeau |
| 2014-08-14 | Fix non-printing of coercions for primitive projections (fixes bug #3433). | Matthieu Sozeau |
| 2014-08-05 | A new step in the new "standard" naming policy for propositional hypotheses | Hugo Herbelin |
| 2014-08-03 | Move to a representation of universe polymorphic constants using indices for ... | Matthieu Sozeau |
| 2014-08-01 | Continuing (incomplete) cleaning of Inductiveops. | Hugo Herbelin |
| 2014-08-01 | A tentative uniform naming policy in module Inductiveops. | Hugo Herbelin |
| 2014-07-03 | Cleanup code related to the constraint solving, which sits now outside the | Matthieu Sozeau |
| 2014-06-28 | Quick fix of bug #2996 continued (case of inductive types). | Hugo Herbelin |
| 2014-06-26 | Deactivate the "Standard Propositions Naming" flag, source of a lot of | Hugo Herbelin |
| 2014-06-25 | Fix type_of_inductive_knowing_conclusion, relying on an actually broken univ_... | Matthieu Sozeau |
| 2014-06-17 | Removing dead code. | Pierre-Marie Pédrot |
| 2014-06-04 | - Fix hashing of levels to get the "right" order in universe contexts etc... | Matthieu Sozeau |
| 2014-06-01 | Use of "H"-based names for propositional hypotheses obtained by | Hugo Herbelin |
| 2014-05-09 | Reuse universe level substitutions for template polymorphism, fixing performance | Matthieu Sozeau |
| 2014-05-06 | Initial work on reintroducing old-style polymorphism for compatibility (the s... | Matthieu Sozeau |
| 2014-05-06 | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau |
| 2014-04-28 | Adding a field ci_cstr_nargs to case_info and mind_consnrealargs to | Hugo Herbelin |
| 2013-10-24 | More monomorphic List.mem + List.assoc + ... | letouzey |
| 2013-04-29 | Splitting Term into five unrelated interfaces: | ppedrot |
| 2013-03-23 | Minor code cleaning in CArray / CList. | ppedrot |
| 2013-03-20 | Check a list length before doing a List.chop (fix #3000) | letouzey |
| 2013-02-26 | kernel/declarations becomes a pure mli | letouzey |
| 2013-01-28 | Uniformization of the "anomaly" command. | ppedrot |
| 2012-11-22 | Monomorphization (pretyping) | ppedrot |
| 2012-09-18 | Cleaning interface of Util. | ppedrot |
| 2012-09-14 | As r15801: putting everything from Util.array_* to CArray.*. | ppedrot |
| 2012-09-14 | Moving Utils.list_* to a proper CList module, which includes stdlib | ppedrot |
| 2012-09-14 | This patch removes unused "open" (automatically generated from | regisgia |
| 2012-09-14 | The new ocaml compiler (4.00) has a lot of very cool warnings, | regisgia |
| 2012-08-08 | Updating headers. | herbelin |
| 2012-03-02 | "Let in" in pattern hell, one more iteration | pboutill |
| 2012-03-02 | Noise for nothing | pboutill |
| 2012-03-01 | Univ: a univ_depends function to avoid a hack in Inductiveops | letouzey |
| 2012-01-16 | Inductiveops.nb_*{,_env} cleaning | pboutill |
| 2010-12-18 | Univ.constraints made fully abstract instead of being a Set of abstract stuff | letouzey |
| 2010-09-24 | Some dead code removal, thanks to Oug analyzer | letouzey |
| 2010-07-24 | Updated all headers for 8.3 and trunk | herbelin |
| 2010-05-18 | Applicative commutative cuts in Fixpoint guard condition | pboutill |
| 2010-04-29 | Remove the svn-specific $Id$ annotations | letouzey |
| 2010-03-12 | fixed confusion between number of cstr arguments and number of pattern variab... | barras |
| 2009-11-09 | A bit of cleaning around name generation + creation of dedicated file namegen.ml | herbelin |
| 2009-10-21 | This big commit addresses two problems: | soubiran |
| 2009-09-17 | Delete trailing whitespaces in all *.{v,ml*} files | glondu |
| 2009-09-13 | - Inductive types in the "using" option of auto/eauto/firstorder are | herbelin |
| 2009-08-11 | Ensures that let-in's in arities of inductive types work well. Maybe not | herbelin |
| 2009-08-02 | Improved parameterization of Coq: | herbelin |
