index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
...
|
|
|
|
|
|
|
*
fix syntax of .mlg
Vincent Laporte
2018-07-03
|
|
|
|
|
|
|
*
Describe attributes in the documentation.
Vincent Laporte
2018-07-03
|
|
|
|
|
|
|
*
[vernac] use a record for the contents of the “deprecated” attribute
Vincent Laporte
2018-07-03
|
|
|
|
|
|
|
*
[vernac] use plain strings as attribute names
Vincent Laporte
2018-07-03
|
|
|
|
|
|
|
*
[vernac] indentation
Vincent Laporte
2018-07-03
|
|
|
|
|
|
|
*
[vernac] Generic syntax for flags/attributes
Vincent Laporte
2018-07-03
|
|
|
|
|
|
|
*
[vernac] Generic parsing rules for attributes
Vincent Laporte
2018-07-03
|
|
|
|
|
|
|
*
[vernac] Add a “deprecated” attribute
Vincent Laporte
2018-07-03
|
|
|
|
|
|
|
*
Allow “Let”-defined coercions
Vincent Laporte
2018-07-03
|
|
|
|
|
|
|
*
[vernac] Concrete syntax for attributes
Vincent Laporte
2018-07-03
|
|
|
|
|
|
|
*
[vernac] mk_atts: an atts record with default values
Vincent Laporte
2018-07-03
|
|
|
|
|
|
|
*
[vernac] attribute_of_flags
Vincent Laporte
2018-07-03
|
|
_
|
_
|
_
|
_
|
_
|
/
|
/
|
|
|
|
|
|
|
*
|
|
|
|
|
Add a test build of Nix package to GitLab CI.
Théo Zimmermann
2018-07-03
|
*
|
|
|
|
|
Adapt default.nix to allow nix-build to run the test-suite.
Théo Zimmermann
2018-07-03
|
/
/
/
/
/
/
*
|
|
|
|
|
Merge PR #7978: [ci] [docker] Make sure we don't install optional packages wi...
Gaëtan Gilbert
2018-07-03
|
\
\
\
\
\
\
|
|
|
*
|
|
|
Add overlay for equations.
Gaëtan Gilbert
2018-07-03
|
|
|
*
|
|
|
Library: use ocaml typing to show that we find at most 2 files
Gaëtan Gilbert
2018-07-03
|
|
|
*
|
|
|
Library.register_loaded_library: remove unused variable
Gaëtan Gilbert
2018-07-03
|
|
|
*
|
|
|
Glob_ops.rename_glob_vars: fix typo
Gaëtan Gilbert
2018-07-03
|
|
|
*
|
|
|
Glob_ops.fix_kind_eq: fix typo
Gaëtan Gilbert
2018-07-03
|
|
|
*
|
|
|
Pputils: fix typo
Gaëtan Gilbert
2018-07-03
|
|
|
*
|
|
|
Evarutil.(e_)new_Type: remove unused env argument
Gaëtan Gilbert
2018-07-03
|
|
|
*
|
|
|
Remove unused function Evd.whd_sort_variable
Gaëtan Gilbert
2018-07-03
|
|
|
*
|
|
|
Remove unused output of Universes.normalize_univ_variables
Gaëtan Gilbert
2018-07-03
|
|
|
*
|
|
|
Remove unused env argument to fresh_sort_in_family
Gaëtan Gilbert
2018-07-03
|
|
|
*
|
|
|
Coq_omega: remove unused Goal.enters
Gaëtan Gilbert
2018-07-03
|
|
|
*
|
|
|
Remove unused function Coq_omega.timing.
Gaëtan Gilbert
2018-07-03
|
|
|
*
|
|
|
Taccoerce: remove various unused arguments.
Gaëtan Gilbert
2018-07-03
|
|
|
*
|
|
|
Remove unused arguments to Ide_slave.concl_next_tac.
Gaëtan Gilbert
2018-07-03
|
|
|
*
|
|
|
Pptactic: remove unused arguments
Gaëtan Gilbert
2018-07-03
|
|
|
*
|
|
|
checker Indtypes: remove unused arguments
Gaëtan Gilbert
2018-07-03
|
|
|
*
|
|
|
Term_typing: remove unused argument to internal function.
Gaëtan Gilbert
2018-07-03
|
|
|
*
|
|
|
Cooking.cook_constant: remove unused env argument.
Gaëtan Gilbert
2018-07-03
|
|
|
*
|
|
|
Indtypes: remove unused is_unit.
Gaëtan Gilbert
2018-07-03
*
|
|
|
|
|
|
Merge PR #7607: Simplify reification of predicate in bytecode and native comp...
Pierre-Marie Pédrot
2018-07-03
|
\
\
\
\
\
\
\
|
|
|
|
*
|
|
|
checker Modops strengthening: remove unused argument resolver
Gaëtan Gilbert
2018-07-03
|
|
|
|
*
|
|
|
Subtyping.check_constant: remove unused module path argument.
Gaëtan Gilbert
2018-07-03
|
|
|
|
*
|
|
|
Inductive.extract_stack,filter_stack_domain: remove unused arguments
Gaëtan Gilbert
2018-07-03
|
|
|
|
*
|
|
|
Nativecode compile_mind, compile_mind_field: remove unused arguments
Gaëtan Gilbert
2018-07-03
|
|
|
|
*
|
|
|
Nativecode.pp_mllam internal pp_letrec: remove unused argument.
Gaëtan Gilbert
2018-07-03
|
|
|
|
*
|
|
|
Util.Empty: implement using polymorphic record.
Gaëtan Gilbert
2018-07-03
|
|
|
|
*
|
|
|
coqdoc Index.find_string: remove unused argument.
Gaëtan Gilbert
2018-07-03
|
|
|
|
*
|
|
|
Coq_makefile.generate_conf_coq_config: remove unused argument.
Gaëtan Gilbert
2018-07-03
|
|
|
|
*
|
|
|
Libobject.apply_dyn_fun: remove unused deflt argument
Gaëtan Gilbert
2018-07-03
|
|
|
|
*
|
|
|
CWarnings.normalize_flags: removed unused ~silent argument.
Gaëtan Gilbert
2018-07-03
|
|
|
|
*
|
|
|
Modops.add_retroknowledge: remove unused argument.
Gaëtan Gilbert
2018-07-03
|
|
_
|
_
|
/
/
/
/
|
/
|
|
|
|
|
|
*
|
|
|
|
|
|
Merge PR #7820: [hints] Add Hint Variables/Constants Opaque/Transparent commands
Pierre-Marie Pédrot
2018-07-03
|
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
Merge PR #7942: Extend readme with 'beginners guide'
Théo Zimmermann
2018-07-03
|
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
Merge PR #7974: Fix default.nix following a package renaming.
Vincent Laporte
2018-07-03
|
\
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
\
Merge PR #7977: allow `make check` to succeed when -prefix is given to ./conf...
Emilio Jesus Gallego Arias
2018-07-03
|
\
\
\
\
\
\
\
\
\
\
[prev]
[next]
Vincent Laporte
Théo Zimmermann
Gaëtan Gilbert
Gaëtan Gilbert
Pierre-Marie Pédrot
Emilio Jesus Gallego Arias