aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/constrintern.ml
Commit message (Expand)AuthorAge
* Merge PR #6185: [parser] Remove unnecessary statically initialized hook.Gravatar Maxime Dénès2017-11-21
|\
* \ Merge PR #6125: Fixing remaining problems with bug #5762 and PR #1120 (clause...Gravatar Maxime Dénès2017-11-20
|\ \
| | * [parser] Remove unnecessary statically initialized hook.Gravatar Emilio Jesus Gallego Arias2017-11-19
| |/ |/|
| * One more step in fixing #5762 ("where" clause).Gravatar Hugo Herbelin2017-11-14
* | [api] Another large deprecation, `Nameops`Gravatar Emilio Jesus Gallego Arias2017-11-13
|/
* Merge PR #1120: Fixing BZ#5762 (supporting implicit arguments in "where" clau...Gravatar Maxime Dénès2017-10-20
|\
| * Fixing #5762 (supporting imp. args. in "where" clause of an inductive def.).Gravatar Hugo Herbelin2017-10-05
* | Efficient fresh name generation relying on sets.Gravatar Pierre-Marie Pédrot2017-09-28
|/
* Making detyping potentially lazy.Gravatar Pierre-Marie Pédrot2017-09-04
* Remove understand_tcc_evars.Gravatar Maxime Dénès2017-08-01
* Fixing a little location bug with recursive binders.Gravatar Hugo Herbelin2017-07-18
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Merge PR#719: Constrexpr.Numeral without bigintGravatar Maxime Dénès2017-06-15
|\
| * Constrexpr.Numeral stays uninterpreted (string+sign instead of BigInt.t)Gravatar Pierre Letouzey2017-06-14
* | Remove support for Coq 8.2.Gravatar Guillaume Melquiond2017-06-14
|/
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-06-08
|\
* \ 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
|\ \ \ \ \
| | | * | | 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
| | |/ / | |/| |
* / | | 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#546: Fix for bug #4499 and other minor related bugsGravatar Maxime Dénès2017-05-29
| |\
* | | [cleanup] Unify all calls to the error function.Gravatar Emilio Jesus Gallego Arias2017-05-27
* | | Merge PR#608: Allow Ltac2 as a pluginGravatar Maxime Dénès2017-05-25
|\ \ \
* | | | [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
|\ \ \ \
| | * \ \ 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
| |/ / / /
| | | * / Allowing to pass arbitrary data in internalization environments.Gravatar Pierre-Marie Pédrot2017-05-03
| | |/ / | |/| |
| * | | Warning 29: non escaped end of line may be non portableGravatar Gaetan Gilbert2017-04-27
| * | | Remove unused [open] statementsGravatar Gaetan Gilbert2017-04-27
* | | | [location] [ast] Port module AST to CAstGravatar Emilio Jesus Gallego Arias2017-04-25
* | | | [location] [ast] Switch Constrexpr AST to an extensible node type.Gravatar Emilio Jesus Gallego Arias2017-04-25
* | | | [location] Make location optional in Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-25