aboutsummaryrefslogtreecommitdiffhomepage
path: root/.depend
Commit message (Expand)AuthorAge
* Export de simplest_eapply, utilisé dans la contrib interfaceGravatar notin2007-04-16
* fix bug with dependent inductive familiesGravatar corbinea2007-04-16
* On n'a plus besoin de compiler les anciens fichiers de functionnal induction ...Gravatar jforest2007-04-05
* Modifications dans Makefile: Gravatar notin2007-03-30
* Modification de la vm:Gravatar notin2007-03-27
* A tentative fix for bug #1455Gravatar lmamane2007-03-22
* finalized sufficesGravatar corbinea2007-01-29
* changes in declarative language : by term using tacticGravatar corbinea2007-01-22
* Merge from Lionel Elie Mamane's private branch:Gravatar lmamane2007-01-10
* Changement dans le kernel : Gravatar bgregoir2006-12-11
* git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9423 85f007b7-540e-04...Gravatar filliatr2006-12-09
* MAJGravatar herbelin2006-12-03
* dependencesGravatar barras2006-10-30
* Suite commit polymorphismeGravatar herbelin2006-10-29
* Extension du polymorphisme de sorte au cas des définitions dans Type.Gravatar herbelin2006-10-28
* Experimental merging of two functional graphs.Gravatar courtieu2006-10-26
* conflit de nom (Field_theory) modulo la casseGravatar barras2006-10-25
* petits pbs de dependancesGravatar barras2006-09-26
* Compilation newringGravatar notin2006-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
* added congruence improvementGravatar corbinea2006-09-19
* Report de l'heuristique d'unification premier ordre flexible/rigideGravatar herbelin2006-09-15
* + Changing "in <hyp>" to "in <clause>" (no at, no InValue and noGravatar jforest2006-08-22
* - Ajout d'un cast vm dans la syntaxe : x <: t Gravatar bgregoir2006-07-22
* functional inversion now takes a quatified hypothesis as first argumentGravatar jforest2006-07-04
* Fix wrong order of existentials in eterm.Gravatar msozeau2006-06-23
* MAJ Makefile dependGravatar herbelin2006-06-08
* Dépendances pour List.vGravatar notin2006-05-18
* Fixing two minor bugs in recdef and graph of function generation. Gravatar jforest2006-05-03
* Cleanning and factorizing code in funind. Spliting new_arg_principles into to...Gravatar jforest2006-05-03
* MAJGravatar herbelin2006-04-27
* Made pretyping a functor over a coercion implementation. Pretyping.Default us...Gravatar msozeau2006-03-22
* - Réintroduction d'un parseur de pattern (q_constr.ml4) à usage deGravatar herbelin2006-03-22
* Ajout de theories/FSets contenant la partie "light" de FSets et FMap:Gravatar letouzey2006-03-15
* r8623@thot: notin | 2006-03-08 12:40:57 +0100Gravatar notin2006-03-08
* r8620@thot: notin | 2006-03-08 11:44:16 +0100Gravatar notin2006-03-08
* majGravatar coq2006-03-05
* majGravatar coq2006-03-02
* majGravatar coq2006-02-27
* dp: sortie WhyGravatar filliatr2006-02-27
* majGravatar coq2006-02-22
* majGravatar coq2006-02-21
* majGravatar coq2006-02-20
* majGravatar coq2006-02-17
* majGravatar coq2006-02-09
* majGravatar coq2006-02-08
* Julien:Gravatar bertot2006-02-08
* majGravatar coq2006-02-07
* majGravatar coq2006-02-04