aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib
Commit message (Expand)AuthorAge
* Starting to add a function schemes merging command (not finished, notGravatar courtieu2006-10-20
* Correction sym -> commGravatar herbelin2006-10-19
* field_simplify_eq profite de la factorisation de LaurentGravatar barras2006-10-17
* affichage des ... dans les scriptsGravatar barras2006-10-16
* typo doc + bug legacy fieldGravatar barras2006-10-16
* changes the use of lists and notations, to avoid that the notationsGravatar bertot2006-10-16
* r9778@tannat: jforest | 2006-10-13 11:36:37 +0200Gravatar jforest2006-10-13
* Fix name clash on leftGravatar thery2006-10-12
* Fix 0 obligations bugGravatar msozeau2006-10-10
* Remove duplicate conditions in Field + Monomial substitution function for PExprGravatar thery2006-10-10
* make sure BinList is not made visible to files that use the tactic RingGravatar bertot2006-10-10
* Notations:Gravatar herbelin2006-10-09
* A version of natprering that should be more efficient and removal of a badGravatar bertot2006-10-05
* Arith NArith et ZArith exportent ring + nettoyage dans Ring_polynomGravatar barras2006-10-05
* Corrects the problem described in PR#1240:Gravatar bertot2006-10-05
* inefficacite de field_simplify_eqGravatar barras2006-10-04
* Correction bug #1211Gravatar notin2006-10-04
* Détection ocaml 3.09 des variables non utilisées (trop peu pour solliciter ...Gravatar herbelin2006-10-03
* bug dans field_simplifyGravatar barras2006-10-02
* Une passe sur l'injection et la discrimination...Gravatar herbelin2006-10-01
* args implicites dans FieldGravatar barras2006-09-29
* git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9188 85f007b7-540e-04...Gravatar barras2006-09-29
* separation de RealFieldGravatar barras2006-09-28
* git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9185 85f007b7-540e-04...Gravatar barras2006-09-28
* Add dependent list combinators test.Gravatar msozeau2006-09-28
* Detection des paramettres pour les Functions bien fondeesGravatar jforest2006-09-27
* petits pbs de dependancesGravatar barras2006-09-26
* Compilation newringGravatar notin2006-09-26
* commit de field + renommagesGravatar barras2006-09-26
* mise a jour du nouveau ring et ajout du nouveau field, avant renommagesGravatar barras2006-09-26
* Declarative Proof Language: main commitGravatar corbinea2006-09-20
* Gestion des arguments implicites dans les Functions bien fondeesGravatar jforest2006-09-19
* added congruence improvementGravatar corbinea2006-09-19
* correction of bug #1220Gravatar jforest2006-09-18
* Message modification in FunctionGravatar jforest2006-09-16
* Minor bug correction in well-founded Function.Gravatar jforest2006-09-15
* Report de l'heuristique d'unification premier ordre flexible/rigideGravatar herbelin2006-09-15
* mise en conformite des messages d'erreur de Function avec la doc.Gravatar jforest2006-09-14
* Fix wrong order for building library, add informative messages.Gravatar msozeau2006-09-04
* New handling of obligations.Gravatar msozeau2006-09-01
* Forgot to add this one.Gravatar msozeau2006-09-01
* Subtac fixes, new way of handling obligations in progress.Gravatar msozeau2006-09-01
* Suite commit 9110 (uniformisation position notation dans les blocs inductifs)Gravatar herbelin2006-09-01
* Ajout possibilité clause "where" dans co-points fixes Gravatar herbelin2006-09-01
* two minor bug corrections in General Recursive Functions Gravatar jforest2006-08-25
* Amelioration des messages d'erreur de Fucntion Gravatar jforest2006-08-24
* making otags working Gravatar jforest2006-08-22
* + Changing "in <hyp>" to "in <clause>" (no at, no InValue and noGravatar jforest2006-08-22
* + timide essai pour le traitement des as dans les patterns lors de la generat...Gravatar jforest2006-08-16
* working on functional induction automation (tactic finduction andGravatar courtieu2006-08-15
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 22:02:36 +0000