aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp
Commit message (Expand)AuthorAge
* Merge PR#662: Fixing bug #5233 and another bug with implicit arguments + a sh...Gravatar Maxime Dénès2017-06-06
|\
* \ Merge PR#716: Don't double up on periods in anomaliesGravatar Maxime Dénès2017-06-06
|\ \
* \ \ Merge PR#590: A more explicit algebraic type for evars of kind MatchingVar + ...Gravatar Maxime Dénès2017-06-05
|\ \ \
| | * | Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
| |/ / |/| |
* | | Merge PR#696: Trunk+cleanup constr of globalGravatar Maxime Dénès2017-06-01
|\ \ \
* \ \ \ Merge PR#561: Improving the Name APIGravatar Maxime Dénès2017-06-01
|\ \ \ \
* \ \ \ \ Merge PR#694: Fixing #5523 (missing support for complex constructions in recu...Gravatar Maxime Dénès2017-06-01
|\ \ \ \ \
| | | | * | Using a more explicit algebraic type for evars of kind "MatchingVar".Gravatar Hugo Herbelin2017-05-31
| | | | * | Renaming allow_patvar flag of intern_gen into pattern_mode.Gravatar Hugo Herbelin2017-05-31
| | * | | | Creating a module Nameops.Name extending module Names.Name.Gravatar Hugo Herbelin2017-05-31
| | * | | | Renaming interp_rawcontext_evars using a more "standard" name.Gravatar Hugo Herbelin2017-05-31
| | | |/ / | | |/| |
| | | | * Locating error about clash between a inductive parameter and a bound variable.Gravatar Hugo Herbelin2017-05-31
| | | | * More precise on preventing clash between bound vars name and hidden impargs.Gravatar Hugo Herbelin2017-05-31
| | | | * Fixing a failure to interpret some local implicit arguments in Inductive.Gravatar Hugo Herbelin2017-05-31
| | | |/ | | |/|
| * | | Fixing #5523 (missing support for complex constructions in recursive notations).Gravatar Hugo Herbelin2017-05-31
| * | | Fixing a too lax constraint for finding recursive binder part of a notation.Gravatar Hugo Herbelin2017-05-31
| |/ /
* / / Support for using type information to infer more precise evar sources.Gravatar Hugo Herbelin2017-05-30
|/ /
| * Cleanup: removal of constr_of_global.Gravatar Matthieu Sozeau2017-05-29
|/
* Merge PR#512: [cleanup] Unify all calls to the error function.Gravatar Maxime Dénès2017-05-29
|\
| * [cleanup] Unify all calls to the error function.Gravatar Emilio Jesus Gallego Arias2017-05-27
* | [coqlib] Move `Coqlib` to `library/`.Gravatar Emilio Jesus Gallego Arias2017-05-27
* | [coqlib] Deprecate redundant Coqlib functions.Gravatar Emilio Jesus Gallego Arias2017-05-27
|/
* Merge PR#637: Short cleaning of the interpretation path for constr_with_bindingsGravatar Maxime Dénès2017-05-25
|\
* \ Merge PR#608: Allow Ltac2 as a pluginGravatar Maxime Dénès2017-05-25
|\ \
* \ \ Merge PR#481: [option] Remove support for non-synchronous options.Gravatar Maxime Dénès2017-05-25
|\ \ \
* | | | [location] Fix warnings.Gravatar Emilio Jesus Gallego Arias2017-05-24
* | | | [location] Renaming "CAst.ast" to "CAst.t"Gravatar Matej Košík2017-05-24
* | | | Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
|\ \ \ \
| | * | | [option] Remove support for non-synchronous options.Gravatar Emilio Jesus Gallego Arias2017-05-24
| |/ / /
| | | * Clarifying the interpretation path for the "constr_with_binding" argument.Gravatar Hugo Herbelin2017-05-22
| | |/ | |/|
| | * Merge branch 'master' into ltac2-hooksGravatar Pierre-Marie Pédrot2017-05-19
| | |\ | | |/ | |/|
| * | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-05-17
| |\ \
| * \ \ Merge PR#630: [interp] [ast] Make raw_cases_pattern_expr private + small cleanupGravatar Maxime Dénès2017-05-17
| |\ \ \
| | | * | Fixing bug #5222 (anomaly with "`pat" in the presence of scope delimiters).Gravatar Hugo Herbelin2017-05-16
| | | * | Fixing a bug with nested "as" clauses in "match".Gravatar Hugo Herbelin2017-05-16
| | * | | [interp] Rework check for casts inside patterns.Gravatar Emilio Jesus Gallego Arias2017-05-15
| | * | | [interp] [ast] Make raw_cases_pattern_expr private.Gravatar Emilio Jesus Gallego Arias2017-05-15
| * | | | Typo in comments of constrintern.Gravatar Hugo Herbelin2017-05-15
| |/ / /
| * | | Remove dead code and unused open.Gravatar Maxime Dénès2017-05-05
| * | | Merge PR#558: Adding a fold_glob_constr_with_binders combinatorGravatar Maxime Dénès2017-05-05
| |\ \ \
| | | | * Allowing to pass arbitrary data in internalization environments.Gravatar Pierre-Marie Pédrot2017-05-03
| | |_|/ | |/| |
| * | | Merge PR#582: Fix warningsGravatar Maxime Dénès2017-05-02
| |\ \ \
| * | | | Revert "Renaming allow_patvar flag of intern_gen into pattern_mode."Gravatar Maxime Dénès2017-04-28
| * | | | Revert "Using a more explicit algebraic type for evars of kind "MatchingVar"."Gravatar Maxime Dénès2017-04-28
| * | | | Using a more explicit algebraic type for evars of kind "MatchingVar".Gravatar Hugo Herbelin2017-04-28
| * | | | Renaming allow_patvar flag of intern_gen into pattern_mode.Gravatar Hugo Herbelin2017-04-28
| * | | | Merge PR#531: Fixing bug #5420 and many similar bugs due to the presence of l...Gravatar Maxime Dénès2017-04-28
| |\ \ \ \
| | | * | | Fix 4.04 warningsGravatar Gaetan Gilbert2017-04-27
| | | * | | Warning 29: non escaped end of line may be non portableGravatar Gaetan Gilbert2017-04-27
| | | * | | Remove unused [open] statementsGravatar Gaetan Gilbert2017-04-27
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-29 19:08:06 +0000