aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/command.ml
Commit message (Expand)AuthorAge
* Extend definition of inductives to include subtyping infoGravatar Amin Timany2017-06-16
* [proof] Deprecate redundant wrappers.Gravatar Emilio Jesus Gallego Arias2017-06-11
* Remove the Sigma (monotonous state) API.Gravatar Maxime Dénès2017-06-06
* Merge PR#662: Fixing bug #5233 and another bug with implicit arguments + a sh...Gravatar Maxime Dénès2017-06-06
|\
* | Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
* | Merge PR#696: Trunk+cleanup constr of globalGravatar Maxime Dénès2017-06-01
|\ \
* \ \ Merge PR#561: Improving the Name APIGravatar Maxime Dénès2017-06-01
|\ \ \
| * | | Creating a module Nameops.Name extending module Names.Name.Gravatar Hugo Herbelin2017-05-31
| | | * More precise on preventing clash between bound vars name and hidden impargs.Gravatar Hugo Herbelin2017-05-31
| | | * Fixing a failure to interpret some local implicit arguments in Inductive.Gravatar Hugo Herbelin2017-05-31
| | |/ | |/|
* / | Support for using type information to infer more precise evar sources.Gravatar Hugo Herbelin2017-05-30
|/ /
| * Command.ml cleanup: remove constr_of_global callsGravatar Matthieu Sozeau2017-05-29
|/
* 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] Deprecate redundant Coqlib functions.Gravatar Emilio Jesus Gallego Arias2017-05-27
|/
* Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
|\
| * Merge PR#582: Fix warningsGravatar Maxime Dénès2017-05-02
| |\
| * \ Merge PR#531: Fixing bug #5420 and many similar bugs due to the presence of l...Gravatar Maxime Dénès2017-04-28
| |\ \
| | | * Fix omitted labels in function callsGravatar 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] 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
| * | Removing tactic compatibility layer in Command.Gravatar Pierre-Marie Pédrot2017-04-24
|/ /
* | [flags] Deprecate is_silent/is_verbose in favor of single flag.Gravatar Emilio Jesus Gallego Arias2017-04-21
* | Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-04-15
* | Merge PR#422: Supporting all kinds of binders, including 'pat, in syntax of r...Gravatar Maxime Dénès2017-04-12
|\ \
| | * Fixing #5420 as well as many related bugs due to miscounting let-ins.Gravatar Hugo Herbelin2017-04-09
| | * Fixing several wrong computations of implicit arguments by positionGravatar Hugo Herbelin2017-04-09
| | * Minor cosmetic commit.Gravatar Hugo Herbelin2017-04-09
* | | Merge branch 'master' into econstrGravatar Pierre-Marie Pédrot2017-04-07
|\ \ \ | | |/ | |/|
| * | Merge PR#508: Optimize pending evarsGravatar Maxime Dénès2017-04-06
| |\ \
* | | | Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-04-04
|\| | |
* | | | Actually exporting delayed universes in the EConstr implementation.Gravatar Pierre-Marie Pédrot2017-04-01
* | | | Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-03-24
| * | | 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
|/ / /
| | * Improving the API of constrexpr_ops.mli.Gravatar Hugo Herbelin2017-03-23
| |/ |/|
| * Ensuring static invariants about handling of pending evars in Pretyping.Gravatar Pierre-Marie Pédrot2017-03-23
|/
* [future] Remove unused parameter greedy.Gravatar Emilio Jesus Gallego Arias2017-03-14
* [stm] Break stm/toplevel dependency loop.Gravatar Emilio Jesus Gallego Arias2017-02-15
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-24 13:23:21 +0000