index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
/
evarconv.ml
Commit message (
Expand
)
Author
Age
...
*
Uniformization of the "anomaly" command.
ppedrot
2013-01-28
*
- Fix evarconv so that we have complete eta-conversion:
msozeau
2013-01-22
*
Evarconv: Check stack before term in Canonical Structure approuval
pboutill
2013-01-18
*
Reductionops reduction machine can refold constant
pboutill
2012-12-19
*
Evarconv.Pseudorigid erasure
pboutill
2012-12-19
*
Modulification of identifier
ppedrot
2012-12-14
*
Moved Intset and Intmap to Int namespace.
ppedrot
2012-12-14
*
Evarconv: Fix #2936 + comments
pboutill
2012-11-28
*
Monomorphization (pretyping)
ppedrot
2012-11-22
*
Cleaning and small optimization in CList.
ppedrot
2012-11-20
*
Remove some more "open" and dead code thanks to OCaml4 warnings
letouzey
2012-10-02
*
As r15801: putting everything from Util.array_* to CArray.*.
ppedrot
2012-09-14
*
Moving Utils.list_* to a proper CList module, which includes stdlib
ppedrot
2012-09-14
*
This patch removes unused "open" (automatically generated from
regisgia
2012-09-14
*
Unification in Evar_conv uses an abstract machine state
pboutill
2012-08-09
*
Updating headers.
herbelin
2012-08-08
*
Reductionops refactoring
pboutill
2012-07-20
*
flex_maybeflex factoring
pboutill
2012-07-12
*
miller_pfenning unification code factoring
pboutill
2012-07-12
*
flex_kind_of_term does not have a copy of term
pboutill
2012-07-12
*
evar reduction is already made by whd_*
pboutill
2012-07-12
*
Added an indirection with respect to Loc in Compat. As many [open Compat]
ppedrot
2012-06-22
*
Fix bug #2791 by doing a fixpoint computation in consider_remaining_problems:
msozeau
2012-06-21
*
Fixing use of an error instead of a boolean result in the unification
herbelin
2012-06-20
*
Reductionops : Better abstract machine stack utilities
pboutill
2012-06-15
*
global_reference migrated from Libnames to new Globnames, less deps in gramma...
letouzey
2012-05-29
*
locus.mli for occurrences+clauses, misctypes.mli for various little things
letouzey
2012-05-29
*
Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evd
letouzey
2012-05-29
*
Unification: Added a heuristic to solve problems of the form
herbelin
2012-03-26
*
evarconv: MaybeFlex/MaybeFlex case infers more Canonical Structures
gareuselesinge
2012-03-22
*
Generalized the use of evar candidates in type inference unification:
herbelin
2012-03-20
*
Reorganizing the structure of evarutil.ml (only restructuration, no
herbelin
2012-03-20
*
Noise for nothing
pboutill
2012-03-02
*
Introducing a notion of evar candidates to be used when an evar is
herbelin
2011-12-16
*
Discarding let-ins from the instances of the evars in the
herbelin
2011-12-04
*
Refined second_order_matching so that a constraint on which
herbelin
2011-11-08
*
optimization: memoization for is_open_canonical_projection
gareuselesinge
2011-11-08
*
Improved check is_open_canonical_projection
gareuselesinge
2011-11-08
*
Fixing incorrect change to pattern-unification over Meta's introduced
herbelin
2011-11-06
*
Deactivating second-order pattern-matching in evarconv for 8.4.
herbelin
2011-10-26
*
Fixing instance/filter mismatch in materialize_evar + documentation.
herbelin
2011-10-24
*
Fail if some conv pbs remain after consider_remaining_unif_problems.
herbelin
2011-10-22
*
Use also second-order unification if first-order fails at the time of conside...
herbelin
2011-10-22
*
Completing r14538 (Chung-Kil Hur's trick for fast dependently-typed
herbelin
2011-10-11
*
More robust and uniform treatment of aliases in evarutil.ml
herbelin
2011-10-10
*
Applied the trick of Chung-Kil Hur to solve second-order matching
herbelin
2011-10-10
*
Evarconv: generic equality on constr replaced by eq_constr
puech
2011-07-29
*
Ensured that the transparency state is used when flag betaiota is on for apply.
herbelin
2011-06-19
*
Applying Enrico Tassi's patch for giving priority to delta over eta in
herbelin
2011-05-24
*
As remarked by Enrico, we'd better use eq_constr than structural equality
herbelin
2011-03-31
[prev]
[next]