aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
Commit message (Expand)AuthorAge
* Ajout "simple apply" et "simple eapply" pour apply sans unfoldGravatar herbelin2008-04-01
* Ajout d'abbréviations/notations paramétriquesGravatar herbelin2008-03-30
* Interpret patterns for hypotheses types in match goal in type_scope (if not aGravatar msozeau2008-03-25
* Une passe sur les réels:Gravatar herbelin2008-03-23
* migration of the old IntMap library from StdLib to a user contrib (Cachan/Int...Gravatar letouzey2008-03-19
* Forget to update the CHANGES file after the commit r10180Gravatar vsiles2008-03-11
* Fix bugs that were reopened due to the change of setoidGravatar msozeau2008-03-08
* Fix bug #1704 (ordering of condition goals for (setoid)rewrite). As partGravatar msozeau2008-03-07
* Application patch #1807 sur hypothèse inutile de Rpower_OGravatar herbelin2008-02-27
* Essai de prise en compte de delta dans unify_0 (même sur termes non clos). Gravatar herbelin2008-02-13
* Documentation of CHANGES and refman doc for the implicit argument binderGravatar msozeau2008-02-08
* Suite révision 10495Gravatar herbelin2008-02-01
* Add new LetPattern construct to replace dest. syntax: let| pat := t in b is b...Gravatar msozeau2008-01-17
* Suite ajout raccourcis à compute et lazy pour réduire tout saufGravatar herbelin2007-11-09
* Cleanup attempt of Hints in *Interface.v files.Gravatar letouzey2007-10-21
* Révision de theories/Logic concernant les axiomes de descriptions.Gravatar herbelin2007-10-03
* Ajout de eelim, ecase, edestruct et einduction (expérimental).Gravatar herbelin2007-10-03
* Ajout infos de débogage de "universe inconsistency" quand option SetGravatar herbelin2007-09-30
* Forget to update the CHANGES fileGravatar vsiles2007-09-28
* Reals: prod_f_SO inclut f(0) dans le produit et devient prod_f_R0Gravatar herbelin2007-09-27
* Petit complément au commit 10131.Gravatar herbelin2007-09-21
* Utilisation d'un nouvel algorithme plus raffiné pour prendre en compte lesGravatar herbelin2007-09-04
* New bootstrapping, improved, Makefile systemGravatar corbinea2007-07-13
* More natural notation for intro pattern: @a -> ?aGravatar glondu2007-07-09
* If a fixpoint is not written with an explicit { struct ... }, then Gravatar letouzey2007-07-07
* a few works about my commits since FebruaryGravatar letouzey2007-07-06
* Documentation for commit 9774.Gravatar glondu2007-07-06
* New intro pattern "@A", which generates a fresh name based on A.Gravatar glondu2007-07-06
* - Ajout de la possibilité d'utiliser la notation Record pour lesGravatar herbelin2007-06-30
* Réaffichage des Structure/Record sous la forme RecordGravatar herbelin2007-05-28
* Nouvelle stratégie d'unification des types des with-bindings dansGravatar herbelin2007-05-22
* Nouveaux changements autour des implicites (notamment suite àGravatar herbelin2007-05-06
* Suite commit 9810Gravatar herbelin2007-04-29
* Ajout de la possibilité de faire référence dans certains cas à un nomGravatar herbelin2007-04-28
* Déplacement des opérations sur bool dans l'état initialGravatar herbelin2007-04-28
* Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.Gravatar herbelin2007-04-28
* - Correction d'un bug de make_clenv_binding_apply révélé par le commit 9771Gravatar herbelin2007-04-18
* Added the option to set/unset the automatic generation of elimination schemesGravatar vsiles2007-04-17
* Nettoyage des tactiques basées sur "simpl" (delta-réduction cachantGravatar herbelin2007-04-13
* Nouveau déplacement de constr, cette fois au niveau 8. En fait, il y aGravatar herbelin2007-04-11
* Remontée de constr de 1 à 5 (pour permettre des notations entre 1 et 5Gravatar herbelin2007-04-10
* Added back the tactics [apply -> ident], etc. to Tactics.v afterGravatar emakarov2007-04-02
* Prise en compte de l'environnement dans les pbs de conversion + MAJ CHANGESGravatar herbelin2007-02-21
* Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé deGravatar herbelin2007-02-13
* MAJ ringGravatar herbelin2007-01-31
* Nouvelle approche pour le discharge modulaireGravatar herbelin2007-01-10
* gestion speciale du niveau 5 des ltacGravatar barras2006-11-02
* fixed field_simplify + changed precedence of let and fun in ltacGravatar barras2006-10-30
* MAJGravatar herbelin2006-10-28
* MAJGravatar herbelin2006-10-06