]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 92c8709) | patch
- Procedural: we now reconstruct "let H := v in t" with "intros (1) H" when the goal...
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Tue, 12 May 2009 19:04:32 +0000 (19:04 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Tue, 12 May 2009 19:04:32 +0000 (19:04 +0000)
commit5bb62857c7d6906da3ab6b52a23505b8e62e6d06
tree13934ed568598feb75743dc07cf6b7352ecfe7e8tree | snapshot
parent92c870913842926076d44bb822ec47f9e0843bc4commit | diff
- Procedural: we now reconstruct "let H := v in t" with "intros (1) H" when the goal starts with an abbreviation. Clearbody before change in reactivated (to change the inferred type of the abbreviations of sort Prop)
- RELATIONAL: notation fixup
- character: autobatch fixup
- ng_tactics: dependences were not committed correctly
16 files changed:
helm/software/components/acic_procedural/procedural2.ml diff | blob | history
helm/software/components/ng_tactics/.depend diff | blob | history
helm/software/components/ng_tactics/.depend.opt diff | blob | history
helm/software/components/syntax_extensions/.depend diff | blob | history
helm/software/matita/contribs/RELATIONAL/NLE/inv.ma diff | blob | history
helm/software/matita/contribs/RELATIONAL/NLE/nplus.ma diff | blob | history
helm/software/matita/contribs/RELATIONAL/NLE/order.ma diff | blob | history
helm/software/matita/contribs/RELATIONAL/NLE/props.ma diff | blob | history
helm/software/matita/contribs/RELATIONAL/NPlus/defs.ma diff | blob | history
helm/software/matita/contribs/RELATIONAL/NPlus/fun.ma diff | blob | history
helm/software/matita/contribs/RELATIONAL/NPlus/inv.ma diff | blob | history
helm/software/matita/contribs/RELATIONAL/NPlus/monoid.ma diff | blob | history
helm/software/matita/contribs/RELATIONAL/ZEq/defs.ma diff | blob | history
helm/software/matita/contribs/RELATIONAL/ZEq/setoid.ma diff | blob | history
helm/software/matita/contribs/character/classes/props_pt.ma diff | blob | history
helm/software/matita/contribs/character/preamble.ma diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.