]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: da6e39e) | patch
The parser accepts terms with metavariables as statements of theorems ==>
authorStefano Zacchiroli <zack@upsilon.cc>
Tue, 6 Apr 2004 12:08:23 +0000 (12:08 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Tue, 6 Apr 2004 12:08:23 +0000 (12:08 +0000)
commitc517601da65ba49769c401105d36c293a2c92a71
treeaeb472c9f7577189e22bf02f42f31860fe6a3128tree | snapshot
parentda6e39e544f2bcb3fdddd18507f9f7f076161a14commit | diff
The parser accepts terms with metavariables as statements of theorems ==>
metavariable instantiation must be propagated also on the theorem statement.
helm/ocaml/tactics/proofEngineHelpers.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.