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
*
Small code cleaning in Evarutil.
ppedrot
2013-10-08
*
Removing useless evar code.
ppedrot
2013-10-06
*
Removing uses of Evar.add in class-related functions.
ppedrot
2013-10-06
*
Removing dubious use of evarmap manipulating functions in printing
ppedrot
2013-10-05
*
Moving side effects into evar_map. There was no reason to keep another
ppedrot
2013-10-05
*
Removing a bunch of generic equalities.
ppedrot
2013-09-27
*
Removing useless evar-related stuff.
ppedrot
2013-09-25
*
Get rid of the uses of deprecated OCaml elements (still remaining compatible ...
xclerc
2013-09-19
*
At least made the evar type opaque! There are still 5 remaining unsafe
ppedrot
2013-09-18
*
Removing the last global evar generation in Term_dnet. The very
ppedrot
2013-09-18
*
Removing unused code from Term_dnet.
ppedrot
2013-09-18
*
Removing almost all new_untyped_evar, and a bunch of Evd.add.
ppedrot
2013-09-18
*
Taming the simpl evar hack that used to use negative evars.
ppedrot
2013-09-18
*
Unplugging Autoinstance. The code is still here if someone wishes
ppedrot
2013-09-12
*
Optimizing some evar_maps manipulation. In particular, using a [map] instead
ppedrot
2013-09-05
*
Documentation of Evd.
ppedrot
2013-09-05
*
Cleaning up of Evd. Extruding the tower of modules used to define evar_maps.
ppedrot
2013-09-05
*
Partly replacing list-based access functions in Evd. This is still
ppedrot
2013-09-03
*
Removing association lists in Reductionops. Btw, defining the dual of the
ppedrot
2013-08-25
*
Actually using the domain function for maps.
ppedrot
2013-08-25
*
Added a more efficient way to recover the domain of a map.
ppedrot
2013-08-25
*
Replacing lists by sets in clear tactic.
ppedrot
2013-08-25
*
Nicer code concerning dirpaths and modpath around Lib
letouzey
2013-08-22
*
Misc changes around coqtop.ml :
letouzey
2013-08-22
*
Universe counters on slaves are in sync with master
gareuselesinge
2013-08-20
*
State Transaction Machine
gareuselesinge
2013-08-08
*
Removing useless casts between arrays and lists.
ppedrot
2013-08-04
*
Removing now useless merging primitives from Evd.
ppedrot
2013-08-04
*
Small fixes due to the arrival of OCaml 3.12.
ppedrot
2013-08-03
*
Fixing #3088. Translation from globconstrs to patterns was forgetting
ppedrot
2013-08-01
*
Added printing of instance priority to the Print Instances command.
ppedrot
2013-08-01
*
- Fix uncaught exception NotASort from reductionops, moving decomp_sort to re...
msozeau
2013-07-19
*
Revising r16550 about providing intro patterns for applying injection:
herbelin
2013-07-09
*
Using the whole tactic environment while Pretyping.
ppedrot
2013-06-24
*
Generalizing the use of maps instead of lists in the interpretation
ppedrot
2013-06-22
*
- Keep the refinement of existing evars comming from unification with a rewri...
msozeau
2013-06-19
*
One more fix for rewrite: disallow resolving of the (partial) constraints
msozeau
2013-06-12
*
Replacing lists by maps in matching interpretation.
ppedrot
2013-06-05
*
Do not compute fallback eagerly in Evarconv
pboutill
2013-05-30
*
export Unification.abstract_list_all_with_dependencies
pboutill
2013-05-30
*
Why not going inside fixpoint definition with appcontext ?
pboutill
2013-05-30
*
comments in mli
pboutill
2013-05-30
*
Pushing lazy lists into Ltac. Now, the control flow is explicit
ppedrot
2013-05-28
*
Code cleaning in Matching.
ppedrot
2013-05-24
*
Mini documentation (evar_absorb_arguments).
herbelin
2013-05-14
*
Delayed the computation of parameters in sort polymorphism of
herbelin
2013-05-14
*
"change ... in ..." and "simpl ... in ..." now consider nested
herbelin
2013-05-14
*
Fixing a regression in unification introduced in r16205 (error raised
herbelin
2013-05-14
*
Removing Gmap from Classops. Fold order only mattered for printing.
ppedrot
2013-05-14
*
Removing useless uses of Gmap.
ppedrot
2013-05-14
[next]