Coercions via unification hints?

- we now add the kernel options in the preamble of the URI hierarchy
- we now quote the identifiers by default to make them NMTOKENS but we added a command line option to disable this quoting (it can be time consuming)

1) stuff moved from categories.ma to setoids*.ma
2) we are now ready to define the category of o-algebras

...

Almost done (up to definition of category).

Porting of Sambin's stuff started.
Everything is now automatically enriched using hints.
It seems to work quite smoothly.

Porting of Sambin's stuff started.

Removed line is back again.

...

Refining with no expected type + unification seems to be faster.

Trying to be faster

Trying to be faster.

Final subst returned by superposition and passed around.

using = instead of alpha conversions. context metasenv and subst are not
needed any more

eq_coerc for smart application.

the sort hierarchy parameter enter the kernel status

Minor bag fixed, relative to failures.

A compiling version?

Added a "sort_metasenv" function.

Commented a couple of calls to "set_reference_of_oxuri".

Added the paramodulation stuff to the status

param "slir" to call the new auto
and "fast paramod" for the constrained narrowing of the goal

Added the paramodulation active/passive tables to the state

Attached fast_eq_check to auto

Added nnAuto.mli

Debug set to ()

Clean up of debgging info

Syntax error

Wrong reference corrected

Minor fixing for last chance

Added a fol operation

Bugfix in inversion (was using refl_eq instead of refl).

Indexing local context for paramod.

Propositional equality

The new paramodulation functions instantiated over nCic.

New ways for initialising the signature required for paramodultion

Passive equations have their own index (not passive goals).
New, simple version of "last chance" (yet to be improved).
Added a narrowing function the merely works on goals, in parallel.

debug takes lazy strings. Moved here the are_alpha_eq test.

Added a function remove_unit_clause

Added a boolean test function to discriminate equations from predicates

Generalized intitialization for EqP

Generalized initialization of eqP.

porting to lablgtk2 >= 2.14 and releasing

...

ndestruct now clears off identity equations whenever it's possible.

Fixed inversion, which was broken by the last changes in the refiner.

Exported forward_inference_step

Bugfix in tipify: a metavariable was set to type without sortifying its type.

In order to prevent useless meta extensions, we optimize the unification of one
type and one unrefined term (currently happening only in the Lambda case).

When unifying

  ?1[a,b] == ?2[a,b,c]

it is not the same to instantiate ?1 or ?2: instantiating ?2 may drop the
dependency over c, while instatianting ?1 does no harm. This patch always
instantiates the meta whose canonical context is a prefix, or the newest one if
the two canonical contexts are the same.

Removed dead code

Subsumption and reduction

- Added a swap parameter to the unification procedure
- Fixed a bug in the metavariable restriction algorithm, which resulted in bad
  metavariable local contexts.

NCicRefiner.force_to_sort implemented on top of NCicUnification.sortfy.

Code factorization for check_type.

ndestruct tactic: mainly bugfixes; the algorithm isn't clean yet, outputting a
number of unnecessary equations which must be cleared; it seems to work
reasonably nonetheless.

Closing the goal.

Implementation of ndestruct tactic (including destruction of constructor forms
in the dependently typed case; not including discrimination of cycles).

Exported apply_subst_context

Added the new auto version (not attached yet).

some interfaces improved

Code made more uniform.

Union find slightly more general (f can now point to external elements)

A case was missing

brg: change in the representation of binders
     local environment pretty printing disabled (needs a fix)

Naif version of the union find

Bug fixed: restrict used to take the list of positions to be restricted, but
it did not return the (potentially bigger) set of actually restricted positions.
Thus, it was possible to create a local context longer then the canonical one.

1) sort computation undone (it used to be bugged anyway)
2) let's unfocus again (even if it is not always correct)

basic_rg: reduction was not tail recursive by mistake

Code simplified.

Useless old code for ad-hoc management of out-scope removed.

New style debugging/profiling for NCicMetaSubst.

Sometimes it is useful to be able to print the subst without applying it.

auto snapshot

- dual_rg: renamed to complete_rg [as suggested in the ToCL documentation]
- Makefile: "lddl" entry generates lddl.tar.bz2

refactoring ...

new xml exportation procedure for basic_rg (10 times faster than previous). the static html pages were changed accordingly. Old exportation procedure removed

Better error message.

For some obscure reason, more universes are now needed (but not used in
scripts). To be better understood.

instantiate/sortfy/kindfy etc. reimplemented with less and more correct code

New function.

Let's use already existent functions.

- lambda-delta: some fixes: now the grundlagen type-checkes through dual_rg
- matita/Makefile: we removed LAMBDA-TYPES from the nightly tests (too slow ???)

Works again

Ad-hoc management of ? vs out_scope in instantiate. The library passes again,
but there seems to be still more work to do in instantiate.

Bug fixed: the `IsTerm attribute is now added by mk_meta and it was not
preserved. The current code should be more stable.

1) new-style debugging/profiling code for old reduction
2) aliases are now dumped to stderr

Commented out code to optimize the case t1 vs t2 when t1 and t2 are both
meta closed. Why is it necessary, anyway?

One-shot aliases were no longer generated because of a bug (i.e. all aliases
retrieved from the universe used to have instance=0). Fixed by parameterizing
once again all the functions with a ~fix_instance function to fix the instance.

Different aliases, better equality inferred.

instances

instance fixed

better indentation

better indentation

better comments and indentation

use prop_only to filter instead of repeting the same function body

better logging

better logging and immediate pruning of new goals when
- length(goals) > maxwidth
- depth = maxdepth and goals <> []

auto navigates a real tree, not a flattened one

labels in group_by_tac