aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
2004-09-29Hugly temporary notationsacerdot
2004-09-29The quoting function is now 100% complete.sacerdot
2004-09-28The quoting function is now almost complete (in the sense that it can findsacerdot
2004-09-27The quoting function of the reflexive tactic is now sound: all the termssacerdot
2004-09-27corrected bug when lhs is matched w.r.t deltabarras
2004-09-25- Prise en compte de Fail n (n>0) dans plusieurs cas qui avaientherbelin
2004-09-24New: (temporary) concrete syntax to specify the morphism signature:sacerdot
2004-09-24Simplifications concommitantes à la correction du bug #855herbelin
2004-09-24Correction bug report #855herbelin
2004-09-17restructuration des printers: proofs passe avant parsingbarras
2004-09-15hiding the meta_map in evar_defsbarras
2004-09-15put empty_env in hint clause (vo were becoming huge!)barras
2004-09-14evar tactic bugfixcorbinea
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-12inclusion de meta_map dans evar_defsbarras
2004-09-10simplification de clenvbarras
2004-09-10Dead code removed.sacerdot
2004-09-101. add_new_morphism now has a new optional argument that is the signaturesacerdot
2004-09-10add_new_morphism has now a new argument that is the signaturesacerdot
2004-09-10Add_new_morphism has now a new optional argument that is the signature ofsacerdot
2004-09-08unification encore...barras
2004-09-08* cleaning/renaming in Setoids.vsacerdot
2004-09-08The Coq part of the reflexive part can now deal with irreflexive relations too.sacerdot
2004-09-07deuxieme vague de modifs: evar_defs fonctionnelbarras
2004-09-07* The Coq part of the reflexive tactic setoid_rewrite is generalized tosacerdot
2004-09-03premiere reorganisation de l\'unificationbarras
2004-09-03New reflexive implementation of setoid_rewrite. The new implementationsacerdot
2004-09-03New command "Add Relation ..." (for the new implementation of setoid_*).sacerdot
2004-08-24Calling setoid_rewrite on a term H whose type (eq x y) was not an applicationsacerdot
2004-08-03Protection contre un indice d'evar égal à 0herbelin
2004-07-30Protection erreur find_eq_data dans decompEqThen et uniformisation messages d...herbelin
2004-07-23Major bug fixing and improvement of the setoid_{replace,rewrite} tactics:sacerdot
2004-07-23Since setoid_{replace,rewrite} now uses replace there is a circularitysacerdot
2004-07-23Setoid_replace.setoid_replace last argument (that was supposed to be alwayssacerdot
2004-07-16Nouvelle en-têteherbelin
2004-07-16Abstraction vis a vis de dummy_locherbelin
2004-07-02syntax compatibility fixcorbinea
2004-06-30instantiate entry: constr -> lconstrcorbinea
2004-06-29moved instantiate binding to extratacticscorbinea
2004-06-28more evar stuffcorbinea
2004-06-28Ajout de la coercion id dans context vers evaluable constant (bug #777)herbelin
2004-06-26effective evar refiningcorbinea
2004-06-02bug #787 de Rolandbarras
2004-06-02Clarify the distinction between quantified_hypothesis and declared_or_quantif...herbelin
2004-05-07Bug mauvais sigmaherbelin
2004-04-30Terminologie plus intuitive: evaluable -> unfoldableherbelin
2004-03-31Morphismes déclarés comme Lemma pas comme Definitionherbelin
2004-03-30Distinction entre declarations internes (p.ex. _subproof) et declarations uti...herbelin
2004-03-18Backtrack sur commit 1.20herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-15 23:49:06 +0000