The proposed architecture is as follows:

- Decl provides the type of declaration, decl, which is a sum
  of type_decl, logic_decl, ind_decl, and prop_decl. decl is 
  h-consed and does not depent on theory, context or anything else.

- Theory provides the types of theories and theories under construction.
  A theory is a list of (decl | use | clone) with namespace, and the set
  of known idents. Theories are not h-consed and they do not depend on
  env or task.

- Task provides the types of environment (env), clone maps (clone), and
  the task itself. It might be interesting to merge Transform with Task.
  An environment stays as it is today. A clone map is a private record 
  with the unique tag and physical equality. A task is essentially what
  context is today:
    
    task_decl  : decl               (* top declaration *)
    task_prev  : task option        (* the previous context *)
    task_known : (ident, decl) map  (* the set of known symbols *)
    task_clone : clone              (* the clone map *)
    task_env   : env                (* the environment *)
    task_tag   : int                (* the unique tag *)

  Tasks are h-consed. There is a guarantee that task_env and task_clone
  of task and task.task_prev are physically equal.

  Unless there is a good reason to do otherwise, the only way to produce
  a task is by split_goal, which takes a theory (and optionally a number
  of goals in it) and creates a list of tasks. Note that sharing IS LOST
  whenever two goals are separated by a clone instruction. However, the
  declarations will still be shared.

- Trasformation works on tasks, producing task lists, tasks, and alphas.

- use_export and clone_export may be allowed on tasks, rebuilding the
  whole task, whenever necessary.

This commit just adds the Decl module, but does not make anything use it.