aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/constrextern.ml
Commit message (Expand)AuthorAge
* A little reorganization of notations + a fix to #5608.Gravatar Hugo Herbelin2017-08-29
* Detyping functions are now operating on EConstr.t.Gravatar Pierre-Marie Pédrot2017-08-01
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Merge PR#719: Constrexpr.Numeral without bigintGravatar Maxime Dénès2017-06-15
|\
* \ Merge PR#765: Remove obsolete Show commandsGravatar Maxime Dénès2017-06-14
|\ \
* | | [print] Allow Selective Printing of NotationsGravatar Emilio Jesus Gallego Arias2017-06-14
| | * Constrexpr.Numeral stays uninterpreted (string+sign instead of BigInt.t)Gravatar Pierre Letouzey2017-06-14
| |/ |/|
| * Remove more dead code (follow-up of previous commit).Gravatar Théo Zimmermann2017-06-12
|/
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-06-08
|\
* \ 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
| |/ / |/| |
| * | Using a more explicit algebraic type for evars of kind "MatchingVar".Gravatar Hugo Herbelin2017-05-31
* | | Creating a module Nameops.Name extending module Names.Name.Gravatar Hugo Herbelin2017-05-31
|/ /
* | Merge PR#481: [option] Remove support for non-synchronous options.Gravatar Maxime Dénès2017-05-25
|\ \
| * | [option] Remove support for non-synchronous options.Gravatar Emilio Jesus Gallego Arias2017-05-24
| * | 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
* | | [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] 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
|/ /
* | 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
| | * Better support for printing constructors with let-ins.Gravatar Hugo Herbelin2017-04-07
| | * Fixing #4499 (not using unnamed record field in {| |} notation).Gravatar Hugo Herbelin2017-04-07
* | | Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-04-04
|\| |
| * | Replacing "cast surgery" in LetIn by a proper field (see PR #404).Gravatar Hugo Herbelin2017-03-24
| * | Using the same type of binders for interning and externing.Gravatar Hugo Herbelin2017-03-24
| * | Unifying standard "constr_level" names for constructors of local_binder_expr.Gravatar Hugo Herbelin2017-03-24
| * | "Standardizing" the name LocalPatten into LocalRawPattern.Gravatar Hugo Herbelin2017-03-24
* | | Namegen primitives now apply on evar constrs.Gravatar Pierre-Marie Pédrot2017-02-14
|/ /
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-17
|\|
| * Merge PR #310 into v8.6Gravatar Pierre-Marie Pédrot2016-10-17
| |\
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-12
|\| |
| * | Fixing a few confusions on the name of the beautify flag.Gravatar Hugo Herbelin2016-10-12
| | * Revert "Make the pretty printer resilient to incomplete nametab (progress on ...Gravatar Théo Zimmermann2016-10-06
* | | Revert "Merge remote-tracking branch 'github/pr/283' into trunk"Gravatar Maxime Dénès2016-09-22
* | | Rename Decl_kinds.binding_kind into Decls_kind.implicit_status.Gravatar Maxime Dénès2016-09-20
* | | Make the user_err header an optional parameter.Gravatar Emilio Jesus Gallego Arias2016-08-19
* | | Unify location handling of error functions.Gravatar Emilio Jesus Gallego Arias2016-08-19
|/ /
* | Some extra fixes in printing patterns in binders.Gravatar Hugo Herbelin2016-07-19
* | errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* | Adding ability to put any pattern in binders, prefixed by a quote.Gravatar Daniel de Rauglaudre2016-06-27
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-02 17:10:40 +0000