CIC Textual Parser added to the repository.
The Makefile stuff has been modified because of ocamllex and ocamlyacc rules.

----------------------------------------------------------------------
Modified Files:
1) schema-h.rdf schema-hth.rdf: bugs fixed
----------------------------------------------------------------------

----------------------------------------------------------------------
Modified Files:
1) schema-h.rdf schema-hth.rdf: added comments
Added Files:
1) 13-dcagent 21-euler dces dcq dctype eor: euler and dublin core schemas
----------------------------------------------------------------------

Generation of forward metadata using a lexical analyser.

The hash-table used in the implementation was of "type"
(UriManager.uri * int) -> Cic.obj

Is is now of type
UriManager.uri -> (int * Cic.obj) list

where the list is ordered from the most cooked to the less cooked.

There is almost no difference at all in the performance of big files
(limit_plus). The new design is easier to extend to a real cache with
rollback.

New architecture for the environment.
The final goal is to have a reentrant, session-aware environment that
also behaves as a true cache.

Fixing of guarded_by_constructors completed.
This is the idea of the implementation:
1) The guarded_by_constructors is called on a term which is going to produce
   an inductive type (in every branch).
2) The guarded_by_constructors now has also a parameter which is the list
   of arguments that are applied to the inductive type that the term
   we are cheking is going to produce.
3) Once the constructor is found, its type is "applied" to the list of
   arguments its inductive type is applied to. This operation gives us
   an instantiated constructor type.
4) Depending on the type of every argument in the instantiated constructor
   type, we call either the does_not_occur or the guarded_by_constructors
   on every term the constructor is applied to. In case we call the
   guarded_by_constructors, we also compute the new parameter (list of
   arguments the new inductive type was applied to).

Note that the analysis of the type of the constructors is based very closely
on the analysis of positivy of an inductive type.

Note also that some cases (e.g. a MutCase, a Fix or a CoFix in head position
in the backbone of the type of a constructor) has not been considered and
raises an exception.

PARTIAL COMMIT:
 The whole logic of the guarded_by_constructors is being changed.
 The new idea is this one:
  1) The guarded_by_constructors is applied to a term t which must always
     generate an inhabitant of an inductive data type or of a co-inductive
     data type.
  2) When it find a constructor in head position, then the constructor
     must construct the inductive or co-inductive data type of 1).
  3) The type of the formal parameter of a constructor determines what
     condition is checked on the actual parameters of the constructors:
     a) Not recursive: the function must not occur in the actual parameter
     b) Simply recursive (to be defined): the function must occur in the
        actual parameter only guarded by constructors (where the constructor
        has already been found).
     c) Imbricated (i.e. it is another inductive type applied to the one
        that is going to be recursively defined): in this case the guarded
        by constructors (where the constructor has already been found) must
        be called, but:
         I) the expected inductive data type is no more the old one, but
            the one of the inductive data type that is in head position in
            the type.
        II) Once (if) one constructor of I) will be found, its type must
            be considered only after the substitution of the left (?)
            parameters and considering recursion IN THE CO-INDUCTIVE TYPE
            THAT IS THE OUTPUT TYPE OF THE WHOLE COFIX.

What is still wrong with this commit is that we don't have the notion of
imbricated argument yet. So, as soon as an imbricated argument is found,
the invariant 1-3 are broken and sooner or later an exception is raised
or false is returned.

----------------------------------------------------------------------
Modified Files:
1) schema-h.rdf, schema-hth.rdf: updated DC schemas + class and
property refinements + value types.
----------------------------------------------------------------------

Bug fixed: the strictly_positive condition was unnecessarily too tight.

The typing rule for LetIn was simply wrong. Fixed.

Bug partially fixed: the branch of a case of type Prod can be not a Lambda.
(e.g. a Rel, a MutConstruct, etc.) I have fixed only the two cases of a
Rel and a MutConstruct.

Bug fixed: cooking w.r.t. a variable with a body must not increment
the number of left parameters.

It now exits gracefully after an End-of-file.

http:/ ==> http://

Very stupid bug fixed: in is_small, I created an environment in reverse order.

The definition of small inductive types has been relaxed: a constructor
is now considered small when its type without the parameters was small
with the previous definition. This is consistent with Coq's behaviour.

Debugging code removed to achieve more tail-recursivity.

Just code clean-up.

Discharging of variables with a body was bugged. Fixed.

* Code improvement: there were two different functions both named eat_prods.
  One has been renamed drop_prods.
* Bug fix: decast was still too weak. Replaced by CicReduction.whd everywhere.

does_not_occur now handles LetIn correctly (i.e. raising an exception
different from NotImplemented)

Error reporting improved.

is_small did not use the environment. Hence the List.nth exception. Fixed.

lift 0 was just a very heavy implementation of the identity function.

decast must also perform LetIn reduction now.

ppterm added

Makefile improved: dependencies from libraries are now considered.

----------------------------------------------------------------------
Added Files:
1) schema-h.rdf, schema-hth.rdf: first draft of rdf schemas for objects
and theories
----------------------------------------------------------------------

Dependencies from libraries now checked.

* Major code cleanup.
* Bug fixing: discharging of objects depending on variables with a body
  is now handled (more) correctly.

Makefile improved.

Main code clean-up.

cicAnnotationHinter.ml* were in the library without any reason.

cicAnnotationHinter.ml* have no reason to be in the library.
In this way, the dependency from lablgtk is removed.

Exception management improved.

...

New implementation of the proof-checker daemon: there is now
only one sequential (= non concurrent) proof-checker that process
one request at a time. The next big step will be to make it re-entrant.

CicCooking.init() must now be used to initialize the proof-checker library.

A .cmo file inside a .cma is linked iff it is referenced at least once.
This was not the case for cicCooking, that simply worked using side-effects
(i.e. registering one function of him to cicEnvironment).

So, I have created a new init function to initialize the wall proof-checker.

LetIn reduction (alias zeta-reduction) is now performed during whd.

LetIn was missing.

* .mli added where needed
* Install and uninstall implemented
* Makefile improvements

configure.in now used (just to check that ocaml and findlib are there)
Very small bug-fixes.

META files are now automatically generated from META-*.src files.
In this way all the hard-coded file paths have been removed.
Installation and uninstallation (still not implemented) should be also
easier.
Moreover, an error in a sub-directory now stops the whole processing.

First version of fix_params into CVS.

First versione of the proofChecker into CVS.

param.annotations was yes or NO. It is now yer or no.

annotations: was yes or NO. It is now yes or no.

First release of cicAnnotationHelper in CVS.
Uses the new HELM OCaml libraries.

.depend must be in the repository

New implementation using the new HELM OCaml libraries.

New implementation that uses the new HELM OCaml libraries.

1) .cma/.cmxa used to simplify META files.
2) Common parts of Makefiles factorized into Makefile.common
3) Makefile added

.cvsignore and .depend forgot

HELM OCaml libraries with findlib support.

initial checkin

Readme for the debianize.helm stuff.

Debianize.helm stuff.
Now you can check out a cvs revision and obtain a *clean* debianized source
tree executing "debian/debianize.helm".
Moreover the generated debian packages are native debian packages.

Synced debian dir.

Removed from debian dir.

Synced debian dir.

added config.sub and config.guess so that the package is ready for Debian

Content-type for MathML Content "fixed". Why was it broken?

out of sync w.r.t. configuration.ml

Underlining of hyperlinks removed.

mkMetaTheoryURL(): param.embedKeys() forgot.
Code improvement.

Changed version number to 0.2.1

BUG FIXED:
An maction with only one child does not have the same semantic
of an mrow. E.g.: when I click to un-expand a node, the first enclosing
maction is the one I am acting on. If it has only one child, nothing
happens. So, if an maction with only one child is put inside an maction with
two children, the inner one stops any possibility to unexpand the outer one.

Checks for mlminidom and lablgtk added.

Some spourious files removed.

...

.cvsignore improved

Disequalities chains for algebra. First draft.

Distribution improvements.

Now automatically generated from Makefile.in

No more used.

First commit towards the 0.2.8 version.

Bug fixed

Bug fixed: $< confused with $^

missing macro

HTTP_GETTER_URIS_DBM added

HTTP_GETTER_SERVERS_FILE introduced

Bug fix: changed "prefix" dir in install target.
Minor changes in debhelper usage.

Changed policy standard version.

Removed INSTALL (not needed) and NEWS (0 sized) from document list.

Remove template like string that lintian hates.

Set DH_COMPAT=2 (instead of 1).

Set section field. Changed maintainer field.

Changed maintainer field and set section field.

Removed temp files from repository.

Small improvement.

Simplification.

0.0.2 ==> 0.2.0 ;-)

- Check for ocamlfind added.
- .cvsignore improved

Unused variable removed.

mlminidom 0.0.2 for minidom 0.1.3

another small bug fixed about the pot

Bug fixed.

Required by the new getxslt method implementation.