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
*
Prise en compte des defs syntaxiques dans is_global et global_reference qui p...
herbelin
2003-11-24
*
Bug introduit avec le 'Simpl f'
herbelin
2003-11-22
*
Ajout 'Simpl f'
herbelin
2003-11-21
*
Deplacement subst_rawconstr dans Rawterm
herbelin
2003-11-19
*
Ajout mis_constructor_nargs_env
herbelin
2003-11-18
*
Ajout reduce_to_quantified_ref
herbelin
2003-11-09
*
Amelioration message d'erreur pour ltac
herbelin
2003-11-04
*
Deplacement de iter_constr_with_full_binders dans Termops
herbelin
2003-10-22
*
Export is_section_variable
herbelin
2003-10-13
*
Deplacement next_global_ident_away dans Termops
herbelin
2003-10-13
*
Correction du bug 335 et Export/Require Export dans un module
coq
2003-10-07
*
Le nom '_' n'est plus valable en v8 pour nommer les variables
herbelin
2003-10-02
*
Oubli du type du terme a filtrer quand pas d'argument dans la traduction de case
herbelin
2003-09-29
*
Changement de l'afficheur pour que les variables liées aient un nom indépen...
herbelin
2003-09-23
*
Deplacement de Declare vers Termops
herbelin
2003-09-13
*
Déplacement de Declare juste à la fin de interp pour pouvoir accéder à in...
herbelin
2003-09-12
*
open superflu
herbelin
2003-09-12
*
Bug predicat old Case
herbelin
2003-09-10
*
Bug predicat let-tuple
herbelin
2003-09-09
*
Ajout construction If primitive dans constr_expr et rawconstr
herbelin
2003-09-09
*
Paramétrisation vis à vis de existential_key
herbelin
2003-09-06
*
Mise en place possibilité de définitions locales dans les paramètres des i...
herbelin
2003-09-06
*
V8: FUNCLASS -> Funclass, SORTCLASS -> Sortclass
herbelin
2003-08-31
*
Bug et améliorations diverses
herbelin
2003-08-12
*
Bug détypage du fix
herbelin
2003-08-12
*
Nouvelle mouture du traducteur v7->v8
herbelin
2003-08-11
*
Pb quand une meme classe est definie dans 2 fichiers
herbelin
2003-06-11
*
Simplification case_info
herbelin
2003-06-10
*
Ajout notation c.(f) en v8 pour les projections de Record
herbelin
2003-06-10
*
Factorisation de detype_case pour utilisation par l'afficheur de pattern
herbelin
2003-06-10
*
Amélioration afficheur de Cases pour les constr_pattern
herbelin
2003-06-10
*
Tables logarithmiques pour les coercions + nettoyage
herbelin
2003-06-08
*
Preservation affichage des ?n en V7
herbelin
2003-05-22
*
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
*
Rien d'important
herbelin
2003-05-13
*
Affichage des Fix contenant des Let dans leur context (ce que la tactique Fix...
herbelin
2003-04-27
*
simplification: fst (list_chop n l) = firstn n l et snd (list_chop n l) = lis...
letouzey
2003-04-16
*
Globalisation des noms de tactiques dans les définitions de tactiques
herbelin
2003-04-07
*
Globalisation des noms de tactiques dans les définitions de tactiques
herbelin
2003-04-07
*
Correction bug #261 + amélioration nommage
herbelin
2003-04-01
*
Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar)
herbelin
2003-03-29
*
*** empty log message ***
barras
2003-03-21
*
*** empty log message ***
barras
2003-03-12
*
Bug affichage let destructurant
herbelin
2003-02-02
*
Backtrack sur le filtrage des applications partielles (change Tauto/Intuition)
herbelin
2003-02-01
*
Ajout d'un filtrage d'application partielle
herbelin
2003-01-31
*
Unification plus efficace vis à vis du LetIn
herbelin
2003-01-31
*
reparation des contribs: lors de l'unification, reduire les beta redexes
barras
2003-01-23
[next]