index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
/
reductionops.ml
Commit message (
Expand
)
Author
Age
*
Fix 'don't expose cases' in cbn
Pierre Boutillier
2015-02-15
*
Univs: proper printing of global and local universe names (only
Matthieu Sozeau
2015-01-17
*
Update headers.
Maxime Dénès
2015-01-12
*
Option -type-in-type continued (deactivate test for inferred sort of
Hugo Herbelin
2014-11-19
*
Evar normalization is now done eagerly.
Pierre-Marie Pédrot
2014-11-10
*
Implement a different strategy to expand primitive projections only when
Matthieu Sozeau
2014-10-15
*
Tentative fix for a badly used Option.get in Reductionops.
Pierre-Marie Pédrot
2014-10-12
*
Work around issues with FO unification trying to unify terms of
Matthieu Sozeau
2014-10-02
*
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
*
Simplify evarconv thanks to new delta status of projections,
Matthieu Sozeau
2014-09-30
*
In evarconv and unification, expand folded primitive projections to
Matthieu Sozeau
2014-09-29
*
Fix bug #3664 by refolding projections that don't reduce in cbn.
Matthieu Sozeau
2014-09-27
*
Add a boolean to indicate the unfolding state of a primitive projection,
Matthieu Sozeau
2014-09-27
*
Reductionops: (Co)Fixpoints are always refolded during iota
Pierre Boutillier
2014-09-18
*
Providing a -type-in-type option for collapsing the universe hierarchy.
Hugo Herbelin
2014-09-13
*
Cleanup code for looking up projection bodies.
Matthieu Sozeau
2014-09-06
*
Debug RAKAM
Pierre Boutillier
2014-08-26
*
Grammar: "avoiding to" isn't proper, either
Jason Gross
2014-08-25
*
Fix bug introduced by earlier commit on first-order unification of primitive
Matthieu Sozeau
2014-08-10
*
- Fix handling of opaque polymorphic definitions which were turned transparent.
Matthieu Sozeau
2014-08-03
*
Move to a representation of universe polymorphic constants using indices for ...
Matthieu Sozeau
2014-08-03
*
Rework code for refolding projections in whd_state/whd_simpl to allow Arguments
Matthieu Sozeau
2014-07-29
*
Reduce non-toplevel letins in splay_prod_assum (bug found in Ergo).
Matthieu Sozeau
2014-07-10
*
Removing dead code.
Pierre-Marie Pédrot
2014-06-17
*
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
*
Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un...
Matthieu Sozeau
2014-06-10
*
Make kernel reduction code parametric over the handling of universes,
Matthieu Sozeau
2014-06-06
*
Collecting in Namegen those conventional default names that are used in diffe...
Hugo Herbelin
2014-06-04
*
- Keep all <= constraints during refinement, otherwise we might miss collapse...
Matthieu Sozeau
2014-06-04
*
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
*
- Fixes for canonical structure resolution (check that the initial term indee...
Matthieu Sozeau
2014-05-06
*
- Fix bug preventing apply from unfolding Fixpoints.
Matthieu Sozeau
2014-05-06
*
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-05-06
*
Remove some dead-code (thanks to ocaml warnings)
Pierre Letouzey
2014-03-05
*
Fix bug 3245: 'simpl nomatch' argument annotation makes cbn go into an infini...
Pierre Boutillier
2014-02-28
*
Dead code elimionation in reductionops
Pierre Boutillier
2014-02-28
*
Ensuring that the module Stack is opaque inside Reductionops.
Pierre-Marie Pédrot
2014-02-24
*
cbn understands Arguments
Pierre Boutillier
2014-02-24
*
Simpl_behaviour becomes Reductionops.ReductionBehaviour
Pierre Boutillier
2014-02-24
*
No more translation array <-> list in Reductionops.Stack
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
[next]