]> matita.cs.unibo.it Git - helm.git/commit
huge commit regarding coercions to funclass and eat_prods. before there was a
authorEnrico Tassi <enrico.tassi@inria.fr>
Sat, 8 Sep 2007 23:50:41 +0000 (23:50 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Sat, 8 Sep 2007 23:50:41 +0000 (23:50 +0000)
commit2a79430fa706179258b3a9c5e68e3e268063aa65
tree278875107c976419a692655d6f525b96cd06902d
parent0c0f43954d75c46e9127da72f4d5f27fa9347c51
huge commit regarding coercions to funclass and eat_prods.  before there was a
so broken behaviour that is impossible to describe the changes.

now:
  eat_prods he hety args

  starts checking if hety is metaclosed, if it is does nothing, if not
  unifies it with ?->?-> ... ->? s.t. there is a Pi for every args.
  if this unification fails, does nothing (all coercions are in the
  second phase.

  continues eating prods in hety and args in parallel, if there is an arg
  and no more prods, tries to fix the arity of (he already_processed_args).
  fix_arity gives a range of possible coercions to funclass s.t.
  (c (he ..)) : FunType. The eat prods and args continues, eting the remaining
  args toghether with FunType. If it fails, it continues with another c to
  another FunType. This recursively (yes, it backtracks. no strong opinion
  here, but there is no sane heuristinc to chose one FunType).

  the code is reduced to 1/3, but Localization of errors probably need fixing.
components/cic_unification/cicRefine.ml