master Used by everyone - Default branch
develop Used by everyone - The state of the art of Dedukti, will be supressed soon (once merged in master)
sizechange Created by Guillaume Genestier - An implementation of a termination checker for Dedukti
acu Created by Gaspard Ferey - Dedukti with AC/ACU (WIP)
sukerujo Created by Raphaël Cauderlier - An alternative parser with syntactic sugar and built-ins. In the long run, should be a soft on its own, independent of Dedukti. See http://deducteam.gforge.inria.fr/sukerujo/
eniqoc Created by François Thiré - Translate proofs from Dedukti[STTforall] to Coq and Matita. Should be a soft on its own, independent of Dedukti.
universo Created by François Thiré - Translate proofs form Dedukti[STTforall] to OpenTheory. Should be a soft on its own (probably merged with eniqoc), independent of Dedukti.
meta Probably created by François Thiré - Meta Dedukti - Add a tool called dkmeta to normalize files. In the long run, should be a soft on its own, independent of Dedukti. See http://deducteam.gforge.inria.fr/metadedukti/
skmeta Created by Raphaël Cauderlier - Meta Sukerujo - Meta Dedukti meets Sukerujo
brackets Created by Gaspard Ferey - Work on issue #22 (Brackets checking) - PR #5
fix-rule-cstr Created by Gaspard Ferey - Work on issue #17 (Rule constraints) - PR #19
fix-rule-cstr2 Created by Gaspard Ferey - Alternative work on issue #17 (Rule constraints) - PR #21
fix-step-reduction Created by Gaspard Ferey - Toward parametric reduction commands. - PR #14
v2.5 merged, Who created this ? Where does it branch from ?
v2.4 merged
v2.3beta merged
v1.2 merged
contextual-typing Created by François Thiré -- An experiment.
metavar Created by François Thiré -- An experiment that adds meta variables in Dedukti.
extract-types Created by Rodolphe Lepigre, merged -- Attempts to extract type information for generating PVS proofs.
develop-oasis Created by François Thiré -- can be suppressed.
ediloh-dev Created by François Thiré - Translate proofs form Dedukti[STTforall] to OpenTheory. Should be a soft on its own (probably merged with eniqoc), independent of Dedukti.
ediloh2 Created by François Thiré -- will be suppressed soon.
trace Created by François Thiré -- can be suppressed.
ediloh Created by François Thiré -- will be suppressed soon.
comments Created by François Thiré -- can be suppressed.
dkprint Created by François Thiré -- can be suppressed.
sukerujo-dev Created by François Thiré -- can be suppressed.
deduktipli Created by François Thiré -- Change the parser fonctor so that mk_declaration ; mk_definition etc... use monads. Should be a soft on its own. But is it useful?
lambdafree Created by Raphaël Cauderlier -- An unfinished variant of Meta Dedukti that removes the lambda abstractions. Should be a soft on its own, maybe an option of Meta Dedukti.
Dedukti_AC
ac_dedukti
printers
da_lib_in_da_place Created by Simon Cruanes, an OCaml library exporting Dedukti features
develop-let
no-de-bruijn-format
no-de-bruijn-let
no-de-bruijn Created by Simon Cruanes, uses named variables instead of De Bruijn indexes
let-binder Created by Simon Cruanes, let bindings in the kernel
develop-simon Created by Simon Cruanes, merged.
mmt Created by Ronan Saillard, a translator from Dedukti to MMT
dkconf
dev Created by Ronan Saillard, old name of the develop branch
confluence
CriticalPairs
Profiling
luaBindings