index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
Commit message (
Expand
)
Author
Age
*
Added support for referring to subterms of the goal by pattern.
herbelin
2011-09-26
*
Generalizing subst_term_occ so that it supports an arbitrary matching
herbelin
2011-09-26
*
Adding subst_term up to conv
herbelin
2011-09-26
*
Moving implicit tactic support from Tacinterp to Pfedit and final evar
herbelin
2011-09-26
*
Propagated information from the reduction tactics to the kernel so
herbelin
2011-08-10
*
Two bugs in pattern-matching compilation:
herbelin
2011-08-08
*
Esubst: make types of substitutions & lifts private
puech
2011-08-08
*
Fix unification: detect invalid evar instantiations due to scoping earlier.
msozeau
2011-08-04
*
Fix nf_evars_undefined
msozeau
2011-08-03
*
Patch to simplify is_open_canonical_projection
herbelin
2011-08-02
*
More robust evar_map debugging printer
herbelin
2011-08-02
*
Evarutil: replace generic list_distinct on constr by constr_list_distinct
puech
2011-07-29
*
Evarutil: replaced some generic = on constr by destructors
puech
2011-07-29
*
Evarutil: generic equality on constr replaced by destructors
puech
2011-07-29
*
Evarconv: generic equality on constr replaced by eq_constr
puech
2011-07-29
*
Cases: generic equality on constr replaced by destructors
puech
2011-07-29
*
Classops: generic equality on constr replaced by eq_constr
puech
2011-07-29
*
Evarutil: generic equality on constr replaced by eq_constr (x2)
puech
2011-07-29
*
Evarutil: generic equality on constr replaced by eq_constr
puech
2011-07-29
*
Tacred: generic equality on constr replaced by eq_constr
puech
2011-07-29
*
This is exactly the structure needed to handle controlling printing
herbelin
2011-07-16
*
Extraction: forbid Prop-polymorphism of inductives when extracting to Ocaml
letouzey
2011-07-04
*
Cleaning debugging printer relative to new proof engine. In
herbelin
2011-06-21
*
Fixing two typos introduced in r14217 and r14223
herbelin
2011-06-20
*
Ensured that the transparency state is used when flag betaiota is on for apply.
herbelin
2011-06-19
*
Generalizing flag use_evars_pattern_unification into a flag
herbelin
2011-06-18
*
Activating flags betaiota by default for apply
herbelin
2011-06-18
*
The ad hoc version for first-order unification at toplevel of "?n args
herbelin
2011-06-18
*
Added full pattern-unification on Meta for tactic unification.
herbelin
2011-06-13
*
Added a flag to restrict conversion in tactic unification on the
herbelin
2011-06-13
*
Oups, typo in previous commit
herbelin
2011-06-12
*
Removed what looks like a (very old) useless f.o. unification pass
herbelin
2011-06-12
*
Added a new flag for freezing evars in tactic unification. Used this
herbelin
2011-06-12
*
Moved allow_K to a unification flag
herbelin
2011-06-10
*
Fixes in pruning, do not fail if pruning is impossible due to typing constrai...
msozeau
2011-06-10
*
More fixes in pruning/restriction of evars during unification.
msozeau
2011-06-09
*
Fixes in pruning in unification.
msozeau
2011-06-08
*
- Fix restrict_hyps to not allow filtering on a variable required to typechec...
msozeau
2011-06-07
*
Applying Enrico Tassi's patch for giving priority to delta over eta in
herbelin
2011-05-24
*
Failing instead of switching to the coercion mechanism when VMcast
herbelin
2011-05-15
*
A better procedure for checking presence of undefined evars.
aspiwack
2011-05-13
*
Fix merge, Cumul moved to CUMUL
msozeau
2011-05-05
*
Merge branch 'subclasses' into coq-trunk
msozeau
2011-05-05
*
First phase removing obsolete support for eta up to conversion in
herbelin
2011-05-04
*
Fixing bug in printing let-in binders in fix/cofix
herbelin
2011-04-24
*
Allow betaiota when checking unification of the types of metas (fixes ATBR co...
msozeau
2011-04-20
*
Add a flag to control betaiota reduction during unification to maintain backw...
msozeau
2011-04-18
*
Fix unification of types of metavariables and error message for sort unificat...
msozeau
2011-04-16
*
Take benefit of eta-expansion so that "ex P" is displayed "exists x, P x".
herbelin
2011-04-15
*
- Make typeclass transparency information directly available
msozeau
2011-04-13
[next]