aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2004-11-04Affichage des universherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6276 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-02Réponse à la conjecture que PI est indépendant de EM dans CCherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6273 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-28qq bugs du highlight de CoqIDEfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6267 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-28Added code to get rid of duplicate rewriting rules.sacerdot
A rule is a duplicate of another rule when their types are alpha convertible. Eliminating duplicates speed up the tactic (but it slows down the operation of addition of a new rule that is also performed every time subst_mps is applied to the module). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6266 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-28Ajout 'dependent rewrite in'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6265 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-27majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6264 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-27Factorisation cut_replacingherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6263 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-27Restructuration fonctions de réécriture depuis égalité dépendanteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6262 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-27Restructuration fonctions de réécriture depuis égalité dépendante; ↵herbelin
factorisation cut_replacing git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6261 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-27Ajout test dependent rewriteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6260 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-27Bug mauvais nom d'entrée binder_constr quand récursion gaucheherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6259 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-27Non affichage des notations réduites à une variableherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6258 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-26majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6257 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-25majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6256 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-25Word "setoid" banned from the error messages. "relation" used instead.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6255 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-25Added option -no-vm.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6254 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-25Missing check implemented (closes a bug from Bas Spitters).sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6253 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-24majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6252 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-22majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6251 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-21majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6250 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-21The morphism lemma type was simplified only in modules and not in modulesacerdot
types. Fixed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6249 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-21Error message improved.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6248 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-20majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6247 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-20majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6246 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-20COMMITED BYTECODE COMPILERbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6245 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-20bug in hashcons fun (List.for_all2 raises exn if given lists of <> lengths)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6244 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-20The bug already closed in revision 1.90 was reintroduced again.sacerdot
Closed again. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6243 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-19majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6242 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-19Proof term size reduction (again).sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6241 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-18majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6240 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-18majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6239 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-18* Code simplification and clean-up. In particular there is no more codesacerdot
duplicated between add_relation and add_setoid. * Less ad-hoc backward compatibility lemmas for setoids required in Setoid.v * Term size reduction (first part): when a relation is registered, we add to the environment a definition that gives back either the relation as an argument or as a relation class. The definition is used to reduce the term size. [ Note: we could save a bit more by defining two definitions in place of one. However, we suppose that the lambda term fragments generated can be shared quite effectively. Thus we would recive almost no benefit by sharing in terms of size. What about proof checking time? ] git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6238 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-18Code simplification and clean-up.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6237 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-18The lem field was not computed properly for morphisms whose argument wassacerdot
a quantified Leibniz relation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6236 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-18The "lem" field of a morphism used to be the compatibility proof, but itsacerdot
became the whole structure of type Morphism_Theory. A new field morphism_theory has now been added to record both informations. Print Setoids now prints again the right information. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6235 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-18Bug fixed: relations quantified more than once where abstracted in the wrongsacerdot
order (and thus they were not accepted). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6234 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-18More informative error message when the tactic tries to generate a newsacerdot
goal with metavariables in it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6233 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-18zeta flag added to reduce LetIns in a morphism type. Morphisms with localsacerdot
definitions in their types are now accepted. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6232 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-18Tacred après Typingherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6230 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-17majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6229 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-17Semble raisonnable de distinguer les noms aussi dans cant_applyherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6227 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-17Vérification de la typability de 'pattern'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6226 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-17*** empty log message ***herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6225 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-15majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6224 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-15majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6223 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-15Wrong comment committed. The tactic behaves correctly only when thesacerdot
relation/morphisms are quantified using LetIns. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6222 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-152 bugs de reconnaissancecoq
de fin de phrase corriges git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6218 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-15Wish of Maggesi implemented: the type of the morphism compatibility lemmasacerdot
is now the one that is shown to the user (and not only convertible to it). In this way it is possible to register the lemma in the Hint database. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6217 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-14majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6216 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-14Bug fixed (reported by Maggesi): sometimes when the tactic had to generate newsacerdot
existential variables it failed. Fixing by propagating the metavariable environment generated by the unification. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6215 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 00:07:43 +0000