index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
plugins
/
funind
/
indfun_common.ml
Age
Commit message (
Expand
)
Author
2019-10-25
[funind] Removed dead code.
Emilio Jesus Gallego Arias
2019-08-29
[funind] Don't export duplicate save function.
Emilio Jesus Gallego Arias
2019-08-29
Merge PR #10674: [declare] Move proof_entry type to declare, put interactive ...
Pierre-Marie Pédrot
2019-08-27
[declare] Move proof_entry type to declare, put interactive proof data on top...
Emilio Jesus Gallego Arias
2019-08-27
[cleanup] Replace uses of UserError constructor, clarify exception names.
Emilio Jesus Gallego Arias
2019-08-07
[funind] Move some exception-based control flow to explicit option typing.
Emilio Jesus Gallego Arias
2019-08-07
[funind] Port indfun to the new tactic engine.
Emilio Jesus Gallego Arias
2019-07-31
[funind] Move duplicated `observe_tac` function to indfun_common.
Emilio Jesus Gallego Arias
2019-07-31
[funind] Move common `make_eq` to funind_common.
Emilio Jesus Gallego Arias
2019-07-31
[funind] Move principle generation to its own file.
Emilio Jesus Gallego Arias
2019-07-08
[api] Deprecate GlobRef constructors.
Emilio Jesus Gallego Arias
2019-07-03
declare_variable: path is always Lib.cwd()
Gaëtan Gilbert
2019-07-03
Declare section variables in direct style "without" an object
Gaëtan Gilbert
2019-07-01
[decls] Remove goal_object_kind type.
Emilio Jesus Gallego Arias
2019-07-01
[declare] Separate kinds from entries in constant declaration
Emilio Jesus Gallego Arias
2019-07-01
[api] Refactor most of `Decl_kinds`
Emilio Jesus Gallego Arias
2019-06-26
[declare] Fine tuning of Hook type.
Emilio Jesus Gallego Arias
2019-06-24
[api] Move `locality` from `library` to `vernac`.
Emilio Jesus Gallego Arias
2019-06-24
[lemmas] [proof] Split proof kinds into per-layer components.
Emilio Jesus Gallego Arias
2019-06-24
[proof] Remove duplicated universe polymorphic from decl_kinds
Emilio Jesus Gallego Arias
2019-06-24
Duplicate the type of constant entries in Proof_global.
Pierre-Marie Pédrot
2019-06-17
[proof] Move declaration hooks to DeclareDef.
Emilio Jesus Gallego Arias
2019-06-12
[funind] Untabify; necessary to ease the review of subsequent work.
Emilio Jesus Gallego Arias
2019-06-08
Cleaning the status of Local Definition and similar.
Hugo Herbelin
2019-05-23
Fixing typos - Part 2
JPR
2019-03-27
[plugins] [funind] Adapt to removal of imperative proof state.
Emilio Jesus Gallego Arias
2019-03-20
Stop accessing proof env via Pfedit in printers
Maxime Dénès
2019-03-14
Add a non-cumulative impredicative universe SProp.
Gaëtan Gilbert
2019-02-23
[vernac] Unify declaration hooks.
Emilio Jesus Gallego Arias
2018-12-13
Move shallow state logic to the function preparing state for workers
Maxime Dénès
2018-12-12
Higher-level libobject API for objects with fixed scopes
Maxime Dénès
2018-11-30
[vernac] [hooks] Refactor towards optional hooks.
Emilio Jesus Gallego Arias
2018-11-23
s/let _ =/let () =/ in some places (mostly goptions related)
Gaëtan Gilbert
2018-11-17
[pfedit] Remove cook_proof stub.
Emilio Jesus Gallego Arias
2018-11-07
[Funind plugin] Remove some dead code
Vincent Laporte
2018-10-19
Deprecating Global.type_of_global_in_context.
Hugo Herbelin
2018-10-18
[universes] deprecate constr_of_global
Matthieu Sozeau
2018-10-10
[coqlib] Rebindable Coqlib namespace.
Emilio Jesus Gallego Arias
2018-10-05
[kernel] Remove section paths from `KerName.t`
Maxime Dénès
2018-06-18
Remove reference name type.
Maxime Dénès
2018-05-30
[api] Remove deprecated object from `Term`
Emilio Jesus Gallego Arias
2018-05-23
Moving Option.smart_map to Option.Smart.map.
Hugo Herbelin
2018-05-17
Split off Universes functions dealing with generating new universes.
Gaëtan Gilbert
2018-03-09
[located] Push inner locations in `reference` to a CAst.t node.
Emilio Jesus Gallego Arias
2018-01-30
Delete duplicate line
Paul Steckler
2017-12-12
In printing, factorizing "match" clauses with same right-hand side.
Hugo Herbelin
2017-11-21
[printing] Deprecate all printing functions accessing the global proof.
Emilio Jesus Gallego Arias
2017-11-19
[plugins] Prepare plugin API for functional handling of state.
Emilio Jesus Gallego Arias
2017-11-06
[api] Move structures deprecated in the API to the core.
Emilio Jesus Gallego Arias
2017-10-17
[stm] Remove state-handling from Futures.
Emilio Jesus Gallego Arias
[next]
