Updating.

A slightly more complicated example.

Finished!

We are still equivalent (even if the definition of ncover is obfuscated).

Urrah!

Extending to the nAx set.

Skipfact function (a partial general recursive function) defined by recursion
over the cover relation of an IGFT.

Fixed a bug in the discrimination principle: the refiner was not able to
synthesize the return type of the inner match correctly.

Finished

1. New paramodulation function
2. goal narrowing works both on the current goal both before and after
demodulation

saturate cust be called with delta=0

Added is_equation

Debugging info

Improved

Partial porting to new syntax.

Source language path must be appended, not replaced.

Categorical stuff postponed.

The body of constants is a reference, not the actual body!

removed debugging info

rebuilding the library

rebuilding the library

rebuilding the library

applyS

refresh uri
applyS

Support for the new auto tactics //

Support for the new // tactics.

new reloc_subst (to avoid cyclic substitutions).
Changed default sig.

....

...

...

Simplified.

Note: it breaks the file later (maybe a coercion conflict, I suppose).

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