index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
engine
Age
Commit message (
Expand
)
Author
2017-06-16
Squashed commit of the following:
Amin Timany
2017-06-16
Check subtyping of inductive types in Kernel
Amin Timany
2017-06-16
Using UInfoInd for universes in inductive types
Amin Timany
2017-06-16
New datastructure for universes of inductive types
Amin Timany
2017-06-14
Deprecate options that were introduced for compatibility with 8.4.
Guillaume Melquiond
2017-06-14
Remove support for Coq 8.4.
Guillaume Melquiond
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-02
Don't double up on periods in anomalies
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
Using EConstr and more invariants in record.ml.
Hugo Herbelin
2017-05-30
Support for using type information to infer more precise evar sources.
Hugo Herbelin
2017-05-29
tactics 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] Move `Coqlib` to `library/`.
Emilio Jesus Gallego Arias
2017-05-26
Merge PR#655: Extra functions exported in EConstr
Maxime Dénès
2017-05-25
Merge PR#481: [option] Remove support for non-synchronous options.
Maxime Dénès
2017-05-24
Merge branch 'trunk' into located_switch
Emilio Jesus Gallego Arias
2017-05-24
[option] Remove support for non-synchronous options.
Emilio Jesus Gallego Arias
2017-05-23
Merge PR#518: Faster universe unification
Maxime Dénès
2017-05-19
Exporting some functions of vars.ml as functions operating on EConstr.
Hugo Herbelin
2017-05-19
In EConstr, defining some "cast" functions earlier.
Hugo Herbelin
2017-05-19
Moving "sym" on "eq" type to lib/util.ml.
Hugo Herbelin
2017-05-03
Merge PR#411: Mention template polymorphism in the documentation.
Maxime Dénès
2017-05-02
Merge PR#582: Fix warnings
Maxime Dénès
2017-05-01
More consistent writing of de Bruijn.
Théo Zimmermann
2017-04-27
Fix 4.04 warnings
Gaetan Gilbert
2017-04-27
Remove unused [open] statements
Gaetan Gilbert
2017-04-27
Add [_] prefix to unused values which maybe should be kept
Gaetan Gilbert
2017-04-27
Remove some unused values and types
Gaetan Gilbert
2017-04-27
Fast path when checking equality of universe levels in UState.
Pierre-Marie Pédrot
2017-04-27
Code cleaning in unification algorithm for universes.
Pierre-Marie Pédrot
2017-04-25
Fix an optimization failure in tclPROGRESS.
Pierre-Marie Pédrot
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-20
"tclENV" is sexier, use it instead of "Env.get"
Matej Kosik
2017-04-20
reduce syntactic noise
Matej Kosik
2017-04-11
Update various comments to use "template polymorphism"
Gaetan Gilbert
2017-04-07
Merge branch 'master' into econstr
Pierre-Marie Pédrot
2017-04-01
Restore a fast path in EConstr instance normalization.
Pierre-Marie Pédrot
2017-04-01
Using delayed universe instances in EConstr.
Pierre-Marie Pédrot
2017-04-01
Actually exporting delayed universes in the EConstr implementation.
Pierre-Marie Pédrot
2017-03-31
Make the Constr.kind_of_term type parametric in sorts and universes.
Pierre-Marie Pédrot
2017-03-31
Ensuring proper cast invariants in EConstr.kind.
Pierre-Marie Pédrot
2017-03-31
Revert "Specially crafted EConstr.kind to be more efficient."
Pierre-Marie Pédrot
2017-03-30
Specially crafted EConstr.kind to be more efficient.
Pierre-Marie Pédrot
[next]
