aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp
Commit message (Expand)AuthorAge
* Renaming allow_patvar flag of intern_gen into pattern_mode.Gravatar Hugo Herbelin2017-05-31
* 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
| | | * | | Remove some unused values and typesGravatar 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
* | | | | [location] Remove Loc.ghost.Gravatar Emilio Jesus Gallego Arias2017-04-25
* | | | | [location] Use located in misctypes.Gravatar Emilio Jesus Gallego Arias2017-04-24
* | | | | [location] More located use.Gravatar Emilio Jesus Gallego Arias2017-04-24
* | | | | [location] Switch glob_constr to Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-24
* | | | | [location] Move Glob_term.predicate_pattern to located.Gravatar Emilio Jesus Gallego Arias2017-04-24
* | | | | [location] Move Glob_term.cases_pattern to located.Gravatar Emilio Jesus Gallego Arias2017-04-24
* | | | | [location] Use Loc.located for constr_expr.Gravatar Emilio Jesus Gallego Arias2017-04-24
* | | | | [constrexpr] Make patterns use Loc.located for location informationGravatar Emilio Jesus Gallego Arias2017-04-24
|/ / / /
* | | | correcting a typo in a commentGravatar Matej Kosik2017-04-20
* | | | Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-04-15
|\ \ \ \ | | |_|/ | |/| |
| | | * Adding a fold_glob_constr_with_binders combinator.Gravatar Hugo Herbelin2017-04-13
* | | | Merge PR#441: Port Toplevel to the Stm APIGravatar Maxime Dénès2017-04-12
|\ \ \ \
| * | | | [flags] Documentation and a minor tweak.Gravatar Emilio Jesus Gallego Arias2017-04-12