fixed coercions

removed debug print

cosmetic fix to pp_location

added save_object_to_disk and basedir

added delift

added basedir and improved let{rec} syntax

better debug prints

added Basedir Ast

Added outtype inference to MutCase

Fixed bug in delift. The recursive call in the Meta case was on t and not
on t lifted to the meta local context.

- removed applyStylesheets
- added Print and print_kind to AST
- added coercion module

added list_obj and list_uri

- added code for Coercion command, Print Env command.
- better error report in matitac

- avoid redefinition of the same uri (checked in add_*_to_worls)
- defined add_inductive_def_to_world
- append owner to baseuri to minimize uri conflicts
- do not clear console!

uses CicPp.ppsort

- removed ancient debugging prints

- renamed Term_not_found exception (useless) with Object_not_found
  (now used)
- added getter exception handling. Now, hopefully, we will no longer see
  Pxp_types.At exception, but more meaningful ones (like Object_not_found)
- added in_libary which checks if an object exists (either in cache
  or via getter)
- in_cache: removed old debugging messages

- added handling of exceptions embedded in xml documents (usually coming
  from http_getter)
- added exception Getter_failure which wraps the above exception
- added exception Parser_failure for generic errors
- removed useless EmptyUri exception

exception carried in response xml documents are now split in two attributes:
"helm:exception" (exception name) and "helm:exception_arg" (exception
argument)

added helm:exception handling of Http_getter_types.Key_not_found

- sync with the new ApplyTransformation API

- Changed ApplyTransformation API to return both the mathml and acic,
  plus all the related tables
- Added the "Coercion" keyword to CicTextualParser2

snapshot, notably:
- attributes support
- new ApplyTransformation interface
- simil-coma commit, browser is partially implemented :(

uniformed prototype of mml_of_cic_{object,sequent}

syntax changes: "." at the end of the phrase instead of ";;"

attributes support

- attributes support
- removed ancient debug prints

attributes support (not yet in the pretty printer)

- attributes support
- default instance is 0 (not -1 !)

attributes support

added attributes support

- added string_of_sort
- attributes support

- added attributes support
- uses string_of_sort from CicPp

added attributes

added attribute support (not yet in the parser)

snapshot, notably:
- added hyperlink handling in check and proof window
- start implementation of cic browser

helmns -> helm_ns

- added rendering of constants/variable with/without body

rendering fixes:
- does not assert false for a missing idref on a symbol (which is not
  available when rendering ast coming from parsing)
- fixed pattern matching rendering

- helmns -> helm_ns
- added xlink_ns

added cast rendering (used in check window by gTopLevel/matita)

added URI concrete syntax

added cmdline alias "command" for "tactica"

coercion application

fix coercGraph.mli

fixed #xpointer handling in uri_of_string. new examples :

"cic:/a/b/c.con" => [| "cic:/a" ; "cic:/a/b" ; "cic:/a/b/c.con" ; "c"; "" |]

"cic:/a/b/c.ind#xpointer(1/1)" =>
  [| "cic:/a" ; "cic:/a/b" ; "cic:/a/b/c.con" ; "c"; "#xpointer(1/1)" |]

"cic:/a/b/c.ind#xpointer(1/1/1)" =>
  [| "cic:/a" ; "cic:/a/b" ; "cic:/a/b/c.con" ; "c"; "#xpointer(1/1/1)" |]

Added coercion handling module

license template

read uri from cmdline

added pp_location (pretty printer of ast location)

added script support

added latex style comment, with start token "%%"

removed spurious debugging prints

snapshot, notably:
- first commit of matitac

fixed comments

- added helm_ns and xhtml_ns (XHTML and HELM namespace, respectively)
- changed usage string so that it is a well fermod XHTML document (added
  namespace, quoted ampersands)

new cicEnvironment implementation

No longer return HTTP 400 answers or non-xml answers: all document returned
by the getter are now XHTML documents, possibly with the addition of an
attribute helm:exception on the root <html> element in the
http://www.cs.unibo.it/helm namespace. The presence of such an attribute
means that an exception has occured, its value is meant to be a string
encoding of the relevant ocaml exception

first (almost) working version: apparently, only generation of coinductive
eliminators does not typecheck

snapshot, notably:
- changed interface, now returns a Cic.obj
- added consistency check between generated body and type

snapshot (1st commit of fix body generation)

fixed clean_and_fill

fixed bug in fill_and_clean (now the helper universes_of_obj knows that
the uri passed as the first parameter can't be in the environment and it
doesn't requests it)

snapshot, notably:
- added support for inductive definitions
- prelimnary support for user searches

added fallback case (assertion failure) for unsupported Implicit annotations

added syntax for URIs

added search commands

- added pack/unpack over AST of terms
- created cicAst.mli (it was missing)

- added pack/unpack over AST of terms
- created cicAst.mli (it was missing)
- added syntax for URIs

added clean_and_fill, to be invoked on qed

snapshot, not yet completed, but ...

- added support for contexts (terms with holes)
- added CicUtil.pack/unpack to pack/unpack several terms in a single term
- added CicUtil.strip_prods to removed a given number of head prods from a term
- added CicUtil.context_of/select to create contexts/select a subterm
  matching a context

cosmetic changes

added begin list and end list comments to help moogle search engine plugin

exported lift_from

snapshot

added an hyperlink to the input syntax page

improved input syntax page with example queries of elim, match and hint

added URI printing in the result page (so that mouse-over is not the
only way to know the URI of results!)

first commit (in the wrong place --by CSC) of induction principles generation

ignores example binaries

ported to new format of Parse_error exception (which includes error position)

(dummy) porting to universes

implemented pretty printer for (mutual) (co)inductive types

(first) complete implementation of (mutual) (co)inductive types syntax

addded inductive definition to AST

- enriched Parse_error exception with error location
- first implementation of inductive type definitions (not yet completed:
  mutual inductive definition are still missing)
- test parser now displays error location using ASCII escape coloring

symmetry of equality NOT used in auto

New version of auto with "width".

snapshot

moogle syntax help page, actually contains only syntax and examples for
the "locate" query. "hint", "match" and "elim" syntaxes are currently
undocumented

changed "locate" so that it supports shell-like pattern matching with
'*' and '?' wildcards

ported to universes

*** empty log message ***

sync with universes and ~subst (and not ?(subst=[]))

Added universes handling. Tag PRE_UNIVERSES may help ;)

Added universes handling. The PRE_UNIVERSES tag may help ;)

Bug in the management of substitutions into auto corrected.
No significative loss in performance.
Comments commented.

- ported tests to newer PP / substitutions

- passes subst to FreshNameGenerator
- removed some old debugging prints