aboutsummaryrefslogtreecommitdiff
path: root/.depend
AgeCommit message (Expand)Author
2007-07-13New bootstrapping, improved, Makefile systemcorbinea
2007-07-12normalisation (by closure) was not performed under fixpointsbarras
2007-06-26additional properties for FMap (and slight rework of SetoidList and FSetPrope...letouzey
2007-06-14Correction du bug sur make dependnotin
2007-05-20- Propagation des evars non résolues vers les with_bindings; permet par exempleherbelin
2007-05-11Processor integers + Print assumption (see coqdev mailing list for the aspiwack
2007-04-16Export de simplest_eapply, utilisé dans la contrib interfacenotin
2007-04-16fix bug with dependent inductive familiescorbinea
2007-04-05On n'a plus besoin de compiler les anciens fichiers de functionnal induction ...jforest
2007-03-30Modifications dans Makefile: notin
2007-03-27Modification de la vm:notin
2007-03-22A tentative fix for bug #1455lmamane
2007-01-29finalized sufficescorbinea
2007-01-22changes in declarative language : by term using tacticcorbinea
2007-01-10Merge from Lionel Elie Mamane's private branch:lmamane
2006-12-11Changement dans le kernel : bgregoir
2006-12-09git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9423 85f007b7-540e-04...filliatr
2006-12-03MAJherbelin
2006-10-30dependencesbarras
2006-10-29Suite commit polymorphismeherbelin
2006-10-28Extension du polymorphisme de sorte au cas des définitions dans Type.herbelin
2006-10-26Experimental merging of two functional graphs.courtieu
2006-10-25conflit de nom (Field_theory) modulo la cassebarras
2006-09-26petits pbs de dependancesbarras
2006-09-26Compilation newringnotin
2006-09-26mise a jour du nouveau ring et ajout du nouveau field, avant renommagesbarras
2006-09-20Declarative Proof Language: main commitcorbinea
2006-09-19added congruence improvementcorbinea
2006-09-15Report de l'heuristique d'unification premier ordre flexible/rigideherbelin
2006-08-22+ Changing "in <hyp>" to "in <clause>" (no at, no InValue and nojforest
2006-07-22- Ajout d'un cast vm dans la syntaxe : x <: t bgregoir
2006-07-04functional inversion now takes a quatified hypothesis as first argumentjforest
2006-06-23Fix wrong order of existentials in eterm.msozeau
2006-06-08MAJ Makefile dependherbelin
2006-05-18Dépendances pour List.vnotin
2006-05-03Fixing two minor bugs in recdef and graph of function generation. jforest
2006-05-03Cleanning and factorizing code in funind. Spliting new_arg_principles into to...jforest
2006-04-27MAJherbelin
2006-03-22Made pretyping a functor over a coercion implementation. Pretyping.Default us...msozeau
2006-03-22- Réintroduction d'un parseur de pattern (q_constr.ml4) à usage deherbelin
2006-03-15Ajout de theories/FSets contenant la partie "light" de FSets et FMap:letouzey
2006-03-08 r8623@thot: notin | 2006-03-08 12:40:57 +0100notin
2006-03-08 r8620@thot: notin | 2006-03-08 11:44:16 +0100notin
2006-03-05majcoq
2006-03-02majcoq
2006-02-27majcoq
2006-02-27dp: sortie Whyfilliatr
2006-02-22majcoq
2006-02-21majcoq
2006-02-20majcoq
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 10:12:13 +0000