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.

Required by the new xslt_index.txt implementation.

Absolute URL to the Getter removed thanks to the new getxslt method
implementation.

No more absolute URLs: the getxslt method of the Getter is now
used uniformly.

Version number updated.

Bug fixed. The bug used to lead to divergence in certain cases (e.g. limit_mul).

- modified /getxslt method, now stylesheets are downloaded on the fly
  and may be kept on various servers
- uncommented /getdtd method
- removed /getstyleconf method
- changed semantics of dbm variables, now ".db" suffix must be present
  in environment variables that reference dbm files

Added ".db" suffix to urls_of_uris default value.