index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
plugins
/
funind
/
indfun.ml
Commit message (
Expand
)
Author
Age
*
Remove reference name type.
Maxime Dénès
2018-06-18
*
[api] Misctypes removal: several moves:
Emilio Jesus Gallego Arias
2018-06-12
*
Deprecate Typing.e_* functions
Gaëtan Gilbert
2018-05-14
*
[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.
Emilio Jesus Gallego Arias
2018-05-04
*
Evar maps contain econstrs.
Gaëtan Gilbert
2018-04-13
*
Correction of ugly message described in #4667
Julien Forest
2018-04-11
*
[ssreflect] Fix module scoping problems due to packing and mli files.
Emilio Jesus Gallego Arias
2018-03-10
*
[located] Push inner locations in `reference` to a CAst.t node.
Emilio Jesus Gallego Arias
2018-03-09
*
[located] More work towards using CAst.t
Emilio Jesus Gallego Arias
2018-03-09
*
[econstr] Continue consolidation of EConstr API under `interp`.
Emilio Jesus Gallego Arias
2018-02-28
*
[ast] Improve precision of Ast location recognition in serialization.
Emilio Jesus Gallego Arias
2018-02-22
*
Moving the argument of CProdN/CLambdaN from binder_expr to local_binder_expr.
Hugo Herbelin
2018-02-20
*
Use r.(p) syntax to print primitive projections.
Maxime Dénès
2018-01-30
*
Remove dead code from funind.
Maxime Dénès
2018-01-24
*
[flags] Make program_mode a parameter for commands in vernac.
Emilio Jesus Gallego Arias
2017-12-17
*
[vernac] Split `command.ml` into separate files.
Emilio Jesus Gallego Arias
2017-12-17
*
[econstr] Switch constrintern API to non-imperative style.
Emilio Jesus Gallego Arias
2017-12-15
*
[api] Deprecate Term destructors, move to Constr
Emilio Jesus Gallego Arias
2017-11-22
*
[printing] Deprecate all printing functions accessing the global proof.
Emilio Jesus Gallego Arias
2017-11-21
*
Making detyping potentially lazy.
Pierre-Marie Pédrot
2017-09-04
*
Detyping functions are now operating on EConstr.t.
Pierre-Marie Pédrot
2017-08-01
*
Removing template polymorphism for definitions.
Pierre-Marie Pédrot
2017-07-26
*
[API] Remove `open API` in ml files in favor of `-open API` flag.
Emilio Jesus Gallego Arias
2017-07-17
*
Safer API for Global.body_of_constant and variants.
Pierre-Marie Pédrot
2017-07-13
*
closing bug #5618 introduce by PR 828
Julien Forest
2017-06-29
*
closing bug #4250
Julien Forest
2017-06-23
*
Removing Proof_type from the API.
Pierre-Marie Pédrot
2017-06-16
*
Remove (useless) aliases from the API.
Matej Košík
2017-06-10
*
Put all plugins behind an "API".
Matej Kosik
2017-06-07
*
Remove the Sigma (monotonous state) API.
Maxime Dénès
2017-06-06
*
Merge PR#716: Don't double up on periods in anomalies
Maxime Dénès
2017-06-06
|
\
*
\
Merge PR#590: A more explicit algebraic type for evars of kind MatchingVar + ...
Maxime Dénès
2017-06-05
|
\
\
|
|
*
Drop '.' from CErrors.anomaly, insert it in args
Jason Gross
2017-06-02
|
|
/
|
/
|
|
*
Renaming allow_patvar flag of intern_gen into pattern_mode.
Hugo Herbelin
2017-05-31
*
|
Creating a module Nameops.Name extending module Names.Name.
Hugo Herbelin
2017-05-31
|
/
*
[cleanup] Unify all calls to the error function.
Emilio Jesus Gallego Arias
2017-05-27
*
[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-25
*
[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
*
[constrexpr] Make patterns use Loc.located for location information
Emilio Jesus Gallego Arias
2017-04-24
*
Merge PR#422: Supporting all kinds of binders, including 'pat, in syntax of r...
Maxime Dénès
2017-04-12
|
\
*
\
Merge branch 'trunk' into pr379
Maxime Dénès
2017-04-04
|
\
\
*
|
|
Using delayed universe instances in EConstr.
Pierre-Marie Pédrot
2017-04-01
|
*
|
Replacing "cast surgery" in LetIn by a proper field (see PR #404).
Hugo Herbelin
2017-03-24
|
*
|
Unifying standard "constr_level" names for constructors of local_binder_expr.
Hugo Herbelin
2017-03-24
|
*
|
Renaming local_binder into local_binder_expr.
Hugo Herbelin
2017-03-24
|
*
|
"Standardizing" the name LocalPatten into LocalRawPattern.
Hugo Herbelin
2017-03-24
[next]