]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: bd59745) | patch
Added a filter for uris in tactic "auto".
authorMatteo Selmi <matteo.selmi@mail.polimi.it>
Mon, 17 May 2004 20:58:56 +0000 (20:58 +0000)
committerMatteo Selmi <matteo.selmi@mail.polimi.it>
Mon, 17 May 2004 20:58:56 +0000 (20:58 +0000)
commit6150b8ef905aaea17b47ff466c067054f976cd8f
treecb9e2405664e8f799e50d229ce6875ea6c94638atree | snapshot
parentbd59745a232bff0e941e97170b88709d0ff6fdf2commit | diff
Added a filter for uris in tactic "auto".
Uris of theorems containing, in the conclusion or in the hypothesis, constants not present in the proof (hypothesis or conclusion) are filtered out.
helm/ocaml/tactics/Makefile diff | blob | history
helm/ocaml/tactics/filter_auto.ml [new file with mode: 0644] blob
helm/ocaml/tactics/filter_auto.mli [new file with mode: 0644] blob
helm/ocaml/tactics/newConstraints.mli diff | blob | history
helm/ocaml/tactics/tacticChaser.ml diff | blob | history
helm/ocaml/tactics/variousTactics.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.