index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
plugins
Commit message (
Expand
)
Author
Age
*
Fixing a significant efficiency leak in the code of the field tactic.
amahboub
2013-08-22
*
Nicer code concerning dirpaths and modpath around Lib
letouzey
2013-08-22
*
Misc changes around coqtop.ml :
letouzey
2013-08-22
*
Less "Coq" strings everywhere
letouzey
2013-08-22
*
micromega: remove empty file CheckerMaker
letouzey
2013-08-22
*
Field_theory : faster and nicer proofs + nice notations.
letouzey
2013-08-22
*
Ring_polynom : shorter proof for Psub_ok
letouzey
2013-08-22
*
Declarations.mli: reorganization of modular structures
letouzey
2013-08-20
*
calling interp by hand is forbidden
gareuselesinge
2013-08-08
*
get rid of closures in global/proof state
gareuselesinge
2013-08-08
*
Vernac classification streamlined (handles VERNAC EXTEND)
gareuselesinge
2013-08-08
*
State Transaction Machine
gareuselesinge
2013-08-08
*
Replacing uses of association lists by maps in notations.
ppedrot
2013-08-03
*
Replacing an association list by a map in globalizing environment.
ppedrot
2013-08-03
*
Tentative fix for #3054: we refresh universes in a term generated
ppedrot
2013-07-29
*
Lib.contents () instead of Lib.contents_after None
letouzey
2013-07-17
*
Extraction : message about lack of support for toplevel Include
letouzey
2013-07-17
*
Expurgating the useless difference between List0 and List1 at the
ppedrot
2013-07-05
*
Removed the distinction between generic Ltac vars and Let/Intro
ppedrot
2013-06-27
*
Useless use of maps in constr internalizing.
ppedrot
2013-06-25
*
Now, idtac closures use maps instead of association list.
ppedrot
2013-06-22
*
Generalizing the use of maps instead of lists in the interpretation
ppedrot
2013-06-22
*
Splitted up Genarg in four different levels:
ppedrot
2013-06-21
*
Cutting the dependency of Genarg in constr_expr, glob_constr
ppedrot
2013-06-21
*
Revert "parse "of" as KEYID "of""
gareuselesinge
2013-06-21
*
parse "of" as KEYID "of"
gareuselesinge
2013-06-19
*
Removing the various glob/subst/interp registering functions for
ppedrot
2013-06-18
*
Hiding tactic value representations.
ppedrot
2013-06-10
*
Uniformizing generic argument types.
ppedrot
2013-06-06
*
Replacing lists by maps in matching interpretation.
ppedrot
2013-06-05
*
bwaa, a Pervasive.compare
pboutill
2013-05-30
*
newring.ml4: interp constr arg at interp time (not parse time)
gareuselesinge
2013-05-29
*
Removing Gmap from Extraction plugin
ppedrot
2013-05-12
*
Use the Hook module here and there.
ppedrot
2013-05-12
*
Use definition_entry to declare local definitions
gareuselesinge
2013-05-09
*
A uniformization step around understand_* and interp_* functions.
herbelin
2013-05-09
*
Uniformizing the [if_warn] flag used for warning printing and put
ppedrot
2013-05-08
*
States: frozen states can hold closures
gareuselesinge
2013-05-06
*
Little fix for Nsatz: hypotheses not directly relevant to the nsatz
herbelin
2013-05-05
*
Merging Context and Sign.
ppedrot
2013-04-29
*
Splitting Term into five unrelated interfaces:
ppedrot
2013-04-29
*
Indfun : use States.with_state_protection instead of freeze/unfreeze
letouzey
2013-04-23
*
code simplifications concerning Summary
letouzey
2013-04-22
*
More functional implementation of locality_flag and program_mode
gareuselesinge
2013-04-15
*
Backport r16394 from 8.4:
msozeau
2013-04-11
*
Revised infrastructure for lazy loading of opaque proofs
letouzey
2013-04-02
*
Minor code cleaning in CArray / CList.
ppedrot
2013-03-23
*
Extraction AccessOpaque is now activated again by default (#2952)
letouzey
2013-03-18
*
Extract_env : correct exceptions mentionned in a try ... with
letouzey
2013-03-15
*
Restrict (try...with...) to avoid catching critical exn (part 15)
letouzey
2013-03-13
[next]