aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Expand)AuthorAge
* Merge remote-tracking branch 'origin/v8.5' into trunkGravatar Hugo Herbelin2015-09-09
|\
| * Documenting the code when preference is given to expansion of defaultGravatar Hugo Herbelin2015-09-08
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-08-05
|\|
| * Continuing 817308ab (use ltac env for terms in ltac context) + fixGravatar Hugo Herbelin2015-08-02
| * Reverting 16 last commits, committed mistakenly using the wrong push command.Gravatar Hugo Herbelin2015-08-02
| * Documenting in passing.Gravatar Hugo Herbelin2015-08-02
| * Hopefully clearer printing of stack when debugging evarconv unification.Gravatar Hugo Herbelin2015-08-02
| * Cosmetic changes in evarconv.ml: hopefully more regular names and formGravatar Hugo Herbelin2015-08-02
| * Cosmetic changes in evarconv.ml: hopefully more regular form andGravatar Hugo Herbelin2015-08-02
| * Cosmetic changes in evarconv.ml: hopefully using better self-documenting names.Gravatar Hugo Herbelin2015-08-02
| * Evarconv.ml: small cut-elimination, saving useless zip.Gravatar Hugo Herbelin2015-08-02
| * Cosmetic in evarconv.ml: naming a local function for better readibility.Gravatar Hugo Herbelin2015-08-02
| * Fixing #4221 (interpreting bound variables using ltac env was possiblyGravatar Hugo Herbelin2015-08-02
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-07-27
|\|
| * Fixing bug #4303: Anomaly: Uncaught exception Invalid_argument.Gravatar Pierre-Marie Pédrot2015-07-21
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-07-18
|\|
| * Refining 71def2f8 on too strong occur-check limiting evar-evarGravatar Hugo Herbelin2015-07-16
| * Slight improvement in naming anonymous variables in error messages:Gravatar Hugo Herbelin2015-07-16
| * Fixing #4177 (find_projectable was liable to ask to instantiate an evar twice).Gravatar Hugo Herbelin2015-07-16
| * Fixing bug #4240 (closure_of_filter was not ensuring refinement ofGravatar Hugo Herbelin2015-07-16
| * Fix universe instantiation with canonical structures.Gravatar Maxime Dénès2015-07-16
| * Continuing 93579407, spotting other potential sources of anomalyGravatar Hugo Herbelin2015-07-16
| * Fixing anomaly #3743 while printing an error message involving evar constraints.Gravatar Hugo Herbelin2015-07-16
| * Continuing handling of NoCoercion after df6e64fd28 and 4944b5e72.Gravatar Hugo Herbelin2015-07-10
| * Option -type-in-type: added support in checker and making it contaminatingGravatar Hugo Herbelin2015-07-10
| * Make retyping of projections more resilient to wrong environment.Gravatar Maxime Dénès2015-07-09
| * Univs: bug fix.Gravatar Matthieu Sozeau2015-07-07
* | Merge branch 'v8.5' into trunkGravatar Maxime Dénès2015-07-06
|\|
| * Fix handling of primitive projections in VM.Gravatar Maxime Dénès2015-07-05
| * Assumptions: more informative print for False axiom (Close: #4054)Gravatar Enrico Tassi2015-06-29
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-06-28
|\|
| * Fix incompleteness of conversion used by evarconvGravatar Matthieu Sozeau2015-06-28
| * Fix bug #4254 with the help of J.H. JourdanGravatar Matthieu Sozeau2015-06-26
* | Merge remote-tracking branch 'forge/v8.5'Gravatar Pierre Boutillier2015-06-22
|\|
| * Make normalization of primitive projections in native_compute the same as wit...Gravatar Maxime Dénès2015-06-08
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-06-01
|\|
| * Fixup for 866c41bGravatar Enrico Tassi2015-05-28
| * Fix bug #4159Gravatar Matthieu Sozeau2015-05-27
| * Adding an extensible global state to evarmaps.Gravatar Pierre-Marie Pédrot2015-05-19
| * Make Coercion.inh_app_fun respect its specification.Gravatar Pierre-Marie Pédrot2015-05-15
* | Merge v8.5 into trunkGravatar Hugo Herbelin2015-05-15
|\|
| * Disable precompilation for native_compute by default.Gravatar Guillaume Melquiond2015-05-14
| * Safer typing primitives.Gravatar Pierre-Marie Pédrot2015-05-13
| * Fix for a second avatar of bug #4234.Gravatar Pierre-Marie Pédrot2015-05-13
| * Better fixing #4198 such that the term to match is looked for beforeGravatar Hugo Herbelin2015-05-13
| * Fixing bug #4234.Gravatar Pierre-Marie Pédrot2015-05-12
| * Code factorization in Constr_matching.Gravatar Pierre-Marie Pédrot2015-05-10
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-05-05
|\|
| * Remove almost all the uses of string concatenation when building error messages.Gravatar Guillaume Melquiond2015-04-23
| * Tactical `progress` compares term up to potentially equalisable universes.Gravatar Arnaud Spiwack2015-04-22