| Commit message (Expand) | Author | Age |
|---|
| * | Restore reasonable performance by not allocating during universe checks, |  Matthieu Sozeau | 2014-05-06 |
| * | - Rename eq to equal in Univ, document new modules, set interfaces. | Matthieu Sozeau | 2014-05-06 |
| * | Fix interface for template polymorphism, cleaning up code in all typing algor... | Matthieu Sozeau | 2014-05-06 |
| * | Properly reinstate old-style polymorphism in the kernel and pretyping/retyping. | Matthieu Sozeau | 2014-05-06 |
| * | Initial work on reintroducing old-style polymorphism for compatibility (the s... | Matthieu Sozeau | 2014-05-06 |
| * | Correct rebase on STM code. Thanks to E. Tassi for help on dealing with | Matthieu Sozeau | 2014-05-06 |
| * | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau | 2014-05-06 |
| * | Fixing #3293 (eta-expansion at "match" printing time was failing |  Hugo Herbelin | 2014-04-28 |
| * | Adding a field ci_cstr_nargs to case_info and mind_consnrealargs to | Hugo Herbelin | 2014-04-28 |
| * | Fix a second, trickier, typo in Termops.eta_reduce_head. |  Arnaud Spiwack | 2014-04-25 |
| * | Fix a small typo in Termops.eta_reduce_head. | Arnaud Spiwack | 2014-04-25 |
| * | Better representation of evar filters: we represent the vacuous filters of |  Pierre-Marie Pédrot | 2014-04-23 |
| * | Removing dead code, thanks to new OCaml warnings and a bit of scripting. | Pierre-Marie Pédrot | 2014-04-23 |
| * | Readback for int31 values from native compiler. |  Maxime Dénès | 2014-04-09 |
| * | Fixing bug #3228 (fixing precedence of ltac variables over variables in env). | Hugo Herbelin | 2014-04-05 |
| * | Fixing #3262 which revealed a non-progressing, hence looping, | Hugo Herbelin | 2014-04-04 |
| * | Propagating conversion_problem towards (postponed) evar/evar problems. | Hugo Herbelin | 2014-04-01 |
| * | Fixing bug #2900 (evar/evar unif was supposed to be treated in | Hugo Herbelin | 2014-04-01 |
| * | Evarconv: exact_ise_stack looks to stack head before bodies or branches |  Pierre Boutillier | 2014-03-17 |
| * | consider_remaining_unif_problems respects Conv_oracle | Pierre Boutillier | 2014-03-16 |
| * | Changing Retrokwnoledge entry type from kind_of_term to constr. It seems it had | Pierre-Marie Pédrot | 2014-03-14 |
| * | Evarconv unification respects Conv_oracle | Pierre Boutillier | 2014-03-10 |
| * | MaybeFlexible semantic changes | Pierre Boutillier | 2014-03-10 |
| * | Remove some dead-code (thanks to ocaml warnings) |  Pierre Letouzey | 2014-03-05 |
| * | Remove many superfluous 'open' indicated by ocamlc -w +33 | Pierre Letouzey | 2014-03-05 |
| * | Goptions do not rely anymore on generic equality. | Pierre-Marie Pédrot | 2014-03-03 |
| * | Matching --> ConstrMatching (was clashing with OCaml's compiler-libs) | Pierre Letouzey | 2014-03-02 |
| * | Grammar.cma with less deps (Glob_ops and Nameops) after moving minor code | Pierre Letouzey | 2014-03-02 |
| * | Adding an equality function over glob_constr | Pierre-Marie Pédrot | 2014-03-02 |
| * | Fixing pervasive comparisons | Pierre-Marie Pédrot | 2014-03-01 |
| * | Fixing bad comparison in Detyping. | Pierre-Marie Pédrot | 2014-03-01 |
| * | Removing Pervasives.compare in Termdn. | Pierre-Marie Pédrot | 2014-02-28 |
| * | Removing a Pervasives.compare in Term_dnet. | Pierre-Marie Pédrot | 2014-02-28 |
| * | Fix bug 3245: 'simpl nomatch' argument annotation makes cbn go into an infini... | Pierre Boutillier | 2014-02-28 |
| * | Dead code elimionation in reductionops | Pierre Boutillier | 2014-02-28 |
| * | Tacinterp: refactoring using Monad. | Arnaud Spiwack | 2014-02-27 |
| * | Code refactoring thanks to the new Monad module. | Arnaud Spiwack | 2014-02-27 |
| * | remoteCounter: backup/restore |  Enrico Tassi | 2014-02-26 |
| * | IStream: change type of thunk, spare allocations. | Arnaud Spiwack | 2014-02-24 |
| * | Ensuring that the module Stack is opaque inside Reductionops. | Pierre-Marie Pédrot | 2014-02-24 |
| * | cbn understands Arguments | Pierre Boutillier | 2014-02-24 |
| * | Simpl_behaviour becomes Reductionops.ReductionBehaviour | Pierre Boutillier | 2014-02-24 |
| * | Create Debug Unification option | Pierre Boutillier | 2014-02-24 |
| * | No more translation array <-> list in Reductionops.Stack | Pierre Boutillier | 2014-02-24 |
| * | Reductionops.Stack.strip* are ready to deal with Shift | Pierre Boutillier | 2014-02-24 |
| * | Reductionops.Stack.app_node is secret | Pierre Boutillier | 2014-02-24 |
| * | app_node, stack, state printers | Pierre Boutillier | 2014-02-24 |
| * | Stack operations of Reductionops in Reductionops.Stack | Pierre Boutillier | 2014-02-24 |
| * | TC: honor the use_typeclasses flag in pretyping | Enrico Tassi | 2014-02-12 |
| * | Made Pre_env.lazy_val opaque. | Pierre-Marie Pédrot | 2014-02-11 |
Matthieu Sozeau
Hugo Herbelin
Arnaud Spiwack
Pierre-Marie Pédrot
Maxime Dénès
Pierre Boutillier
Pierre Letouzey
Enrico Tassi