GitLab

like f_map_sign should only be applied from specialized
recursive functions and these funcitons will usually supply
the polarity argument.

It's not more expressive but much nicer than epsilon.

  as it is most often ignored
- check for empty map in t_subst/f_subst
- bugfix: don't forget nested match statements in Decl and Compile_match

- check pattern well-formedness in Pattern
- add arguments to exceptions in Ty and Term

(unusable so far, must eliminate match statements, too)

   - Util : Ajout de Creation generique de Set,Map et Hashtbl 
            quand on a un tag et une egalitée physique
   - Hashweak : Implementation de l'idee de Jean-Christophe et Andreï
   - Register : Simplification des types comme demandé par Jean-Christophe
                Mise à jour des fichiers qui en dépendait
   - Theory   : Ajout d'une facilité de création des th_inst
   - Encoding_decorate : Prelude pour l'encodage de Stéphane en utilisant flat_theory d'Andreï
   - Ty : Ajout de Sty, Mty et Hty
   - Main : Reduction de la taille des lignes à 80 colonnes

- unify Lfunction and Lpredicate (mucho bettar)
- separation of prop and fmla
- making prop and tvsymbol private aliases of ident

to build an ill-typed formula. Unsafe functions are actually unsafe.

This is less dangerous than I previously thought,
because we still can never create an ill-typed term,
nor we can push a term with an unprotected de Bruijn
index into a context. Salut, François ;)

- preserve labels on t_map/f_map/...
- comment out t_map_trans/f_map_trans
- rename X_forall/X_exists to X_all/X_any
- rename X_map_open/X_fold_open to X_map/X_fold

also, rewrite application of "<>" into "not ( = )"

- prevent leak of idents by separating them into two types:
  - "preid" -- user-created and non-unique
  - "ident" -- unique, generated from "preid" by various
               smart constructors: create_tysymbol, etc

  This guarantees that two different symbols never share
  an ident.

- no need to hashcons tysymbols, fsymbols, and psymbols,
  as they are unique by construction

- make separate hashconsing smart constructors for decl

- export namespace as a private record (no reason to not to)

- some code rearrangement in hashconsing of decls

- fix namespace merging in close_namespace

- namespace name can be just a string, no need to use ident