projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: f1efdff) | patch
- destruct tactic: automatic simplification in case of failure removed
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Mon, 12 Nov 2007 18:35:12 +0000 (18:35 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Mon, 12 Nov 2007 18:35:12 +0000 (18:35 +0000)
commit5aa4da5846c72942f3d204f71ecfba8d6cc7911b
tree3fb8e5f9d7188847468a21fcec621228517e67c8tree | snapshot
parentf1efdff5ded26d264f2848ff53c19fe2099682a3commit | diff
- destruct tactic: automatic simplification in case of failure removed
- library scripts: changed accordingly
- LOGIC: injection lemmas for the coercions added and applied where neaded

Note: destruct does not whd the equality argument as the old subst did
components/tactics/destructTactic.ml diff | blob | history
matita/contribs/LOGIC/CLE/defs.ma diff | blob | history
matita/contribs/LOGIC/Insert/defs.ma diff | blob | history
matita/contribs/LOGIC/Lift/defs.ma diff | blob | history
matita/contribs/LOGIC/PEq/defs.ma diff | blob | history
matita/contribs/LOGIC/Track/pred.ma diff | blob | history
matita/contribs/LOGIC/Weight/defs.ma diff | blob | history
matita/contribs/LOGIC/datatypes_props/Sequent.ma diff | blob | history
matita/library/decidable_kit/fintype.ma diff | blob | history
matita/library/decidable_kit/list_aux.ma diff | blob | history
matita/library/demo/propositional_sequent_calculus.ma diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.