aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)Gravatar Pierre Letouzey2016-07-03
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Merge branch 'reduction-flags' into trunkGravatar Maxime Dénès2016-07-01
|\
| * Add and document match, fix and cofix reduction flags.Gravatar Maxime Dénès2016-07-01
| * Make semantics of whd_zeta consistent with other whd_* functions.Gravatar Maxime Dénès2016-07-01
| * Separate flags for fix/cofix/match reduction and clean reduction function names.Gravatar Maxime Dénès2016-07-01
|/
* Fixing #4865 (deciding on which arguments to recompute scopes was not robust).Gravatar Hugo Herbelin2016-06-29
* Exporting section_segment_of_reference.Gravatar Hugo Herbelin2016-06-29
* Updated CHANGES about subst. More on recursive equations in reference manual.Gravatar Hugo Herbelin2016-06-29
* Merge branch 'programcases' into trunkGravatar Matthieu Sozeau2016-06-29
|\
| * Fixes in documentation.Gravatar Matthieu Sozeau2016-06-29
| * Program: cleanup in cases, add optionsGravatar Matthieu Sozeau2016-06-29
|/
* Merge branch 'bug4527' into trunkGravatar Matthieu Sozeau2016-06-29
|\
| * Univ: Use loc even if there are more unbound levelsGravatar Matthieu Sozeau2016-06-29
| * CHANGES: document fix for #4726 too.Gravatar Matthieu Sozeau2016-06-29
| * CHANGES: document fix for 4527 and compatibility.Gravatar Matthieu Sozeau2016-06-29
| * universes.ml: Minor code cleanupGravatar Matthieu Sozeau2016-06-29
| * Univs: Fix bug #4726Gravatar Matthieu Sozeau2016-06-29
| * Univs: add source locations of levelsGravatar Matthieu Sozeau2016-06-29
| * Univs: earlier errors for strict univ decls #4527Gravatar Matthieu Sozeau2016-06-29
|/
* Merge branch 'warnings' into trunkGravatar Maxime Dénès2016-06-29
|\
| * Fix issues in test-suite revealed by warnings.Gravatar Maxime Dénès2016-06-29
| * A new infrastructure for warnings.Gravatar Maxime Dénès2016-06-29
| * Add [Unset Printing Dependent Evars Line]Gravatar Jason Gross2016-06-29
* | Revert "A new infrastructure for warnings."Gravatar Maxime Dénès2016-06-28
* | Typeclasses: use once in by clause for typeclass eautoGravatar Matthieu Sozeau2016-06-28
* | Merge branch 'warnings' into trunkGravatar Maxime Dénès2016-06-28
|\ \
| * | A new infrastructure for warnings.Gravatar Maxime Dénès2016-06-28
|/ /
* | Merge remote-tracking branch 'github/pr/207' into trunkGravatar Maxime Dénès2016-06-28
|\ \ | |/ |/|
* | Finalizing the only printing feature.Gravatar Pierre-Marie Pédrot2016-06-28
|\ \
| * | Documenting the "only printing" notation flag.Gravatar Pierre-Marie Pédrot2016-06-28
| * | Adding a test-suite for the only printing flag.Gravatar Pierre-Marie Pédrot2016-06-28
| * | Properly handle the only printing flag in Reserved Notations.Gravatar Pierre-Marie Pédrot2016-06-28
| * | Properly handling the only printing flag when parsing rules already exist.Gravatar Pierre-Marie Pédrot2016-06-28
|/ /
* | Merge branch 'shrinkobl' into trunkGravatar Matthieu Sozeau2016-06-27
|\ \
| * | Update CHANGES and COMPATIBILITYGravatar Matthieu Sozeau2016-06-27
| * | Program: refine shrinking of obligationsGravatar Matthieu Sozeau2016-06-27
| * | Rework treatment of default transparency of obligationsGravatar Matthieu Sozeau2016-06-27
| * | Add Unset Shrink Abstract/Obligations in Coq85Gravatar Matthieu Sozeau2016-06-27
| * | Shrink Proofs/Obligations by default and deprecateGravatar Matthieu Sozeau2016-06-27
|/ /
* | Typeclasses: fix treatment of exceptions in compatGravatar Matthieu Sozeau2016-06-27
* | Typeclasses: mark unresolvable goals in new implementationGravatar Matthieu Sozeau2016-06-27
* | Fix off-by-1 bug in coq_makefileGravatar Matthieu Sozeau2016-06-27
* | We want tclORELSE to catch exceptions on backtrackingsGravatar Matthieu Sozeau2016-06-27
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-27
|\ \
* \ \ Merge remote-tracking branch 'github/pr/223' into feedback-locationsGravatar Maxime Dénès2016-06-27
|\ \ \
* | | | ssrmatching: avoid warnings about redundant typing clauses in ARGUMENT EXTENDGravatar Pierre Letouzey2016-06-27
* | | | Merge branch 'sort-fields' into trunkGravatar Maxime Dénès2016-06-27
|\ \ \ \
* \ \ \ \ Merge branch 'funpattern-tests' into trunk.Gravatar Maxime Dénès2016-06-27
|\ \ \ \ \
| | * | | | minor: comment on the meaning of the 'boolean' variableGravatar Gabriel Scherer2016-06-27
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-23 19:29:09 +0000