index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
plugins
/
funind
/
glob_termops.ml
Commit message (
Expand
)
Author
Age
*
[located] More work towards using CAst.t
Emilio Jesus Gallego Arias
2018-03-09
*
pretyping: restore API understand_judgment_tcc (now understand_tcc_ty)
Enrico Tassi
2018-02-19
*
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
*
Efficient fresh name generation relying on sets.
Pierre-Marie Pédrot
2017-09-28
*
Making detyping potentially lazy.
Pierre-Marie Pédrot
2017-09-04
*
closing bug 5315
Julien Forest
2017-07-29
*
[API] Remove `open API` in ml files in favor of `-open API` flag.
Emilio Jesus Gallego Arias
2017-07-17
*
Merge PR#513: A fix to #5414 (ident bound by ltac names now known for "match").
Maxime Dénès
2017-06-14
|
\
*
|
Remove (useless) aliases from the API.
Matej Košík
2017-06-10
|
*
A fix to #5414 (ident bound by ltac names now known for "match").
Hugo Herbelin
2017-06-09
|
/
*
Put all plugins behind an "API".
Matej Kosik
2017-06-07
*
Merge PR#716: Don't double up on periods in anomalies
Maxime Dénès
2017-06-06
|
\
|
*
Drop '.' from CErrors.anomaly, insert it in args
Jason Gross
2017-06-02
*
|
solving implicit resolution in Function
Julien Forest
2017-06-01
|
/
*
[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] Make location optional in Loc.located
Emilio Jesus Gallego Arias
2017-04-25
*
[location] Switch glob_constr to Loc.located
Emilio Jesus Gallego Arias
2017-04-24
*
[location] Move Glob_term.cases_pattern to located.
Emilio Jesus Gallego Arias
2017-04-24
*
Replacing "cast surgery" in LetIn by a proper field (see PR #404).
Hugo Herbelin
2017-03-24
*
Make the user_err header an optional parameter.
Emilio Jesus Gallego Arias
2016-08-19
*
errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...
Pierre Letouzey
2016-07-03
*
Add syntax for naming new goals in refine: writing ?[id] instead of _
Hugo Herbelin
2014-09-30
*
Revert specific syntax for primitive projections, avoiding ugly
Matthieu Sozeau
2014-09-17
*
A tentative uniform naming policy in module Inductiveops.
Hugo Herbelin
2014-08-01
*
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-05-06
*
Adding generic solvers to term holes. For now, no resolution mechanism nor
Pierre-Marie Pédrot
2013-11-27
*
More monomorphic List.mem + List.assoc + ...
letouzey
2013-10-24
*
Removing a bunch of generic equalities.
ppedrot
2013-09-27
*
Restrict (try...with...) to avoid catching critical exn (part 9)
letouzey
2013-03-13
*
invalid_arg instead of raise (Invalid_argement ...)
letouzey
2013-03-12
*
Uniformization of the "anomaly" command.
ppedrot
2013-01-28
*
New implementation of the conversion test, using normalization by evaluation to
mdenes
2013-01-22
*
Modulification of identifier
ppedrot
2012-12-14
*
Partial revert of Yann commit in order to use CLib.List when opening
ppedrot
2012-09-14
*
This patch removes unused "open" (automatically generated from
regisgia
2012-09-14
*
Added an indirection with respect to Loc in Compat. As many [open Compat]
ppedrot
2012-06-22
*
global_reference migrated from Libnames to new Globnames, less deps in gramma...
letouzey
2012-05-29
*
locus.mli for occurrences+clauses, misctypes.mli for various little things
letouzey
2012-05-29
*
Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evd
letouzey
2012-05-29
*
Noise for nothing
pboutill
2012-03-02
*
Remove dynamic stuff from constr_expr and glob_constr
glondu
2011-10-28
*
Rename mkR* smart constructors (mostly in funind)
glondu
2010-12-25
*
More {raw => glob} changes for consistency
glondu
2010-12-24
*
Rename files in funind to respect new conventions
glondu
2010-12-24