* env renamed to context everywhere in cicTypeChecker.ml
* Definitions should be allowed in the contexts as well as Declarations.
This is the very first step: the notion of context is introduced in cic.ml
and the interface of cicTypeChecker.mli reflects that. (Of course, also the
interface of cicReduction should do the same!)
The new implementation just raises an exception when a definition is found
in the context.
Reduction tactics in the scratch window implemented.
NOTE: if you select an hypothesis and you apply a reduction tactic, nothing
will happen and no error message will be reported!
* Many improvements
* The interface now gives the user the possibility of (re-)opening an existing
constant.
* Tactic Elim no more exposed in the user interface. Replaced by ElimIntros.
* Selection of subterms in the hypothesis of the goal is now "sound".
* Reduction tactics (Whd, Reduce, Simpl) now work also on the hypothesis.
New bug/feature: their changes are lost when moving to another goal
and coming back afterwards.
* identifiers can now also have digits in them
* arrow notation for non-dependent Pi-abstraction introduced.
It seems to be bugged w.r.t. application (a problem of priority?)
* CicTextualParserContext provides an highly not-reentrant implementation
of parsing in a given environment
* Many improvements
* Added the possibility to select parts of the goal of a sequent and retrieve
the corresponding CIC term.
* New tactics implemented: Cut, Whd, Reduce, Simpl, Change
proofEngineReduction.ml added
It holds functions to perform reduction and simplification of terms.
They are used in the implementation of the reduction/conversion tactics.
* Bug fixed: applications of MutCase that are not iota-redexes were reduced
just to their head.
* More debugging enabled (to be removed when code becomes stable)
Andrea Asperti [Tue, 16 Apr 2002 09:00:50 +0000 (09:00 +0000)]
1. CicReduction moved into CicReductionNaif
2. CicReductionMachine is the new implementation based on an
"environment machine".
You must make a sumbolic link from one implementation (.ml) to
cicReduction.ml
Modified Files:
1) mmlnotation.xsl xslt_index.txt: MathML default presentation now is
generated by mmlctop.xsl
Added Files:
1) mmlctop.xsl mmlctop2_0.xsl: link and new Igor stylesheet for MathML default
presentation
* Many improvements
* Proofs are now rendered in natural language. The inner-types file is
store in /public/sacerdot/innertypes and directly retrieved from there.
We must find a better solution.
* Apply tactic now implemented. It is based on the unification stuff of
Andrea.
First commit of our future proof-assistant/proof-improver (???)
This commit is based on some un-committed changes to our libraries. So,
it won't compile out-of-the-box.
Debian changes for version 0.3.0 of lablgtkmathview.
Major changes:
- split shared library package
- debian native package, diff.gz is no longer needed
* Linking was still static for native compilation.
* Automatic compilation of the test in native mode can no more be performed
because the dynamic library is always searched in the position where
it will be installed ;-(
Irene Schena [Mon, 11 Mar 2002 14:39:53 +0000 (14:39 +0000)]
Modified Files:
1) html/Makefile html/proposal/.cvsignore xml/home.xml
xml/menu.xml xml/project.xml xml/proposal/EC-contribution.xml
xml/proposal/contribution.xml
xml/proposal/econ-scient-tech-prospects.xml
xml/proposal/innovation.xml
xml/proposal/project-components.xml
xml/proposal/project-management.xml
xml/proposal/project-objectives.xml
xml/proposal/project-planning.xml
xml/proposal/project-summary.xml xsl/project.xsl: now the proposal index is
in project.xml that is linked in the Project Menu
Removed Files:
1) xml/proposal/proposal-index.xml: now is in project.xml
projects / helm.git / log