index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
proofs
/
logic.ml
Commit message (
Expand
)
Author
Age
*
Util.option_compare devient Option.Misc.Compare et change un peu de type
aspiwack
2007-12-07
*
Plus de combinateurs sont passés de Util à Option. Le module Options
aspiwack
2007-12-06
*
Uniformisation politique de nommage evd/isevars (evd si evar_defs,
herbelin
2007-09-06
*
Correction d'un bug dans l'affichage du message d'erreur real_clean
herbelin
2007-05-29
*
Correction bug #1519
herbelin
2007-04-28
*
Suppression argument pattern_source du case_info (code jamais utilisé)
herbelin
2007-03-15
*
Correction d'un bug dans check_and_clear_in_constr + simplification de
notin
2007-01-31
*
Nouvelle implantation de clear_hyps
notin
2007-01-30
*
Correction du bug #1315:
notin
2007-01-22
*
Débranchement du polymorphisme de sorte sur les définitions dans Type
herbelin
2006-10-30
*
Compatibilité du polymorphisme de constantes avec les sections.
herbelin
2006-10-29
*
Extension du polymorphisme de sorte au cas des définitions dans Type.
herbelin
2006-10-28
*
Changement de comportement du [rewrite ... in H]: Coq échoue si H
notin
2006-10-03
*
Declarative Proof Language: main commit
corbinea
2006-09-20
*
- Indtypes: en attente opinion CoRN, les occurrences de Type non explicites
herbelin
2006-05-28
*
patch pour contourner l'échec de type_of_applied_inductive sur un inductif a...
herbelin
2006-04-11
*
Inductifs avec polymorphisme de sorte (version initiale)
herbelin
2006-03-29
*
Patch envoy\'e par Benjamin Gregoire, permettant de corriger
letouzey
2006-03-24
*
Correction bug #842 (rename d'une hyp du contexte)
herbelin
2006-03-01
*
Création d'un type d'erreur RecursionSchemeError distinct de InductiveError ...
herbelin
2005-12-17
*
Changement des named_context
gregoire
2005-12-02
*
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
*
Correction erreur grossière de non restauration d'état en cas de retour exc...
herbelin
2005-03-19
*
restructuration des printers: proofs passe avant parsing
barras
2004-09-17
*
When refining a given term, the primitive refiner used to accepts some casts,
sacerdot
2004-09-10
*
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
*
open superflu
herbelin
2003-09-12
*
Affichage des tactiques en v8
herbelin
2003-04-07
*
Globalisation des noms de tactiques dans les définitions de tactiques
herbelin
2003-04-07
*
Bug Rename
herbelin
2003-02-08
*
Légère amélioration des messages d'erreur des with-bindings et des Rewrite
herbelin
2002-12-21
*
Option pour rendre les vérifications du refiner optionnelle
herbelin
2002-12-09
*
Bug non vérification non redondance par Cut
herbelin
2002-06-13
*
Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...
herbelin
2002-05-29
*
q: Commande introuvable.
herbelin
2002-04-12
*
Simplification de Proof_type.prim_rule
herbelin
2002-03-27
*
Clear ne substitue plus le corps dans le reste du but
barras
2002-03-07
*
Uniformisation convert_hyp
herbelin
2002-02-28
*
suppression de pop_named
barras
2002-02-22
*
petits changements cosmetiques sur les tactiques
barras
2002-02-15
*
prterm -> prterm_env
filliatr
2002-02-08
*
petit nettoyage de kernel/inductive
barras
2002-02-07
*
Ajout tactiques Rename et Pose; modifications pour Inversion
herbelin
2002-02-01
*
compat ocaml 3.03
filliatr
2001-12-13
*
nouvel algo de conversion plus uniforme
barras
2001-11-29
*
Suites modifs du noyau. Univ devient purement fonctionnel.
barras
2001-11-12
[next]