aboutsummaryrefslogtreecommitdiff
path: root/interp/constrintern.ml
AgeCommit message (Expand)Author
2017-06-06Merge PR#662: Fixing bug #5233 and another bug with implicit arguments + a sh...Maxime Dénès
2017-06-06Merge PR#716: Don't double up on periods in anomaliesMaxime Dénès
2017-06-05Merge PR#590: A more explicit algebraic type for evars of kind MatchingVar + ...Maxime Dénès
2017-06-02Drop '.' from CErrors.anomaly, insert it in argsJason Gross
2017-06-01Merge PR#696: Trunk+cleanup constr of globalMaxime Dénès
2017-06-01Merge PR#561: Improving the Name APIMaxime Dénès
2017-05-31Using a more explicit algebraic type for evars of kind "MatchingVar".Hugo Herbelin
2017-05-31Renaming allow_patvar flag of intern_gen into pattern_mode.Hugo Herbelin
2017-05-31Creating a module Nameops.Name extending module Names.Name.Hugo Herbelin
2017-05-31Renaming interp_rawcontext_evars using a more "standard" name.Hugo Herbelin
2017-05-31Locating error about clash between a inductive parameter and a bound variable.Hugo Herbelin
2017-05-31More precise on preventing clash between bound vars name and hidden impargs.Hugo Herbelin
2017-05-31Fixing a failure to interpret some local implicit arguments in Inductive.Hugo Herbelin
2017-05-30Support for using type information to infer more precise evar sources.Hugo Herbelin
2017-05-29Cleanup: removal of constr_of_global.Matthieu Sozeau
2017-05-29Merge PR#546: Fix for bug #4499 and other minor related bugsMaxime Dénès
2017-05-27[cleanup] Unify all calls to the error function.Emilio Jesus Gallego Arias
2017-05-25Merge PR#608: Allow Ltac2 as a pluginMaxime Dénès
2017-05-24[location] Renaming "CAst.ast" to "CAst.t"Matej Košík
2017-05-24Merge branch 'trunk' into located_switchEmilio Jesus Gallego Arias
2017-05-19Merge branch 'master' into ltac2-hooksPierre-Marie Pédrot
2017-05-17Merge branch 'v8.6'Pierre-Marie Pédrot
2017-05-17Merge PR#630: [interp] [ast] Make raw_cases_pattern_expr private + small cleanupMaxime Dénès
2017-05-16Fixing bug #5222 (anomaly with "`pat" in the presence of scope delimiters).Hugo Herbelin
2017-05-16Fixing a bug with nested "as" clauses in "match".Hugo Herbelin
2017-05-15[interp] Rework check for casts inside patterns.Emilio Jesus Gallego Arias
2017-05-15[interp] [ast] Make raw_cases_pattern_expr private.Emilio Jesus Gallego Arias
2017-05-15Typo in comments of constrintern.Hugo Herbelin
2017-05-03Allowing to pass arbitrary data in internalization environments.Pierre-Marie Pédrot
2017-04-27Warning 29: non escaped end of line may be non portableGaetan Gilbert
2017-04-27Remove unused [open] statementsGaetan Gilbert
2017-04-25[location] [ast] Port module AST to CAstEmilio Jesus Gallego Arias
2017-04-25[location] [ast] Switch Constrexpr AST to an extensible node type.Emilio Jesus Gallego Arias
2017-04-25[location] Make location optional in Loc.locatedEmilio Jesus Gallego Arias
2017-04-25[location] Remove Loc.ghost.Emilio Jesus Gallego Arias
2017-04-24[location] More located use.Emilio Jesus Gallego Arias
2017-04-24[location] Switch glob_constr to Loc.locatedEmilio Jesus Gallego Arias
2017-04-24[location] Move Glob_term.predicate_pattern to located.Emilio Jesus Gallego Arias
2017-04-24[location] Move Glob_term.cases_pattern to located.Emilio Jesus Gallego Arias
2017-04-24[location] Use Loc.located for constr_expr.Emilio Jesus Gallego Arias
2017-04-24[constrexpr] Make patterns use Loc.located for location informationEmilio Jesus Gallego Arias
2017-04-07Better support for printing constructors with let-ins.Hugo Herbelin
2017-04-04Merge branch 'trunk' into pr379Maxime Dénès
2017-03-24Merge branch 'trunk' into pr379Maxime Dénès
2017-03-24Replacing "cast surgery" in LetIn by a proper field (see PR #404).Hugo Herbelin
2017-03-24Using the same type of binders for interning and externing.Hugo Herbelin
2017-03-24Unifying standard "constr_level" names for constructors of local_binder_expr.Hugo Herbelin
2017-03-24Type extended_glob_local_binder now contains only glob_constr.Hugo Herbelin
2017-03-24Standardized the order of constructors for binders: Assum then Def.Hugo Herbelin
2017-03-24Cleaning phase around local binder at glob level:Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:08:54 +0000