index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
interp
/
implicit_quantifiers.mli
Commit message (
Expand
)
Author
Age
*
Swapping Context and Constr: defining declarations on constr in Constr.
Hugo Herbelin
2018-06-27
*
Remove reference name type.
Maxime Dénès
2018-06-18
*
[api] Misctypes removal: miscellaneous aliases.
Emilio Jesus Gallego Arias
2018-06-12
*
[api] Move `Constrexpr` to the `interp` module.
Emilio Jesus Gallego Arias
2018-05-31
*
[api] Move `Vernacexpr` to parsing.
Emilio Jesus Gallego Arias
2018-05-23
*
[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.
Emilio Jesus Gallego Arias
2018-05-04
*
Update headers following #6543.
Théo Zimmermann
2018-02-27
*
[ast] Improve precision of Ast location recognition in serialization.
Emilio Jesus Gallego Arias
2018-02-22
*
Remove unused boolean from cl_context field of Typeclasses.typeclass
Gaëtan Gilbert
2017-11-30
*
Bump year in headers.
Pierre-Marie Pédrot
2017-07-04
*
[location] Make location optional in Loc.located
Emilio Jesus Gallego Arias
2017-04-25
*
Renaming local_binder into local_binder_expr.
Hugo Herbelin
2017-03-24
*
CLEANUP: Context.{Rel,Named}.Declaration.t
Matej Kosik
2016-02-09
*
Update copyright headers.
Maxime Dénès
2016-01-20
*
Fix some typos.
Guillaume Melquiond
2015-10-13
*
Fixing bug #3811: "Universe annotations confused inside generalizing binders".
Pierre-Marie Pédrot
2015-07-29
*
Update headers.
Maxime Dénès
2015-01-12
*
Remove many superfluous 'open' indicated by ocamlc -w +33
Pierre Letouzey
2014-03-05
*
Merging Context and Sign.
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
*
global_reference migrated from Libnames to new Globnames, less deps in gramma...
letouzey
2012-05-29
*
New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr
letouzey
2012-05-29
*
Noise for nothing
pboutill
2012-03-02
*
More comments and less doublons in some mli
pboutill
2011-02-10
*
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
*
Fix bug #2262: bad implicit argument number by avoiding counting
msozeau
2010-06-09
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Move from ocamlweb to ocamdoc to generate mli documentation
pboutill
2010-04-29
*
Use generalizable variables info when internalizing arbitrary bindings,
msozeau
2009-11-08
*
Add a new vernacular command for controling implicit generalization of
msozeau
2009-10-27
*
Fix bug #2162 and a name clashing bug in generalized binders.
msozeau
2009-10-09
*
Rewrite of Program Fixpoint to overcome the previous limitations:
msozeau
2009-03-28
*
Open notation for declaring record instances.
msozeau
2008-10-23
*
Generalized implementation of generalization.
msozeau
2008-10-23
*
A much better implementation of implicit generalization:
msozeau
2008-10-22
*
Fixes in handling of implicit arguments:
msozeau
2008-07-04
*
Code cleanup in typeclasses, remove dead and duplicated code.
msozeau
2008-06-21
*
Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaient
herbelin
2008-04-01
*
Do another pass on the typeclasses code. Correct globalization of class
msozeau
2008-03-19
*
Move generally useful definition of nf_evar on contexts to evarutil.
msozeau
2008-02-08
*
Generalize instance declarations to any context, better name handling. Add ho...
msozeau
2008-01-15
*
Cleaner quantifiers for type classes, breaks clrewrite for the moment but imp...
msozeau
2008-01-07
*
Fix a naming bug reported by Arnaud Spiwack, allow instance search to create ...
msozeau
2008-01-05
[next]