]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 0c6428d) | 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)
commit59d7f64e2e1a22ded8f9017942ca640fe62d886a
tree54f7b86ce4e18aede150dcb46ea92bc4129c8004tree | snapshot
parent0c6428dca864b9bae4b8d09c8f4d40c214815633commit | 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
helm/software/components/tactics/destructTactic.ml diff | blob | history
helm/software/matita/contribs/LOGIC/CLE/defs.ma diff | blob | history
helm/software/matita/contribs/LOGIC/Insert/defs.ma diff | blob | history
helm/software/matita/contribs/LOGIC/Lift/defs.ma diff | blob | history
helm/software/matita/contribs/LOGIC/PEq/defs.ma diff | blob | history
helm/software/matita/contribs/LOGIC/Track/pred.ma diff | blob | history
helm/software/matita/contribs/LOGIC/Weight/defs.ma diff | blob | history
helm/software/matita/contribs/LOGIC/datatypes_props/Sequent.ma diff | blob | history
helm/software/matita/library/decidable_kit/fintype.ma diff | blob | history
helm/software/matita/library/decidable_kit/list_aux.ma diff | blob | history
helm/software/matita/library/demo/propositional_sequent_calculus.ma diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.