index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
contrib
/
subtac
/
eterm.ml
Age
Commit message (
Expand
)
Author
2007-03-19
Add a parameter to QuestionMark evar kind to say it can be turned into an obl...
msozeau
2007-02-24
Opacity parameterization for obligations working.
msozeau
2007-02-23
Debug wellfounded defs, work on cleaning obls envs
msozeau
2007-01-15
Various subtac fixes.
msozeau
2006-11-10
Work on mutual defs, various bug fixes.
msozeau
2006-10-31
Debug obligation handling code
msozeau
2006-10-31
Work on obligation separation.
msozeau
2006-09-01
New handling of obligations.
msozeau
2006-09-01
Subtac fixes, new way of handling obligations in progress.
msozeau
2006-06-23
Fix wrong order of existentials in eterm.
msozeau
2006-06-01
Fix some nasty bug with the evars-to-dependent sum encoding.
msozeau
2006-04-27
Standardisation nom option_app en option_map
herbelin
2006-04-07
- Documentation of the Program tactics.
msozeau
2006-03-22
Subtac fixes, single fixpoint definitions are working again. Added a toggle o...
msozeau
2006-03-13
Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.
msozeau
2006-02-21
Work with binder lists, problem of tycons
coq
2006-02-21
Latest fixes, should work fine now for non recursive definitions, although st...
coq
2006-02-20
Rewrite of the subtac tactic, needs some work on implicit arguments.
coq
2005-12-02
Changement des named_context
gregoire
2005-07-15
Subtac: traitement correct des existentielles et de la récursion.
coq
