index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
/
detyping.mli
Commit message (
Expand
)
Author
Age
*
Remove reference name type.
Maxime Dénès
2018-06-18
*
[api] Move universe syntax to `Glob_term`
Emilio Jesus Gallego Arias
2018-05-08
*
Detyping: Adding a variant of share_names for patterns.
Hugo Herbelin
2018-03-28
*
Update headers following #6543.
Théo Zimmermann
2018-02-27
*
In printing, factorizing "match" clauses with same right-hand side.
Hugo Herbelin
2017-12-12
*
[api] Move structures deprecated in the API to the core.
Emilio Jesus Gallego Arias
2017-11-06
*
[general] Remove Econstr dependency from `intf`
Emilio Jesus Gallego Arias
2017-10-25
*
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
*
deprecate Pp.std_ppcmds type alias
Matej Košík
2017-07-27
*
Bump year in headers.
Pierre-Marie Pédrot
2017-07-04
*
[location] [ast] Port module AST to CAst
Emilio Jesus Gallego Arias
2017-04-25
*
[location] Switch glob_constr to Loc.located
Emilio Jesus Gallego Arias
2017-04-24
*
Namegen primitives now apply on evar constrs.
Pierre-Marie Pédrot
2017-02-14
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-21
|
\
|
*
Update copyright headers.
Maxime Dénès
2016-01-20
*
|
CLEANUP: kernel/context.ml{,i}
Matej Kosik
2016-01-11
*
|
Univs: proper printing of global and local universe names (only
Matthieu Sozeau
2015-01-18
|
*
Univs: proper printing of global and local universe names (only
Matthieu Sozeau
2015-01-17
|
/
*
Fix issue in printing due to de Bruijn bug when constructing compatibility
Matthieu Sozeau
2015-01-13
*
Update headers.
Maxime Dénès
2015-01-12
*
Reactivating option "Set Printing Existential Instances" for asking printing ...
Hugo Herbelin
2014-12-04
*
Printing function for [uconstr].
Arnaud Spiwack
2014-11-19
*
A patch for printing "match" when constructors are defined with let-in
Hugo Herbelin
2014-10-20
*
Revert specific syntax for primitive projections, avoiding ugly
Matthieu Sozeau
2014-09-17
*
Referring to evars by names. Added a parser for evars (but parsing of
Hugo Herbelin
2014-09-12
*
Remove many superfluous 'open' indicated by ocamlc -w +33
Pierre Letouzey
2014-03-05
*
Goptions do not rely anymore on generic equality.
Pierre-Marie Pédrot
2014-03-03
*
Adding generic solvers to term holes. For now, no resolution mechanism nor
Pierre-Marie Pédrot
2013-11-27
*
Merging Context and Sign.
ppedrot
2013-04-29
*
Splitting Term into five unrelated interfaces:
ppedrot
2013-04-29
*
Modulification of name
ppedrot
2012-12-18
*
Modulification of identifier
ppedrot
2012-12-14
*
Updating headers.
herbelin
2012-08-08
*
Added an indirection with respect to Loc in Compat. As many [open Compat]
ppedrot
2012-06-22
*
No more Univ in grammar.cma
letouzey
2012-05-29
*
locus.mli for occurrences+clauses, misctypes.mli for various little things
letouzey
2012-05-29
*
Glob_term.predicate_pattern: No number of parameters with letins.
pboutill
2012-03-02
*
Noise for nothing
pboutill
2012-03-02
*
Allow "|_=>_" in "match" in patterns, no more forced enumeration of constructors
letouzey
2011-11-07
*
This is exactly the structure needed to handle controlling printing
herbelin
2011-07-16
*
More {raw => glob} changes for consistency
glondu
2010-12-24
*
Rename rawterm.ml into glob_term.ml
glondu
2010-12-23
*
Change of nomenclature: rawconstr -> glob_constr
glondu
2010-12-23
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
New script dev/tools/change-header to automatically update Coq files headers.
herbelin
2010-06-22
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Move from ocamlweb to ocamdoc to generate mli documentation
pboutill
2010-04-29
*
A bit of cleaning around name generation + creation of dedicated file namegen.ml
herbelin
2009-11-09
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
[next]