Changements d'organisation / modules :
--------------------------------------

  Std, More_util		-> lib/util.ml

  Names				-> kernel/names.ml et kernel/sign.ml
    (les parties noms et signatures ont été séparées)

  Avm,Mavm,Fmavm,Mhm  ->  utiliser plutôt Map (et freeze alors gratuit)
  Mhb                 ->  Bij


Changements dans les types de données :
---------------------------------------
  dans Generic: free_rels : constr -> int Listset.t
                  devient : constr -> Intset.t

  type_judgement ->  typed_type
  environment    ->  context
  context        ->  typed_type signature


ATTENTION:
----------

  Il y a maintenant d'autres exceptions que UserError (TypeError,
  RefinerError, etc.)

  Il ne faut donc plus se contenter (pour rattraper) de faire
  
		try . .. with UserError _ -> ...

  mais écrire à la place
 
                try ... with e when Logic.catchable_exception e -> ...


Changements dans les fonctions :
--------------------------------

	Vectops.
	  it_vect          ->  Array.fold_left
	  vect_it          ->  Array.fold_right
	  exists_vect      ->  Util.array_exists
	  for_all2eq_vect  ->  Util.array_for_all2
	  tabulate_vect    ->  Array.init
	  hd_vect          ->  Util.array_hd
	  tl_vect          ->  Util.array_tl
	  last_vect        ->  Util.array_last
	  it_vect_from     ->  array_fold_left_from
	  vect_it_from     ->  array_fold_right_from
	  app_tl_vect	   ->  array_app_tl
	  cons_vect	   ->  array_cons
	  map_i_vect	   ->  Array.mapi
	  map2_vect	   ->  array_map2
	  list_of_tl_vect  ->  array_list_of_tl

	Std 
	  comp           ->  Util.compose
	  rev_append	 ->  List.rev_append

	Termenv
	  mind_specif_of_mind  -> Global.lookup_mind_specif
                ou Environ.lookup_mind_specif si on a un env sous la main
	  mis_arity      ->  instantiate_arity
	  mis_lc	 ->  instantiate_lc	

	Ex-Environ	 
	  mind_of_path      -> Global.lookup_mind

	Printer
	  gentermpr	->   gen_pr_term

	Typing, Machops
	  type_of_type     ->  judge_of_type
	  fcn_proposition  ->  judge_of_prop_contents

Changements dans les inductifs
------------------------------
Nouveaux types "constructor" et "inductive" dans Term
La plupart des fonctions de typage des inductives prennent maintenant
un inductive au lieu d'un oonstr comme argument. Les seules fonctions
à traduite un constr en inductive sont les find_mrectype and co.

Changements dans les grammaires
-------------------------------

 . le lexer (parsing/lexer.mll) est maintenant un lexer ocamllex

 . attention : LIDENT -> IDENT  (les identificateurs n'ont pas de
                                 casse particulière dans Coq)
		
	
Changements divers
------------------

 . il n'y a plus de script coqtop => coqtop et coqtop.byte sont
   directement le résultat du link du code
   => debuggage et profiling directs

 . il n'y a plus d'installation locale dans bin/$ARCH
 
 . #use "include.ml"  =>  #use "include"
   go()               =>  loop()

 . il y a "make depend" et "make dependcamlp4" car ce dernier prend beaucoup
   de temps