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_term_to_relation.ml
Commit message (
Expand
)
Author
Age
*
Fix a bug preventing the generation of graphs when doing multiple
Matthieu Sozeau
2015-11-18
*
Univs: fix after rebase (from_ctx/from_env)
Matthieu Sozeau
2015-10-02
*
Univs: fix evar_map leaks bugs in Function
Matthieu Sozeau
2015-10-02
*
Univs: Add universe binding lists to definitions
Matthieu Sozeau
2015-09-14
*
Safer typing primitives.
Pierre-Marie Pédrot
2015-05-13
*
Function now supports puniveres
jforest
2015-04-14
*
Fix some typos in comments.
Guillaume Melquiond
2015-02-23
*
handling Functional Scheme for required but not imported modules
Julien Forest
2014-12-11
*
Closing bug 3837
Julien Forest
2014-12-08
*
Revert specific syntax for primitive projections, avoiding ugly
Matthieu Sozeau
2014-09-17
*
Uniformisation of the order of arguments env and sigma.
Hugo Herbelin
2014-09-12
*
Referring to evars by names. Added a parser for evars (but parsing of
Hugo Herbelin
2014-09-12
*
Parsing of Type@{max(i,j)}.
Matthieu Sozeau
2014-09-08
*
Remove [Infer] option of records.
Arnaud Spiwack
2014-09-04
*
Print [Variant] types with the keyword [Variant].
Arnaud Spiwack
2014-09-04
*
A tentative uniform naming policy in module Inductiveops.
Hugo Herbelin
2014-08-01
*
Adapt Y. Bertot's path on private inductives (now the keyword is "Private").
Yves Bertot
2014-05-06
*
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-05-06
*
More monomorphic List.mem + List.assoc + ...
letouzey
2013-10-24
*
cList: set-as-list functions are now with an explicit comparison
letouzey
2013-10-23
*
Removing a bunch of generic equalities.
ppedrot
2013-09-27
*
A uniformization step around understand_* and interp_* functions.
herbelin
2013-05-09
*
Merging Context and Sign.
ppedrot
2013-04-29
*
Splitting Term into five unrelated interfaces:
ppedrot
2013-04-29
*
Restrict (try...with...) to avoid catching critical exn (part 9)
letouzey
2013-03-13
*
Uniformization of the "anomaly" command.
ppedrot
2013-01-28
*
Modulification of name
ppedrot
2012-12-18
*
Modulification of identifier
ppedrot
2012-12-14
*
correcting a little bug in Function
jforest
2012-10-31
*
Remove some more "open" and dead code thanks to OCaml4 warnings
letouzey
2012-10-02
*
Some documentation and cleaning of CList and Util interfaces.
ppedrot
2012-09-15
*
As r15801: putting everything from Util.array_* to CArray.*.
ppedrot
2012-09-14
*
Moving Utils.list_* to a proper CList module, which includes stdlib
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
*
Getting rid of Pp.msgnl and Pp.message.
ppedrot
2012-06-01
*
Getting rid of Pp.msg
ppedrot
2012-05-30
*
global_reference migrated from Libnames to new Globnames, less deps in gramma...
letouzey
2012-05-29
*
Basic stuff about constr_expr migrated from topconstr to constrexpr_ops
letouzey
2012-05-29
*
Stuff about notation_constr (ex-aconstr) now in notation_ops.ml
letouzey
2012-05-29
*
New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr
letouzey
2012-05-29
*
Glob_term now mli-only, operations now in Glob_ops
letouzey
2012-05-29
*
locus.mli for occurrences+clauses, misctypes.mli for various little things
letouzey
2012-05-29
*
"A -> B" is a notation for "forall _ : A, B".
pboutill
2012-04-12
*
Second step of integration of Program:
msozeau
2012-03-14
*
Noise for nothing
pboutill
2012-03-02
*
Remove dynamic stuff from constr_expr and glob_constr
glondu
2011-10-28
*
correction du bug 2047
jforest
2011-09-09
*
A new mechanism to handle errors.
aspiwack
2011-05-13
*
Rename mkR* smart constructors (mostly in funind)
glondu
2010-12-25
[next]