Makefile to extract to ocaml code.

Oops, part of last commit (ocaml extraction implementation)

Ooops, this completes the previous commit (ocaml extraction implementation).

Implementation of Ocaml extraction (largely ported from Coq).
Note: yet to be thoroughly debugged.

In order to use, recompile everything with "OCAML_EXTRACTION=1 ocamlc".

Identity change, improves readability.

- Now the nodes count does not include the generated objects

lambda finaly moved in lib

match now only uses the new move operation

- ng_refiner:
  now the expected type is `XTNone (was None), `XTSome (was Some, also
  was `Term), `XTSort (any sort, was `Sort), `XTInd (any (co)inductive type).
  `XTProd (was `Prod) is used in "try_coercions"
- we replaced some instances of None with `XTSort or `XTInd through the code.
  lib, lambda, and lambdadelta compile,
  in case of errors like "the term ... is not a sort" or
  "the term ... is not a (co)inductive type", revert to `XTNone in the
  corresponding check.
- Now generated objects have the `Generated attribute properly set
- lambda: many "?" removed because of the improvement in the refiner
          other instances of "?" removed for other reasons

Speed-up in match.ma.

Proved old axiom.

Yippeee! Completes proof of soundness of the universal machine
(multi-tape formalization).

unistep!!!

update in basic_2

- notation change for weight functions (following lambda)
  that used to clash with the lref construction
- some parentheses added arround application arguments

funzioni ausiliarie

cfg_in_table_to_tuple

sem_copy_strict

many axioms and daemons removed

quasi finito

well-foundedness done

sem_exec_move completed

almost there

A lot of changes

Splitted unistep_aux
Added another semantics for cfg_to_obj

started unistep

progress in termination

- paths and left residuals: forth case of the equivalence proved!
  The proof is now complete!!

finished semantics for termination of match machine

progress

progress

- paths and left residuals: third case of the equivalence proved!

progress

termination!

Universal machine

Removed all axioms in unistep_aux

removed daemons

universal

tape_move_obj completed (modulo daemons)

cfg_to_obj completed (modulo daemons)

progress

semantics of unistep

- paths and left residuals: second case of the equivalence proved!
- some additions to lstar and Allr

progress in cfg_to_obj

copy char form obj to cfg at the end

high level semantics

high level semantics

semantics of uni_step

progress

progress

progress

progress

progress

Moved a list comparison function in the list file

normal and tuples

- paths and left residuals: first case of the equivalence proved!
- some corrections and additions
- some "?" removed in customized eliminations

added null character to the alphabet

progress

- some additions and renaming ...

progress in unistep_aux

unistep_aux

more unistep

unistep_aux

copy finished

- a few more lemmas ...
- some renaming

copy.ma

match.ma completed

match termination completed, still a small case ignored in wsem_match

wsem_match finished

advancement in match

Closed some daemons

nth_current_chars

standardization: equivalence between paths and left residuals started

match almost finished

more porting to machines that can move without writing

parmove based on end of the tape

porting to machine that can move without writing

dependences update

refactoring ...

Ported permutation.ma and fermat_little_theorem.ma

refactoring

Refactoring

Chebishev ported

lambda: some refactoring + support for subsets of subterms started
core_notation: some "term 19" added
predefined_virtuals: an addition

- probe: new application to compute some data on the proof objects of
a development, such as their net size (aka intrinsinc complexity)
- lambdadelta: Makefile now asks "probe" fore some data

update in basic_2

commit completed! some bugs fixed and some instances of auto resized

xoa: change in naming convenctions for existential quantifies
     to cope with ex2 in lib
lib: some additions
lambdadelta: partial commit in basic_2: just grammar, substitution,
unfold, static

- lambda_delta: programmed renaming to lambdadelta
- nat: general weight-based eliminator added for lambdadelta

- we introduced the pointer_step rc in the perspective of proving
results on head normal forms
- some renaming

some renaming ...

one file was missing .... :(

Many changes

mem/append lemmas

bertrand OK.

- nat.ma: cut removed from f_ind :)
- lanbda: some refactoring

reordering and corrections

bertrand!
-tThis line, and those below, will be ignored--

A    chebyshev/bertrand256.ma
A    chebyshev/bertrand.ma

we simplified our proof of standardization
by removing Kashima's "hap" computation

sqrt.ma