index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
/
unification.mli
Commit message (
Expand
)
Author
Age
*
Bump year in headers.
Pierre-Marie Pédrot
2017-07-04
*
Remove the Sigma (monotonous state) API.
Maxime Dénès
2017-06-06
*
unification.mli: Fix a spelling typo in a comment
Jason Gross
2017-05-23
*
Merge branch 'master' into econstr
Pierre-Marie Pédrot
2017-04-07
|
\
|
*
Ensuring static invariants about handling of pending evars in Pretyping.
Pierre-Marie Pédrot
2017-03-23
*
|
Definining EConstr-based contexts.
Pierre-Marie Pédrot
2017-02-14
*
|
Unification API using EConstr.
Pierre-Marie Pédrot
2017-02-14
|
/
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-21
|
\
|
*
Update copyright headers.
Maxime Dénès
2016-01-20
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-13
|
\
|
|
*
Fix essential bug in new Keyed Unification mode reported by R. Krebbers.
Matthieu Sozeau
2016-01-12
*
|
CLEANUP: kernel/context.ml{,i}
Matej Kosik
2016-01-11
*
|
More monotonicity in Tactics.
Pierre-Marie Pédrot
2015-10-19
|
/
*
Update headers.
Maxime Dénès
2015-01-12
*
Follow up to experimental eager evar unification in bcba6d1bc9:
Hugo Herbelin
2014-11-08
*
Enlarge the cases where the like first selection is used in destruct.
Hugo Herbelin
2014-10-31
*
Fixing destruct/induction with a using clause on a non-inductive type,
Hugo Herbelin
2014-10-26
*
This commit introduces changes in induction and destruct.
Hugo Herbelin
2014-10-25
*
A step towards better differentiating when w_unify is used for subterm
Hugo Herbelin
2014-09-10
*
Made the subterm finding function make_abstraction independent of the
Hugo Herbelin
2014-06-28
*
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-05-06
*
Removing dead code, thanks to new OCaml warnings and a bit of scripting.
Pierre-Marie Pédrot
2014-04-23
*
At least made the evar type opaque! There are still 5 remaining unsafe
ppedrot
2013-09-18
*
export Unification.abstract_list_all_with_dependencies
pboutill
2013-05-30
*
Fixed a little inefficiency of "set/destruct" over a pattern. Now
herbelin
2012-12-18
*
Improving error message when abtraction over goal (abstract_list_all
herbelin
2012-10-04
*
Updating headers.
herbelin
2012-08-08
*
Added a flag to control the use of typing when instantiating applied
herbelin
2011-12-17
*
Moved to a more standard order of arguments (i.e. env followed by evar_map)
herbelin
2011-10-11
*
Fix unification: detect invalid evar instantiations due to scoping earlier.
msozeau
2011-08-04
*
Generalizing flag use_evars_pattern_unification into a flag
herbelin
2011-06-18
*
Added a flag to restrict conversion in tactic unification on the
herbelin
2011-06-13
*
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
*
Add a flag to control betaiota reduction during unification to maintain backw...
msozeau
2011-04-18
*
- Add modulo_delta_types flag for unification to allow full
msozeau
2011-03-13
*
Added eta-expansion in kernel, type inference and tactic unification,
herbelin
2010-09-20
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
New script dev/tools/change-header to automatically update Coq files headers.
herbelin
2010-06-22
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Move from ocamlweb to ocamdoc to generate mli documentation
pboutill
2010-04-29
*
Promote evar_defs to evar_map (in Evd)
glondu
2009-11-11
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
Reactivation of pattern unification of evars in apply unification, in
herbelin
2009-07-08
*
Add new variants of [rewrite] and [autorewrite] which differ in the
msozeau
2009-06-30
*
Minor unification changes:
msozeau
2009-05-18
*
- Backtrack sur option with_types suite à confusion sur l'utilisation
herbelin
2008-04-27
*
- Backtrack sur extension de syntaxe pour pose qui rentre en conflit avec
herbelin
2008-04-26
*
Prise en compte des coercions dans les clauses "with" même si le type
herbelin
2008-04-23
*
- Parameterize unification by two sets of transparent_state, one for open
msozeau
2008-04-21
[next]