]> matita.cs.unibo.it Git - helm.git/log
projects / helm.git / log
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
helm.git
19 years agoAdded outtype inference to MutCase
commit | commitdiff | tree
Enrico Tassi [Mon, 31 Jan 2005 17:11:14 +0000 (17:11 +0000)]
Added outtype inference to MutCase

19 years agoFixed bug in delift. The recursive call in the Meta case was on t and not
commit | commitdiff | tree
Enrico Tassi [Mon, 31 Jan 2005 17:10:38 +0000 (17:10 +0000)]
Fixed bug in delift. The recursive call in the Meta case was on t and not
on t lifted to the meta local context.

19 years ago- removed applyStylesheets
commit | commitdiff | tree
Enrico Tassi [Tue, 25 Jan 2005 09:32:35 +0000 (09:32 +0000)]
- removed applyStylesheets
- added Print and print_kind to AST
- added coercion module

19 years agoadded list_obj and list_uri
commit | commitdiff | tree
Enrico Tassi [Tue, 25 Jan 2005 09:28:50 +0000 (09:28 +0000)]
added list_obj and list_uri

19 years ago- added code for Coercion command, Print Env command.
commit | commitdiff | tree
Enrico Tassi [Tue, 25 Jan 2005 09:26:01 +0000 (09:26 +0000)]
- added code for Coercion command, Print Env command.
- better error report in matitac

19 years ago- avoid redefinition of the same uri (checked in add_*_to_worls)
commit | commitdiff | tree
Stefano Zacchiroli [Mon, 24 Jan 2005 16:22:32 +0000 (16:22 +0000)]
- 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!

19 years agouses CicPp.ppsort
commit | commitdiff | tree
Stefano Zacchiroli [Mon, 24 Jan 2005 16:20:29 +0000 (16:20 +0000)]
uses CicPp.ppsort

19 years ago- removed ancient debugging prints
commit | commitdiff | tree
Stefano Zacchiroli [Mon, 24 Jan 2005 16:18:13 +0000 (16:18 +0000)]
- removed ancient debugging prints

19 years ago- renamed Term_not_found exception (useless) with Object_not_found
commit | commitdiff | tree
Stefano Zacchiroli [Mon, 24 Jan 2005 16:17:33 +0000 (16:17 +0000)]
- 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

19 years ago- added handling of exceptions embedded in xml documents (usually coming
commit | commitdiff | tree
Stefano Zacchiroli [Mon, 24 Jan 2005 16:15:11 +0000 (16:15 +0000)]
- 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

19 years agoexception carried in response xml documents are now split in two attributes:
commit | commitdiff | tree
Stefano Zacchiroli [Mon, 24 Jan 2005 16:13:00 +0000 (16:13 +0000)]
exception carried in response xml documents are now split in two attributes:
"helm:exception" (exception name) and "helm:exception_arg" (exception
argument)

19 years agoadded helm:exception handling of Http_getter_types.Key_not_found
commit | commitdiff | tree
Stefano Zacchiroli [Mon, 24 Jan 2005 12:57:00 +0000 (12:57 +0000)]
added helm:exception handling of Http_getter_types.Key_not_found

19 years ago- sync with the new ApplyTransformation API
commit | commitdiff | tree
Enrico Tassi [Fri, 21 Jan 2005 11:52:24 +0000 (11:52 +0000)]
- sync with the new ApplyTransformation API

19 years ago- Changed ApplyTransformation API to return both the mathml and acic,
commit | commitdiff | tree
Enrico Tassi [Fri, 21 Jan 2005 11:49:03 +0000 (11:49 +0000)]
- Changed ApplyTransformation API to return both the mathml and acic,
  plus all the related tables
- Added the "Coercion" keyword to CicTextualParser2

19 years agosnapshot, notably:
commit | commitdiff | tree
Stefano Zacchiroli [Fri, 21 Jan 2005 09:40:48 +0000 (09:40 +0000)]
snapshot, notably:
- attributes support
- new ApplyTransformation interface
- simil-coma commit, browser is partially implemented :(

19 years agouniformed prototype of mml_of_cic_{object,sequent}
commit | commitdiff | tree
Stefano Zacchiroli [Fri, 21 Jan 2005 09:39:03 +0000 (09:39 +0000)]
uniformed prototype of mml_of_cic_{object,sequent}

19 years agosyntax changes: "." at the end of the phrase instead of ";;"
commit | commitdiff | tree
Stefano Zacchiroli [Fri, 21 Jan 2005 09:35:33 +0000 (09:35 +0000)]
syntax changes: "." at the end of the phrase instead of ";;"

19 years agoattributes support
commit | commitdiff | tree
Stefano Zacchiroli [Fri, 21 Jan 2005 09:33:11 +0000 (09:33 +0000)]
attributes support

19 years ago- attributes support
commit | commitdiff | tree
Stefano Zacchiroli [Fri, 21 Jan 2005 09:30:41 +0000 (09:30 +0000)]
- attributes support
- removed ancient debug prints

19 years agoattributes support (not yet in the pretty printer)
commit | commitdiff | tree
Stefano Zacchiroli [Fri, 21 Jan 2005 09:29:48 +0000 (09:29 +0000)]
attributes support (not yet in the pretty printer)

19 years ago- attributes support
commit | commitdiff | tree
Stefano Zacchiroli [Fri, 21 Jan 2005 09:29:15 +0000 (09:29 +0000)]
- attributes support
- default instance is 0 (not -1 !)

19 years agoattributes support
commit | commitdiff | tree
Stefano Zacchiroli [Fri, 21 Jan 2005 09:26:13 +0000 (09:26 +0000)]
attributes support

19 years agoadded attributes support
commit | commitdiff | tree
Stefano Zacchiroli [Fri, 21 Jan 2005 09:21:35 +0000 (09:21 +0000)]
added attributes support

19 years ago- added string_of_sort
commit | commitdiff | tree
Stefano Zacchiroli [Fri, 21 Jan 2005 09:21:16 +0000 (09:21 +0000)]
- added string_of_sort
- attributes support

19 years ago- added attributes support
commit | commitdiff | tree
Stefano Zacchiroli [Fri, 21 Jan 2005 09:20:58 +0000 (09:20 +0000)]
- added attributes support
- uses string_of_sort from CicPp

19 years agoadded attributes
commit | commitdiff | tree
Stefano Zacchiroli [Fri, 21 Jan 2005 09:20:09 +0000 (09:20 +0000)]
added attributes

19 years agoadded attribute support (not yet in the parser)
commit | commitdiff | tree
Stefano Zacchiroli [Fri, 21 Jan 2005 09:19:02 +0000 (09:19 +0000)]
added attribute support (not yet in the parser)

19 years agosnapshot, notably:
commit | commitdiff | tree
Stefano Zacchiroli [Thu, 20 Jan 2005 10:33:50 +0000 (10:33 +0000)]
snapshot, notably:
- added hyperlink handling in check and proof window
- start implementation of cic browser

19 years agohelmns -> helm_ns
commit | commitdiff | tree
Stefano Zacchiroli [Thu, 20 Jan 2005 10:32:38 +0000 (10:32 +0000)]
helmns -> helm_ns

19 years ago- added rendering of constants/variable with/without body
commit | commitdiff | tree
Stefano Zacchiroli [Thu, 20 Jan 2005 10:32:01 +0000 (10:32 +0000)]
- added rendering of constants/variable with/without body

19 years agorendering fixes:
commit | commitdiff | tree
Stefano Zacchiroli [Thu, 20 Jan 2005 10:31:25 +0000 (10:31 +0000)]
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

19 years ago- helmns -> helm_ns
commit | commitdiff | tree
Stefano Zacchiroli [Thu, 20 Jan 2005 10:26:58 +0000 (10:26 +0000)]
- helmns -> helm_ns
- added xlink_ns

19 years agoadded cast rendering (used in check window by gTopLevel/matita)
commit | commitdiff | tree
Stefano Zacchiroli [Thu, 20 Jan 2005 10:26:06 +0000 (10:26 +0000)]
added cast rendering (used in check window by gTopLevel/matita)

19 years agoadded URI concrete syntax
commit | commitdiff | tree
Stefano Zacchiroli [Thu, 20 Jan 2005 10:24:59 +0000 (10:24 +0000)]
added URI concrete syntax

19 years agoadded cmdline alias "command" for "tactica"
commit | commitdiff | tree
Stefano Zacchiroli [Thu, 20 Jan 2005 10:24:44 +0000 (10:24 +0000)]
added cmdline alias "command" for "tactica"

19 years agocoercion application
commit | commitdiff | tree
Enrico Tassi [Wed, 19 Jan 2005 16:03:27 +0000 (16:03 +0000)]
coercion application

19 years agofix coercGraph.mli
commit | commitdiff | tree
Enrico Tassi [Wed, 19 Jan 2005 15:48:44 +0000 (15:48 +0000)]
fix coercGraph.mli

19 years agofixed #xpointer handling in uri_of_string. new examples :
commit | commitdiff | tree
Enrico Tassi [Wed, 19 Jan 2005 15:26:12 +0000 (15:26 +0000)]
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)" |]

19 years agoAdded coercion handling module
commit | commitdiff | tree
Enrico Tassi [Wed, 19 Jan 2005 15:23:12 +0000 (15:23 +0000)]
Added coercion handling module

19 years agolicense template
commit | commitdiff | tree
Stefano Zacchiroli [Tue, 18 Jan 2005 18:18:56 +0000 (18:18 +0000)]
license template

19 years agoread uri from cmdline
commit | commitdiff | tree
Stefano Zacchiroli [Tue, 18 Jan 2005 18:18:35 +0000 (18:18 +0000)]
read uri from cmdline

19 years agoadded pp_location (pretty printer of ast location)
commit | commitdiff | tree
Stefano Zacchiroli [Tue, 18 Jan 2005 18:18:00 +0000 (18:18 +0000)]
added pp_location (pretty printer of ast location)

19 years agoadded script support
commit | commitdiff | tree
Stefano Zacchiroli [Tue, 18 Jan 2005 18:17:33 +0000 (18:17 +0000)]
added script support

19 years agoadded latex style comment, with start token "%%"
commit | commitdiff | tree
Stefano Zacchiroli [Tue, 18 Jan 2005 18:16:43 +0000 (18:16 +0000)]
added latex style comment, with start token "%%"

19 years agoremoved spurious debugging prints
commit | commitdiff | tree
Stefano Zacchiroli [Tue, 18 Jan 2005 18:15:57 +0000 (18:15 +0000)]
removed spurious debugging prints

19 years agosnapshot, notably:
commit | commitdiff | tree
Stefano Zacchiroli [Tue, 18 Jan 2005 18:15:25 +0000 (18:15 +0000)]
snapshot, notably:
- first commit of matitac

19 years agofixed comments
commit | commitdiff | tree
Enrico Tassi [Tue, 18 Jan 2005 09:21:25 +0000 (09:21 +0000)]
fixed comments

19 years ago- added helm_ns and xhtml_ns (XHTML and HELM namespace, respectively)
commit | commitdiff | tree
Stefano Zacchiroli [Mon, 17 Jan 2005 16:24:22 +0000 (16:24 +0000)]
- 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)

19 years agonew cicEnvironment implementation
commit | commitdiff | tree
Enrico Tassi [Mon, 17 Jan 2005 16:24:17 +0000 (16:24 +0000)]
new cicEnvironment implementation

19 years agoNo longer return HTTP 400 answers or non-xml answers: all document returned
commit | commitdiff | tree
Stefano Zacchiroli [Mon, 17 Jan 2005 16:23:26 +0000 (16:23 +0000)]
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

19 years agofirst (almost) working version: apparently, only generation of coinductive
commit | commitdiff | tree
Stefano Zacchiroli [Mon, 17 Jan 2005 14:53:03 +0000 (14:53 +0000)]
first (almost) working version: apparently, only generation of coinductive
eliminators does not typecheck

19 years agosnapshot, notably:
commit | commitdiff | tree
Stefano Zacchiroli [Fri, 14 Jan 2005 17:35:26 +0000 (17:35 +0000)]
snapshot, notably:
- changed interface, now returns a Cic.obj
- added consistency check between generated body and type

19 years agosnapshot (1st commit of fix body generation)
commit | commitdiff | tree
Stefano Zacchiroli [Thu, 13 Jan 2005 07:08:55 +0000 (07:08 +0000)]
snapshot (1st commit of fix body generation)

19 years agofixed clean_and_fill
commit | commitdiff | tree
Enrico Tassi [Wed, 12 Jan 2005 15:08:35 +0000 (15:08 +0000)]
fixed clean_and_fill

19 years agofixed bug in fill_and_clean (now the helper universes_of_obj knows that
commit | commitdiff | tree
Enrico Tassi [Wed, 12 Jan 2005 14:56:46 +0000 (14:56 +0000)]
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)

19 years agosnapshot, notably:
commit | commitdiff | tree
Stefano Zacchiroli [Tue, 11 Jan 2005 16:11:12 +0000 (16:11 +0000)]
snapshot, notably:
- added support for inductive definitions
- prelimnary support for user searches

19 years agoadded fallback case (assertion failure) for unsupported Implicit annotations
commit | commitdiff | tree
Stefano Zacchiroli [Tue, 11 Jan 2005 16:09:20 +0000 (16:09 +0000)]
added fallback case (assertion failure) for unsupported Implicit annotations

19 years agoadded syntax for URIs
commit | commitdiff | tree
Stefano Zacchiroli [Tue, 11 Jan 2005 16:08:24 +0000 (16:08 +0000)]
added syntax for URIs

19 years agoadded search commands
commit | commitdiff | tree
Stefano Zacchiroli [Tue, 11 Jan 2005 16:05:23 +0000 (16:05 +0000)]
added search commands

19 years ago- added pack/unpack over AST of terms
commit | commitdiff | tree
Stefano Zacchiroli [Tue, 11 Jan 2005 16:04:31 +0000 (16:04 +0000)]
- added pack/unpack over AST of terms
- created cicAst.mli (it was missing)

19 years ago- added pack/unpack over AST of terms
commit | commitdiff | tree
Stefano Zacchiroli [Tue, 11 Jan 2005 16:04:31 +0000 (16:04 +0000)]
- added pack/unpack over AST of terms
- created cicAst.mli (it was missing)
- added syntax for URIs

19 years agoadded clean_and_fill, to be invoked on qed
commit | commitdiff | tree
Stefano Zacchiroli [Tue, 11 Jan 2005 16:03:13 +0000 (16:03 +0000)]
added clean_and_fill, to be invoked on qed

19 years agosnapshot, not yet completed, but ...
commit | commitdiff | tree
Stefano Zacchiroli [Tue, 11 Jan 2005 16:02:53 +0000 (16:02 +0000)]
snapshot, not yet completed, but ...

19 years ago- added support for contexts (terms with holes)
commit | commitdiff | tree
Stefano Zacchiroli [Tue, 11 Jan 2005 16:01:46 +0000 (16:01 +0000)]
- 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

19 years agocosmetic changes
commit | commitdiff | tree
Stefano Zacchiroli [Tue, 11 Jan 2005 15:59:06 +0000 (15:59 +0000)]
cosmetic changes

19 years agoadded begin list and end list comments to help moogle search engine plugin
commit | commitdiff | tree
Enrico Tassi [Mon, 10 Jan 2005 10:47:47 +0000 (10:47 +0000)]
added begin list and end list comments to help moogle search engine plugin

19 years agoexported lift_from
commit | commitdiff | tree
Stefano Zacchiroli [Wed, 5 Jan 2005 14:07:33 +0000 (14:07 +0000)]
exported lift_from

19 years agosnapshot
commit | commitdiff | tree
Stefano Zacchiroli [Wed, 5 Jan 2005 14:06:41 +0000 (14:06 +0000)]
snapshot

19 years agoadded an hyperlink to the input syntax page
commit | commitdiff | tree
Stefano Zacchiroli [Tue, 21 Dec 2004 17:52:32 +0000 (17:52 +0000)]
added an hyperlink to the input syntax page

19 years agoimproved input syntax page with example queries of elim, match and hint
commit | commitdiff | tree
Stefano Zacchiroli [Tue, 21 Dec 2004 17:48:59 +0000 (17:48 +0000)]
improved input syntax page with example queries of elim, match and hint

19 years agoadded URI printing in the result page (so that mouse-over is not the
commit | commitdiff | tree
Stefano Zacchiroli [Tue, 21 Dec 2004 17:19:40 +0000 (17:19 +0000)]
added URI printing in the result page (so that mouse-over is not the
only way to know the URI of results!)

19 years agofirst commit (in the wrong place --by CSC) of induction principles generation
commit | commitdiff | tree
Stefano Zacchiroli [Tue, 21 Dec 2004 15:49:03 +0000 (15:49 +0000)]
first commit (in the wrong place --by CSC) of induction principles generation

19 years agoignores example binaries
commit | commitdiff | tree
Stefano Zacchiroli [Sat, 11 Dec 2004 16:32:14 +0000 (16:32 +0000)]
ignores example binaries

19 years agoported to new format of Parse_error exception (which includes error position)
commit | commitdiff | tree
Stefano Zacchiroli [Thu, 9 Dec 2004 20:31:24 +0000 (20:31 +0000)]
ported to new format of Parse_error exception (which includes error position)

19 years ago(dummy) porting to universes
commit | commitdiff | tree
Stefano Zacchiroli [Thu, 9 Dec 2004 20:29:44 +0000 (20:29 +0000)]
(dummy) porting to universes

19 years agoimplemented pretty printer for (mutual) (co)inductive types
commit | commitdiff | tree
Stefano Zacchiroli [Thu, 9 Dec 2004 17:20:56 +0000 (17:20 +0000)]
implemented pretty printer for (mutual) (co)inductive types

19 years ago(first) complete implementation of (mutual) (co)inductive types syntax
commit | commitdiff | tree
Stefano Zacchiroli [Thu, 9 Dec 2004 17:20:06 +0000 (17:20 +0000)]
(first) complete implementation of (mutual) (co)inductive types syntax

19 years agoaddded inductive definition to AST
commit | commitdiff | tree
Stefano Zacchiroli [Thu, 9 Dec 2004 15:18:50 +0000 (15:18 +0000)]
addded inductive definition to AST

19 years ago- enriched Parse_error exception with error location
commit | commitdiff | tree
Stefano Zacchiroli [Thu, 9 Dec 2004 15:18:30 +0000 (15:18 +0000)]
- 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

19 years agosymmetry of equality NOT used in auto
commit | commitdiff | tree
Andrea Asperti [Tue, 7 Dec 2004 08:25:12 +0000 (08:25 +0000)]
symmetry of equality NOT used in auto

19 years agoNew version of auto with "width".
commit | commitdiff | tree
Andrea Asperti [Mon, 6 Dec 2004 12:16:07 +0000 (12:16 +0000)]
New version of auto with "width".

19 years agosnapshot
commit | commitdiff | tree
Stefano Zacchiroli [Fri, 3 Dec 2004 16:30:13 +0000 (16:30 +0000)]
snapshot

19 years agomoogle syntax help page, actually contains only syntax and examples for
commit | commitdiff | tree
Stefano Zacchiroli [Fri, 3 Dec 2004 16:05:27 +0000 (16:05 +0000)]
moogle syntax help page, actually contains only syntax and examples for
the "locate" query. "hint", "match" and "elim" syntaxes are currently
undocumented

19 years agochanged "locate" so that it supports shell-like pattern matching with
commit | commitdiff | tree
Stefano Zacchiroli [Fri, 3 Dec 2004 16:04:01 +0000 (16:04 +0000)]
changed "locate" so that it supports shell-like pattern matching with
'*' and '?' wildcards

19 years agoported to universes
commit | commitdiff | tree
Stefano Zacchiroli [Fri, 3 Dec 2004 15:13:29 +0000 (15:13 +0000)]
ported to universes

19 years ago*** empty log message ***
commit | commitdiff | tree
Stefano Zacchiroli [Thu, 2 Dec 2004 14:55:54 +0000 (14:55 +0000)]
*** empty log message ***

19 years agosync with universes and ~subst (and not ?(subst=[]))
commit | commitdiff | tree
Enrico Tassi [Thu, 2 Dec 2004 13:43:58 +0000 (13:43 +0000)]
sync with universes and ~subst (and not ?(subst=[]))

20 years agoAdded universes handling. Tag PRE_UNIVERSES may help ;)
commit | commitdiff | tree
Enrico Tassi [Wed, 1 Dec 2004 09:43:44 +0000 (09:43 +0000)]
Added universes handling. Tag PRE_UNIVERSES may help ;)

20 years agoAdded universes handling. The PRE_UNIVERSES tag may help ;)
commit | commitdiff | tree
Enrico Tassi [Wed, 1 Dec 2004 09:42:42 +0000 (09:42 +0000)]
Added universes handling. The PRE_UNIVERSES tag may help ;)

20 years agoBug in the management of substitutions into auto corrected.
commit | commitdiff | tree
Andrea Asperti [Tue, 30 Nov 2004 14:55:27 +0000 (14:55 +0000)]
Bug in the management of substitutions into auto corrected.
No significative loss in performance.
Comments commented.

20 years ago- ported tests to newer PP / substitutions
commit | commitdiff | tree
Stefano Zacchiroli [Mon, 29 Nov 2004 12:31:21 +0000 (12:31 +0000)]
- ported tests to newer PP / substitutions

20 years ago- passes subst to FreshNameGenerator
commit | commitdiff | tree
Stefano Zacchiroli [Mon, 29 Nov 2004 12:30:31 +0000 (12:30 +0000)]
- passes subst to FreshNameGenerator
- removed some old debugging prints

20 years agoremoved old debugging prints
commit | commitdiff | tree
Stefano Zacchiroli [Mon, 29 Nov 2004 12:30:09 +0000 (12:30 +0000)]
removed old debugging prints

20 years agopasses ~subst to FreshNameGenerator
commit | commitdiff | tree
Stefano Zacchiroli [Mon, 29 Nov 2004 12:24:47 +0000 (12:24 +0000)]
passes ~subst to FreshNameGenerator

20 years agopasses subst to FreshNameGenerator
commit | commitdiff | tree
Stefano Zacchiroli [Mon, 29 Nov 2004 12:24:25 +0000 (12:24 +0000)]
passes subst to FreshNameGenerator

20 years ago- pass subst to FreshNameGenerator on mk_fresh_name invocations
commit | commitdiff | tree
Stefano Zacchiroli [Mon, 29 Nov 2004 12:24:09 +0000 (12:24 +0000)]
- pass subst to FreshNameGenerator on mk_fresh_name invocations
- removed assert failures on get_cooked_obj (rolled back last commit)
- reindented (the huuuuuuuge) eat_prods function

20 years agobugfix: FreshNameGenerator uses the type checker on mk_fresh_name
commit | commitdiff | tree
Stefano Zacchiroli [Mon, 29 Nov 2004 12:22:23 +0000 (12:22 +0000)]
bugfix: FreshNameGenerator uses the type checker on mk_fresh_name
invocation, thus it should receive in input a subst to be passed to the
type checker in order to avoid "unknown" Metas in the term to be type
checked

20 years agobugfix in type_of_aux' which erroneously discard given substitution
commit | commitdiff | tree
Stefano Zacchiroli [Mon, 29 Nov 2004 12:20:06 +0000 (12:20 +0000)]
bugfix in type_of_aux' which erroneously discard given substitution
(fixes a lot of CicUtil.Meta_not_found spurious exceptions)

20 years agoported to Mysql
commit | commitdiff | tree
Stefano Zacchiroli [Fri, 26 Nov 2004 14:17:15 +0000 (14:17 +0000)]
ported to Mysql

20 years agoported to new xpointer syntax
commit | commitdiff | tree
Stefano Zacchiroli [Fri, 26 Nov 2004 14:17:01 +0000 (14:17 +0000)]
ported to new xpointer syntax

next
Unnamed repository; edit this file 'description' to name the repository.