aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2004-09-29impl relation and impl/and/or/not morphisms over impl declared.sacerdot
2004-09-291) bug fixed: new goals where compared according to the relation argumentssacerdot
2004-09-29The list of possible solutions proposed by the tactic cannot contain anysacerdot
2004-09-29Test updated.sacerdot
2004-09-29Hugly temporary notationsacerdot
2004-09-29The quoting function is now 100% complete.sacerdot
2004-09-28majfilliatr
2004-09-28majfilliatr
2004-09-28The quoting function is now almost complete (in the sense that it can findsacerdot
2004-09-27majfilliatr
2004-09-27The quoting function of the reflexive tactic is now sound: all the termssacerdot
2004-09-27?(mod_delta=true) parameter added to each unification function.sacerdot
2004-09-27firstorder bugfix to cope with elim of sigma types with goal is of the wrong ...corbinea
2004-09-27corrected bug when lhs is matched w.r.t deltabarras
2004-09-27collapse apps of patterns to avoid failuresbarras
2004-09-26majfilliatr
2004-09-26no-assert en mode natifherbelin
2004-09-25Ajoutsherbelin
2004-09-25Remplacement de l'exception NextOccurrence _ par PatternMatchingFailure dans ...herbelin
2004-09-25- Prise en compte de Fail n (n>0) dans plusieurs cas qui avaientherbelin
2004-09-24majfilliatr
2004-09-24majfilliatr
2004-09-24New: (temporary) concrete syntax to specify the morphism signature:sacerdot
2004-09-24Ajout bug #255herbelin
2004-09-24Simplifications concommitantes à la correction du bug #855herbelin
2004-09-24Correction bug report #855herbelin
2004-09-23majfilliatr
2004-09-23error if binder was already definedbarras
2004-09-22majfilliatr
2004-09-22majfilliatr
2004-09-22link order againbarras
2004-09-21majfilliatr
2004-09-20majfilliatr
2004-09-20pbs with link order and depsbarras
2004-09-19majfilliatr
2004-09-17majfilliatr
2004-09-17restructuration des printers: proofs passe avant parsingbarras
2004-09-17repaired depsbarras
2004-09-16majfilliatr
2004-09-15majfilliatr
2004-09-15hiding the meta_map in evar_defsbarras
2004-09-15put empty_env in hint clause (vo were becoming huge!)barras
2004-09-14majfilliatr
2004-09-14majfilliatr
2004-09-14evar tactic bugfixcorbinea
2004-09-13majfilliatr
2004-09-13* The ML tactic is now also aware of rewriting directions.sacerdot
2004-09-13The ML part of the tactic now knows about covariant and contravariant morphismsacerdot
2004-09-12majfilliatr
2004-09-12majfilliatr
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 08:10:30 +0000