aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2004-09-30cutrewrite does not work with relations that are not Coq-like equalities.sacerdot
2004-09-30setoid_replace E1 with E2sacerdot
2004-09-29majfilliatr
2004-09-29* error messages improvedsacerdot
2004-09-29Add Relation is now able to detect non well typed relation registrations.sacerdot
2004-09-29The Add Morphism command is now able to detect in advance:sacerdot
2004-09-29New syntaxsacerdot
2004-09-29The Prod special case works only when the premise is of type Prop.sacerdot
2004-09-291. major code clean-up for the Prod casesacerdot
2004-09-29impl is a reflexive relation (it used to be areflexive).sacerdot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-20 00:45:47 +0000