Change (or better define) the order of hints premises.
They are now processed top to bottom, and not viceversa as before. This seems
to be right thing, since rules like:
X := carr T
....
R := mk_foo ... (P X) ... T ...
--------------------------------- |-
carr R = (P X)
can't be written putting X := carr T last, but you really want to be sure that
the needed assumptions to obtain a foo (in that case, that X is the carrier of
a setoid T) are available _before_ you even try to typecheck the bigger
unification problem (that may not be well typed if X and carr T are not
_convertible_, since in the fix function called in instantiate we call the
typechecker and not the refiner).
Some refactoring in set*.ma, some new notations and new hints for \cup.
non uniform coercions still to be pushed from re-setoids.ma to a place
before sets.ma, maybe in hints_declaration.ma since they are complementary.
Ferruccio Guidi [Fri, 6 Aug 2010 23:26:57 +0000 (23:26 +0000)]
ld.dtd: updated to comply with crg
Makefiles: updated to comply with new HELM server configuration
top: some traces of old command line option "-m" removed
Ferruccio Guidi [Fri, 6 Aug 2010 18:23:25 +0000 (18:23 +0000)]
we renamed the module abbreviations according to src/modules.ml
ld.dtd: now is more strict
Makefiles: some refactoring
crg: bug fix in name/indexes translation
xmlLibrary: bug fix in the rendering of the "name" attribute: ^ is
forbidden in a NMTOKEN
brgOutput: new xml exportation via xmlCrg
Ferruccio Guidi [Fri, 6 Aug 2010 10:21:49 +0000 (10:21 +0000)]
txtLexer: bug fix in parsing the string tokens
library: we now export the "meta" attribute
crgXml: crg exportation factorized and alpha conversion now works
crgBrg: we now mark the abstraction and the reverse translation works
ld.dtd: updated to export crg contents
Ferruccio Guidi [Tue, 3 Aug 2010 20:54:58 +0000 (20:54 +0000)]
- we simplified the parser return values
- now the display of parser and lexer debug information is controlled
from the command line (with the options -P and -L)
complete_rg: now the empty binders are not treated especially
top: we isolated a fragment of slow code (process_streaming) to be
investigated. It can be enabled with the -1 command line option)
Makefile: we now create the etc directory when it is missing
Experimental enhancements to the ndestruct tactic. By using the syntax
ndestruct (e1 ... em) skip (H1 ... Hn)
the user can tell the tactic that
- only equations e1 ... em should be considered
- rewriting should happen only in hypotheses H1 ... Hn and in the goal
both "(e1 ... em)" and "skip (H1 ... Hn)" are optional parameters.
Fixed a bug in the undebruijnate function which caused the refiner to produce
a wrong object when refining mutually recursive functions (the references to
recursive calls would contain the wrong index to the recursive argument).
Enrico Tassi [Mon, 10 May 2010 09:48:33 +0000 (09:48 +0000)]
new intro:
- #; -- introduces into the context every possible assumption giving
to it an unusable name
- #h1 .. h2; -- multi intros
- intros; -- macro che espande a #h1...hn.
During unification of E1 with E2, E1 and E2 where not always reduced.
In particular, reduction was not performed in the cases:
LetIn vs LetIn, Match vs Match
and maybe also in some cases Appl Meta vs Appl Meta (who knows?)
* Fixed a couple of glitches in ndestruct
- blob equations were not always handled properly
- tactic used to fail due to not optimal behaviour of the refiner
* Added (experimental) support for JM equality to ndestruct
projects / helm.git / log