aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind/indfun.ml
Commit message (Expand)AuthorAge
* Remove reference name type.Gravatar Maxime Dénès2018-06-18
* [api] Misctypes removal: several moves:Gravatar Emilio Jesus Gallego Arias2018-06-12
* Deprecate Typing.e_* functionsGravatar Gaëtan Gilbert2018-05-14
* [api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Gravatar Emilio Jesus Gallego Arias2018-05-04
* Evar maps contain econstrs.Gravatar Gaëtan Gilbert2018-04-13
* Correction of ugly message described in #4667Gravatar Julien Forest2018-04-11
* [ssreflect] Fix module scoping problems due to packing and mli files.Gravatar Emilio Jesus Gallego Arias2018-03-10
* [located] Push inner locations in `reference` to a CAst.t node.Gravatar Emilio Jesus Gallego Arias2018-03-09
* [located] More work towards using CAst.tGravatar Emilio Jesus Gallego Arias2018-03-09
* [econstr] Continue consolidation of EConstr API under `interp`.Gravatar Emilio Jesus Gallego Arias2018-02-28
* [ast] Improve precision of Ast location recognition in serialization.Gravatar Emilio Jesus Gallego Arias2018-02-22
* Moving the argument of CProdN/CLambdaN from binder_expr to local_binder_expr.Gravatar Hugo Herbelin2018-02-20
* Use r.(p) syntax to print primitive projections.Gravatar Maxime Dénès2018-01-30
* Remove dead code from funind.Gravatar Maxime Dénès2018-01-24
* [flags] Make program_mode a parameter for commands in vernac.Gravatar Emilio Jesus Gallego Arias2017-12-17
* [vernac] Split `command.ml` into separate files.Gravatar Emilio Jesus Gallego Arias2017-12-17
* [econstr] Switch constrintern API to non-imperative style.Gravatar Emilio Jesus Gallego Arias2017-12-15
* [api] Deprecate Term destructors, move to ConstrGravatar Emilio Jesus Gallego Arias2017-11-22
* [printing] Deprecate all printing functions accessing the global proof.Gravatar Emilio Jesus Gallego Arias2017-11-21
* Making detyping potentially lazy.Gravatar Pierre-Marie Pédrot2017-09-04
* Detyping functions are now operating on EConstr.t.Gravatar Pierre-Marie Pédrot2017-08-01
* Removing template polymorphism for definitions.Gravatar Pierre-Marie Pédrot2017-07-26
* [API] Remove `open API` in ml files in favor of `-open API` flag.Gravatar Emilio Jesus Gallego Arias2017-07-17
* Safer API for Global.body_of_constant and variants.Gravatar Pierre-Marie Pédrot2017-07-13
* closing bug #5618 introduce by PR 828Gravatar Julien Forest2017-06-29
* closing bug #4250Gravatar Julien Forest2017-06-23
* Removing Proof_type from the API.Gravatar Pierre-Marie Pédrot2017-06-16
* Remove (useless) aliases from the API.Gravatar Matej Košík2017-06-10
* Put all plugins behind an "API".Gravatar Matej Kosik2017-06-07
* Remove the Sigma (monotonous state) API.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
| |/ |/|
| * 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
|/
* [cleanup] Unify all calls to the error function.Gravatar Emilio Jesus Gallego Arias2017-05-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] Switch glob_constr to Loc.locatedGravatar 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#422: Supporting all kinds of binders, including 'pat, in syntax of r...Gravatar Maxime Dénès2017-04-12
|\
* \ Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-04-04
|\ \
* | | Using delayed universe instances in EConstr.Gravatar Pierre-Marie Pédrot2017-04-01
| * | Replacing "cast surgery" in LetIn by a proper field (see PR #404).Gravatar Hugo Herbelin2017-03-24
| * | Unifying standard "constr_level" names for constructors of local_binder_expr.Gravatar Hugo Herbelin2017-03-24
| * | Renaming local_binder into local_binder_expr.Gravatar Hugo Herbelin2017-03-24
| * | "Standardizing" the name LocalPatten into LocalRawPattern.Gravatar Hugo Herbelin2017-03-24
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-13 19:24:20 +0000