index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
contrib
Commit message (
Expand
)
Author
Age
*
Modification of VernacScheme to handle a new scheme: Equality (equality in
vsiles
2007-05-25
*
fixed (PR#1483)
corbinea
2007-05-24
*
Nouvelle stratégie d'unification des types des with-bindings dans
herbelin
2007-05-22
*
- Propagation des evars non résolues vers les with_bindings; permet par exemple
herbelin
2007-05-20
*
correction de bug dans Function et augmentation de la classe des fonctions su...
jforest
2007-05-17
*
Processor integers + Print assumption (see coqdev mailing list for the
aspiwack
2007-05-11
*
Nouveaux changements autour des implicites (notamment suite à
herbelin
2007-05-06
*
Orthographe en passant
herbelin
2007-04-29
*
Ajout possibilité d'options à trois mots.
herbelin
2007-04-29
*
Ajout de la possibilité de faire référence dans certains cas à un nom
herbelin
2007-04-28
*
Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.
herbelin
2007-04-28
*
New keyword "Inline" for Parameters and Axioms for automatic
soubiran
2007-04-25
*
Correct implementation of undo in obligations handling code, correct some bug...
msozeau
2007-04-17
*
Export de simplest_eapply, utilisé dans la contrib interface
notin
2007-04-16
*
Mise en place d'une nouvelle strategie plus efficace pour les preuves de Func...
jforest
2007-04-05
*
Extension to the general sequence operator (tactical). Now in addition to ...
emakarov
2007-04-02
*
Support for implicit formal argument types in Program ; parse types in type s...
msozeau
2007-03-28
*
Make multiple patterns work again with Program while simplifying the code.
msozeau
2007-03-26
*
Some tactic fixes in Subtac, fix obvious bug in admit_obligations but still a...
msozeau
2007-03-20
*
traces Ergo
filliatr
2007-03-20
*
Forgot to update to new cast
msozeau
2007-03-19
*
Add a parameter to QuestionMark evar kind to say it can be turned into an obl...
msozeau
2007-03-19
*
r11153@tannat: jforest | 2007-03-16 10:25:55 +0100
jforest
2007-03-16
*
Suppression argument pattern_source du case_info (code jamais utilisé)
herbelin
2007-03-15
*
Add destruct_call variant where naming of introduced hypotheses is possible. ...
msozeau
2007-03-15
*
Add destruct_call_concl in SubtacTactics and fix obvious obligation handling ...
msozeau
2007-03-14
*
Solve obligation handling bug of trying to solve automatically at Next Obliga...
msozeau
2007-03-13
*
correction du bug 1432
jforest
2007-03-11
*
Remove bugguy notations
msozeau
2007-03-11
*
Create a program_scope in subtac Utils
msozeau
2007-03-08
*
The right tactics for definitions using measures.
msozeau
2007-02-28
*
Fix wf bug from F. Besson and work on ineqs generation.
msozeau
2007-02-27
*
Achèvement commit 9677 (suppression résidu v7 dans PrintGrammar)
herbelin
2007-02-24
*
Opacity parameterization for obligations working.
msozeau
2007-02-24
*
Debug wellfounded defs, work on cleaning obls envs
msozeau
2007-02-23
*
Échange des mots clés 'using' et 'with' en argument de 'firstorder' (wish #...
notin
2007-02-22
*
Correct coq depend, add eq_rect elimination tactic to SubtacTactics
msozeau
2007-02-19
*
Various little subtac fixes, add some useful tactics.
msozeau
2007-02-19
*
Add subtac keywords to coqide and coqdoc, add 'dec' as keyword in subtac Utils.
msozeau
2007-02-16
*
lift params appropriately, do not need to coerce to tycon
msozeau
2007-02-16
*
Update implementation for dependent types. Works just as well as before for s...
msozeau
2007-02-16
*
encodage des types
filliatr
2007-02-14
*
tactique yices
filliatr
2007-02-14
*
Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé de
herbelin
2007-02-13
*
Bug mineur dans la generation des principes d'induction pour Function
jforest
2007-02-12
*
Fix matching on dependent types, taking a safe stand.
msozeau
2007-02-12
*
Correction d'un bug dans la génération des principes d'induction
jforest
2007-02-11
*
Retour r9310 en attendant mieux
herbelin
2007-02-09
*
Separate Tactics in subtac.
msozeau
2007-02-09
*
Add lif then else for if in bool.
msozeau
2007-02-08
[next]