index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
vernac
/
command.ml
Age
Commit message (
Expand
)
Author
2017-09-04
Making detyping potentially lazy.
Pierre-Marie Pédrot
2017-08-31
Merge PR #980: Adding combinators + a canonical renaming in List, Option, Name
Maxime Dénès
2017-08-29
Adapting code to renaming fold_map/fold_map' into fold_left_map/fold_right_map
Hugo Herbelin
2017-08-01
Remove understand_tcc_evars.
Maxime Dénès
2017-07-04
Merge branch 'v8.6'
Pierre-Marie Pédrot
2017-07-04
Bump year in headers.
Pierre-Marie Pédrot
2017-06-20
[vernac] Remove forward hooks from Obligations.
Emilio Jesus Gallego Arias
2017-06-20
[vernac] Remove unused hooks.
Emilio Jesus Gallego Arias
2017-06-16
Clean up universes of constants and inductives
Amin Timany
2017-06-16
Fix bugs and add an option for cumulativity
Amin Timany
2017-06-16
Fix bugs
Amin Timany
2017-06-16
Squashed commit of the following:
Amin Timany
2017-06-16
Change the place of inference after sect discharge
Amin Timany
2017-06-16
Subtyping inference for inductoves and records
Amin Timany
2017-06-16
Add subtyping inference for inductive types
Amin Timany
2017-06-16
Using UInfoInd for universes in inductive types
Amin Timany
2017-06-16
Extend definition of inductives to include subtyping info
Amin Timany
2017-06-11
[proof] Deprecate redundant wrappers.
Emilio Jesus Gallego Arias
2017-06-06
Remove the Sigma (monotonous state) API.
Maxime Dénès
2017-06-06
Merge PR#662: Fixing bug #5233 and another bug with implicit arguments + a sh...
Maxime Dénès
2017-06-02
Drop '.' from CErrors.anomaly, insert it in args
Jason Gross
2017-06-01
Merge PR#696: Trunk+cleanup constr of global
Maxime Dénès
2017-06-01
Merge PR#561: Improving the Name API
Maxime Dénès
2017-05-31
Creating a module Nameops.Name extending module Names.Name.
Hugo Herbelin
2017-05-31
More precise on preventing clash between bound vars name and hidden impargs.
Hugo Herbelin
2017-05-31
Fixing a failure to interpret some local implicit arguments in Inductive.
Hugo Herbelin
2017-05-30
Support for using type information to infer more precise evar sources.
Hugo Herbelin
2017-05-29
Command.ml cleanup: remove constr_of_global calls
Matthieu Sozeau
2017-05-29
Merge PR#512: [cleanup] Unify all calls to the error function.
Maxime Dénès
2017-05-27
[cleanup] Unify all calls to the error function.
Emilio Jesus Gallego Arias
2017-05-27
[coqlib] Deprecate redundant Coqlib functions.
Emilio Jesus Gallego Arias
2017-05-24
Merge branch 'trunk' into located_switch
Emilio Jesus Gallego Arias
2017-05-02
Merge PR#582: Fix warnings
Maxime Dénès
2017-04-28
Merge PR#531: Fixing bug #5420 and many similar bugs due to the presence of l...
Maxime Dénès
2017-04-27
Fix omitted labels in function calls
Gaetan Gilbert
2017-04-25
[location] [ast] Port module AST to CAst
Emilio 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.located
Emilio Jesus Gallego Arias
2017-04-25
[location] Remove Loc.ghost.
Emilio Jesus Gallego Arias
2017-04-24
[location] Switch glob_constr to Loc.located
Emilio Jesus Gallego Arias
2017-04-24
[location] Use Loc.located for constr_expr.
Emilio Jesus Gallego Arias
2017-04-24
Removing tactic compatibility layer in Command.
Pierre-Marie Pédrot
2017-04-21
[flags] Deprecate is_silent/is_verbose in favor of single flag.
Emilio Jesus Gallego Arias
2017-04-15
Merge branch 'v8.6' into trunk
Maxime Dénès
2017-04-12
Merge PR#422: Supporting all kinds of binders, including 'pat, in syntax of r...
Maxime Dénès
2017-04-09
Fixing #5420 as well as many related bugs due to miscounting let-ins.
Hugo Herbelin
2017-04-09
Fixing several wrong computations of implicit arguments by position
Hugo Herbelin
2017-04-09
Minor cosmetic commit.
Hugo Herbelin
2017-04-07
Merge branch 'master' into econstr
Pierre-Marie Pédrot
2017-04-06
Merge PR#508: Optimize pending evars
Maxime Dénès
[next]
