aboutsummaryrefslogtreecommitdiff
path: root/interp
AgeCommit message (Expand)Author
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-05Remove dead code and unused open.Maxime Dénès
2017-05-05Merge PR#558: Adding a fold_glob_constr_with_binders combinatorMaxime Dénès
2017-05-02Merge PR#582: Fix warningsMaxime Dénès
2017-04-28Revert "Renaming allow_patvar flag of intern_gen into pattern_mode."Maxime Dénès
2017-04-28Revert "Using a more explicit algebraic type for evars of kind "MatchingVar"."Maxime Dénès
2017-04-28Using a more explicit algebraic type for evars of kind "MatchingVar".Hugo Herbelin
2017-04-28Renaming allow_patvar flag of intern_gen into pattern_mode.Hugo Herbelin
2017-04-28Merge PR#531: Fixing bug #5420 and many similar bugs due to the presence of l...Maxime Dénès
2017-04-27Fix 4.04 warningsGaetan Gilbert
2017-04-27Warning 29: non escaped end of line may be non portableGaetan Gilbert
2017-04-27Remove unused [open] statementsGaetan Gilbert
2017-04-27Remove some unused values and typesGaetan Gilbert
2017-04-20correcting a typo in a commentMatej Kosik
2017-04-15Merge branch 'v8.6' into trunkMaxime Dénès
2017-04-13Adding a fold_glob_constr_with_binders combinator.Hugo Herbelin
2017-04-12Merge PR#441: Port Toplevel to the Stm APIMaxime Dénès
2017-04-12[flags] Documentation and a minor tweak.Emilio Jesus Gallego Arias
2017-04-12Merge PR#422: Supporting all kinds of binders, including 'pat, in syntax of r...Maxime Dénès
2017-04-09More explicit message when a {struct x} argument refers to a local definition.Hugo Herbelin
2017-04-05Fixing #5454 (an assert false with 'pat).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-24Renaming local_binder into local_binder_expr.Hugo Herbelin
2017-03-24Merging glob_binder and glob_decl.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
2017-03-24"Standardizing" the name LocalPatten into LocalRawPattern.Hugo Herbelin
2017-03-23Factorizing/unifying code in dealing with binders.Hugo Herbelin
2017-03-23Improving the API of constrexpr_ops.mli.Hugo Herbelin
2017-03-14[safe_string] interp/dumpglobEmilio Jesus Gallego Arias
2017-02-22Merge branch 'v8.6'Pierre-Marie Pédrot
2017-02-20Merge PR#189: Remove tabulation support from pretty-printing.Maxime Dénès
2017-02-14Merge branch 'master'.Pierre-Marie Pédrot
2017-02-14Namegen primitives now apply on evar constrs.Pierre-Marie Pédrot
2017-02-14Definining EConstr-based contexts.Pierre-Marie Pédrot
2017-02-14Removing various compatibility layers of tactics.Pierre-Marie Pédrot
2017-02-14Ltac now uses evar-based constrs.Pierre-Marie Pédrot
2017-02-14Reductionops now return EConstrs.Pierre-Marie Pédrot
2017-02-14Tactics API using EConstr.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 18:03:32 +0000