]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: bc2a1fc) | patch
- In the case (?i args) vs term the term is now eta-expanded w.r.t. args.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 18 Jun 2004 11:26:45 +0000 (11:26 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 18 Jun 2004 11:26:45 +0000 (11:26 +0000)
commitfb0f22004d533abca8d157ed89665dbf1041e0e2
treeb8cb66d39207e80754ebb436bfcab71e99019dbatree | snapshot
parentbc2a1fce21a66af077172344854c709b64b7fe82commit | diff
- In the case (?i args) vs term the term is now eta-expanded w.r.t. args.
  This allows to easily implement elim using apply and it makes the auto
  tactic much more powerful.
- CicMetaSubst.apply_subst semantics changed: it now always performs
  beta-reduction when a meta in head-position in an application is istantiated
  with a lambda-abstraction.
- CicMetaSubst.apply_subst_reducing no longer in use: removed.
helm/ocaml/cic_unification/Makefile diff | blob | history
helm/ocaml/cic_unification/cicMetaSubst.ml diff | blob | history
helm/ocaml/cic_unification/cicMetaSubst.mli diff | blob | history
helm/ocaml/cic_unification/cicRefine.mli diff | blob | history
helm/ocaml/cic_unification/cicUnification.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.