index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
/
reductionops.mli
Commit message (
Expand
)
Author
Age
*
Inv API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Clenv API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Unification API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Pretyping API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Reductionops API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Termops API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
no-refold patch
Paul Steckler
2016-09-09
*
closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)
Pierre Letouzey
2016-07-03
*
Make semantics of whd_zeta consistent with other whd_* functions.
Maxime Dénès
2016-07-01
*
Separate flags for fix/cofix/match reduction and clean reduction function names.
Maxime Dénès
2016-07-01
*
Using monotonic types for conversion functions.
Pierre-Marie Pédrot
2016-02-15
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-21
|
\
|
*
Update copyright headers.
Maxime Dénès
2016-01-20
*
|
merge
Matej Kosik
2016-01-11
|
\
\
|
*
|
CLEANUP: kernel/context.ml{,i}
Matej Kosik
2016-01-11
*
|
|
Remove duplicate declarations.
Guillaume Melquiond
2016-01-02
|
/
/
*
/
CLEANUP: in the Reductionops module
Matej Kosik
2015-12-17
|
/
*
Avoid dependency of the pretyper on C code.
Maxime Dénès
2015-10-15
*
Fix #4346 2/2: VM casts were not inferring universe constraints.
Maxime Dénès
2015-10-15
*
Fix #4346 1/2: native casts were not inferring universe constraints.
Maxime Dénès
2015-10-15
*
Reverting 16 last commits, committed mistakenly using the wrong push command.
Hugo Herbelin
2015-08-02
*
Documenting in passing.
Hugo Herbelin
2015-08-02
*
Fix bug #3532, providing universe inconsistency information when a
Matthieu Sozeau
2015-03-04
*
Add support so that the type of a match in an inductive type with let-in
Hugo Herbelin
2015-02-27
*
Update headers.
Maxime Dénès
2015-01-12
*
fix make mlidoc
Pierre Boutillier
2014-10-08
*
Fix treatment of projections in Cst_stacks and unfolding behavior in evarconv.
Matthieu Sozeau
2014-10-02
*
Fix cbn behavior wrt simpl no match
Pierre Boutillier
2014-10-01
*
Fix the refolding by cbn of mutal constants defined in not included modules
Pierre Boutillier
2014-10-01
*
In evarconv and unification, expand folded primitive projections to
Matthieu Sozeau
2014-09-29
*
Add a boolean to indicate the unfolding state of a primitive projection,
Matthieu Sozeau
2014-09-27
*
Providing a -type-in-type option for collapsing the universe hierarchy.
Hugo Herbelin
2014-09-13
*
Adapt simpl/cbn unfolding and refolding machinery to projections, so that
Matthieu Sozeau
2014-06-13
*
- Fix bug #3368, due to wrong use of the Cst_stack for projections.
Matthieu Sozeau
2014-06-11
*
cbn understand ! Arguments directive
Pierre Boutillier
2014-06-04
*
Cbn reduces Pos.compare p~1 q~1 to Pos.compare p q
Pierre Boutillier
2014-05-26
*
Reduction.Stack.Fix/Case stores Cst_stack.t
Pierre Boutillier
2014-05-26
*
Cst_stack before stack (abstraction leak in whd_gen)
Pierre Boutillier
2014-05-26
*
cbn: args list instead of arg number
Pierre Boutillier
2014-05-26
*
Reductionops.Stack.map & Reduction.iterate_whd_gen
Pierre
2014-05-26
*
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-05-06
*
Remove many superfluous 'open' indicated by ocamlc -w +33
Pierre Letouzey
2014-03-05
*
Dead code elimionation in reductionops
Pierre Boutillier
2014-02-28
*
Simpl_behaviour becomes Reductionops.ReductionBehaviour
Pierre Boutillier
2014-02-24
*
Reductionops.Stack.strip* are ready to deal with Shift
Pierre Boutillier
2014-02-24
*
Reductionops.Stack.app_node is secret
Pierre Boutillier
2014-02-24
*
app_node, stack, state printers
Pierre Boutillier
2014-02-24
*
Stack operations of Reductionops in Reductionops.Stack
Pierre Boutillier
2014-02-24
*
Conv_orable made functional and part of pre_env
gareuselesinge
2013-10-31
*
Do not generate useless argument arrays in whd_* functions.
ppedrot
2013-10-29
[next]