| Commit message (Expand) | Author | Age |
... | |
* | Fix performance problem with unification in presence of universes (bug #3302)... | Matthieu Sozeau | 2014-05-08 |
* | - Add a primitive tclEVARUNIVERSECONTEXT to reset the universe context of an ... | Matthieu Sozeau | 2014-05-08 |
* | Moving Dnet-related code to tactics/. | Pierre-Marie Pédrot | 2014-05-08 |
* | - Fix treatment of global universe constraints which should be passed along | Matthieu Sozeau | 2014-05-06 |
* | Find a more efficient fix for dealing with template universes: | Matthieu Sozeau | 2014-05-06 |
* | Try a new way of handling template universe levels | Matthieu Sozeau | 2014-05-06 |
* | - Add back some compatibility functions to avoid rewriting plugins. | Matthieu Sozeau | 2014-05-06 |
* | Keep track of universes on coercion applications even if they're not polymorp... | Matthieu Sozeau | 2014-05-06 |
* | Refresh some universes in cases.ml as they might appear in the term. | Matthieu Sozeau | 2014-05-06 |
* | Correct universe handling in program coercions (bug #2378). | Matthieu Sozeau | 2014-05-06 |
* | Fix set_leq_sort refusing max(u,Set) <= Set when u is flexible. | Matthieu Sozeau | 2014-05-06 |
* | - Fix arity handling in retyping (de Bruijn bug!) | Matthieu Sozeau | 2014-05-06 |
* | Allow records whose sort is defined by a constant. | Matthieu Sozeau | 2014-05-06 |
* | - Fixes for canonical structure resolution (check that the initial term indee... | Matthieu Sozeau | 2014-05-06 |
* | - Fix eq_constr_universes restricted to Sorts.equal | Matthieu Sozeau | 2014-05-06 |
* | Remove postponed constraints (unused) | Matthieu Sozeau | 2014-05-06 |
* | - Fix bug preventing apply from unfolding Fixpoints. | Matthieu Sozeau | 2014-05-06 |
* | Adapt universe polymorphic branch to new handling of futures for delayed proofs. | Matthieu Sozeau | 2014-05-06 |
* | Honor the Opaque flag for projections in simpl. | Matthieu Sozeau | 2014-05-06 |
* | In case two constants/vars/rels are _not_ defined, force unification of unive... | Matthieu Sozeau | 2014-05-06 |
* | Adapt Y. Bertot's path on private inductives (now the keyword is "Private"). | Yves Bertot | 2014-05-06 |
* | - Fix comparison of universes. | Matthieu Sozeau | 2014-05-06 |
* | 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 |