index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
proofs
Commit message (
Expand
)
Author
Age
*
Restructuration des points d'entrée de Pretyping et Constrintern
herbelin
2005-12-21
*
Création d'un type d'erreur RecursionSchemeError distinct de InductiveError ...
herbelin
2005-12-17
*
changement d'egalite pour le named_context_val
gregoire
2005-12-05
*
Changement des named_context
gregoire
2005-12-02
*
Nettoyage suite à la détection par défaut des variables inutilisées par o...
herbelin
2005-11-08
*
Confusion assert/error détectée par nouveau warning X de ocaml 3.09
herbelin
2005-11-04
*
catchable_exception laisse passer les InductiveError
werner
2005-10-27
*
Correction double bug #986: Fold ne préserve pas nécessairement le typage e...
herbelin
2005-07-13
*
unification: evar_define checks the free variables are bound in the evar context
barras
2005-05-28
*
Adoption du nom canonique global_of_constr pour éviter confusion avec type r...
herbelin
2005-05-20
*
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
*
Protection against saving a proof with still non-instantiated evars (cf bug #...
herbelin
2005-04-29
*
Protection against saving a proof with still non-instantiated evars (cf bug #...
herbelin
2005-04-29
*
Implementation of a new backtracking system, that allow to go back
coq
2005-04-20
*
Correction erreur grossière de non restauration d'état en cas de retour exc...
herbelin
2005-03-19
*
Added 'clear - id' to clear all hypotheses except the ones dependent in the s...
herbelin
2005-03-07
*
Ajout constructeur External pour appel outil externe à Coq
herbelin
2005-02-04
*
Compatibilité ocamlweb pour cible doc
herbelin
2005-01-21
*
Compatibilité ocamlweb pour cible doc
herbelin
2005-01-21
*
Partie reduction_of_red_expr de tacred.ml qui dépend de la vm maintenant dan...
herbelin
2005-01-02
*
Déplacement de 'project' dans Refiner pour supprimer des dépendances en Tac...
herbelin
2004-12-31
*
Suppression de la dépendance en Tacmach pour pouvoir être appelé de top_pr...
herbelin
2004-12-31
*
Code mort
herbelin
2004-11-18
*
Mise en page
herbelin
2004-11-17
*
COMMITED BYTECODE COMPILER
barras
2004-10-20
*
'match term' now evaluates by default. Added 'lazy' keyword to delay the eval...
herbelin
2004-10-11
*
restructuration des printers: proofs passe avant parsing
barras
2004-09-17
*
hiding the meta_map in evar_defs
barras
2004-09-15
*
inclusion de meta_map dans evar_defs
barras
2004-09-12
*
simplification de clenv
barras
2004-09-10
*
When refining a given term, the primitive refiner used to accepts some casts,
sacerdot
2004-09-10
*
unification encore...
barras
2004-09-08
*
deuxieme vague de modifs: evar_defs fonctionnel
barras
2004-09-07
*
deplacement de clenv vers pretyping
barras
2004-09-03
*
premiere reorganisation de l\'unification
barras
2004-09-03
*
Nouvelle en-tête
herbelin
2004-07-16
*
bugs #667 and #783 (mimick_evar and loc_table on large files)
barras
2004-07-13
*
bypass w_Define when w_refine-ing
corbinea
2004-07-07
*
updated printing of evar context (may loop ?)
corbinea
2004-06-30
*
moved instantiate binding to extratactics
corbinea
2004-06-29
*
more evar stuff
corbinea
2004-06-28
*
effective evar refining
corbinea
2004-06-26
*
Amélioration message d'erreur quand échec unification
clrenard
2004-04-20
*
Export du type de preuve en cours pour xml
herbelin
2004-03-29
*
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
*
Déplacement définition intro_pattern_expr dans Genarg
herbelin
2004-03-01
*
added breakpoints to help ide
corbinea
2004-02-26
*
Localisation des erreurs d'internalisation des notations de tactiques
herbelin
2004-02-12
[next]