]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: cc7e298) | patch
1) moved select and pattern_of from cicUtil to proofEngineHelpers
authorEnrico Tassi <enrico.tassi@inria.fr>
Mon, 27 Jun 2005 10:42:27 +0000 (10:42 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Mon, 27 Jun 2005 10:42:27 +0000 (10:42 +0000)
commitf85e6f52232af229b80a8447492cfae80f95d832
tree0d6f4bcc5e3c9b763453f284a8efb1a5b0841c4ftree | snapshot
parentcc7e298cf9d19f6f7230a4796b945836c30f1ccdcommit | diff
1) moved select and pattern_of from cicUtil to proofEngineHelpers
2) select now returns a couple (context, term) so that we can build the right context from each returned term
helm/ocaml/cic/cicUtil.ml diff | blob | history
helm/ocaml/cic/cicUtil.mli diff | blob | history
helm/ocaml/cic_proof_checking/.depend diff | blob | history
helm/ocaml/tactics/.depend diff | blob | history
helm/ocaml/tactics/equalityTactics.ml diff | blob | history
helm/ocaml/tactics/proofEngineHelpers.ml diff | blob | history
helm/ocaml/tactics/proofEngineHelpers.mli diff | blob | history
helm/ocaml/tactics/reductionTactics.ml diff | blob | history
helm/ocaml/tactics/variousTactics.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.