index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
parsing
/
q_coqast.ml4
Commit message (
Expand
)
Author
Age
*
Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme...
herbelin
2006-05-30
*
+ destruct now works as induction on multiple arguments :
jforest
2006-03-21
*
induction now admits multiple induction arguments. The principle must
coq
2006-02-10
*
Ajout option 'using lemmas' à auto/trivial/eauto
herbelin
2006-01-28
*
Messages de idtac et fail peuvent maintenant être des listes de string, int ...
herbelin
2006-01-21
*
Ajout motif d'introduction "?" (IntroAnonymous) pour laisser Coq
herbelin
2006-01-16
*
- Tactic "assert" now accepts "as" intro patterns and "by" tactic clauses
herbelin
2006-01-16
*
Petite correction nom QuantHypArgType suite suppression traducteur
herbelin
2005-12-26
*
Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...
herbelin
2005-12-26
*
Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...
herbelin
2005-05-17
*
Allow auto to have a parametric argument (wish #967)
herbelin
2005-05-15
*
Added 'clear - id' to clear all hypotheses except the ones dependent in the s...
herbelin
2005-03-07
*
ExtraRedExpr maintenant sans argument: pas très souple mais au moins convien...
herbelin
2004-12-29
*
Restauration type casted_open_constr pour tactique refine car l'unification n...
herbelin
2004-12-09
*
Généralisation de CastedOpenConstrArg en OpenConstrArg, à charge des tacti...
herbelin
2004-12-06
*
IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).
sacerdot
2004-11-16
*
COMMITED BYTECODE COMPILER
barras
2004-10-20
*
'match term' now evaluates by default. Added 'lazy' keyword to delay the eval...
herbelin
2004-10-11
*
Dépendance en pa_ifdef dans la ligne camlp4deps de q_coqast induit make depe...
herbelin
2004-08-26
*
Distinction location ocaml 3.08 ou pas (suite)
herbelin
2004-07-29
*
Distinction location ocaml 3.08 ou pas
herbelin
2004-07-29
*
Abstraction vis à vis du type loc pour compatibilité ocaml 3.08
herbelin
2004-07-16
*
Nouvelle en-tête
herbelin
2004-07-16
*
Changement de natural en int_or_var pour 'do' et 'fail' pour paramétrisation...
herbelin
2004-03-02
*
Generalisation de la syntaxe de 'with_names' pour accepter 'as id' avec id va...
herbelin
2004-03-02
*
Généralisation du type ltac Identifier en IntroPattern; prise en compte des...
herbelin
2004-03-01
*
bugs avec Pose et Assert
barras
2004-01-09
*
Nouvelle tactique EExists
clrenard
2003-12-01
*
Uniformisation des politiques de nommage de NewDestruct sur arguments recursi...
herbelin
2003-11-25
*
reparation bug moins unaire (erreur de PP)
barras
2003-11-18
*
New tactics : econstructor, eleft, eright, esplit
clrenard
2003-11-17
*
factorisation et generalisation des clauses
barras
2003-11-13
*
Idtac peut prendre un argument à afficher
narboux
2003-11-12
*
Traduction semantique des InHyp de clause en InHypValue si local def
herbelin
2003-11-09
*
nouvelle syntaxe de ltac
barras
2003-10-16
*
changement nouvelle syntaxe (pt fixes)
barras
2003-10-10
*
Mise en place d'implicites par noms en v8
herbelin
2003-09-21
*
Nouvelle mouture du traducteur v7->v8
herbelin
2003-08-11
*
Ajout 'Symmetry in Hyp'
herbelin
2003-06-19
*
Utilisation de intro_pattern dans NewDestruct/NewInduction
herbelin
2003-06-13
*
Ajout notation c.(f) en v8 pour les projections de Record
herbelin
2003-06-10
*
Suppression définitive de lmatch et or_metanum dans tacinterp
herbelin
2003-05-21
*
Fusion à l'essai de lmatch et lfun dans tacinterp; utilisation de noms pour ...
herbelin
2003-05-21
*
Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern
herbelin
2003-05-19
*
Globalisation des noms de tactiques dans les définitions de tactiques
herbelin
2003-04-07
*
Ajout cas Match
herbelin
2003-04-07
*
Ajout d'un message à FailTac
herbelin
2003-03-31
*
*** empty log message ***
barras
2003-03-12
*
Légère amélioration des messages d'erreur des with-bindings et des Rewrite
herbelin
2002-12-21
*
Ajout Simpl et Change sur des sous-termes
herbelin
2002-12-09
[next]