]> matita.cs.unibo.it Git - helm.git/history - helm/ocaml/cic_unification/cicMetaSubst.ml
rebuilt
[helm.git] / helm / ocaml / cic_unification / cicMetaSubst.ml
2004-02-06 Stefano Zacchiroliadded annotations to Cic.Implicit
2004-02-06 Claudio Sacerdoti... Comments (notes) removed.
2004-02-06 Claudio Sacerdoti... Code riorganization.
2004-02-06 Stefano Zacchiroliadded Format-library-friendly pretty printers defined...
2004-02-05 Claudio Sacerdoti... Final answer: the local context MUST be normalized...
2004-02-05 Claudio Sacerdoti... Restrict reimplemented to avoid generating lists of...
2004-02-05 Claudio Sacerdoti... Bug fixed: the canonical contexts were traversed in...
2004-02-04 Claudio Sacerdoti... ppcontext (and thus also ppmetasenv) were buggy: the...
2004-02-04 Claudio Sacerdoti... Bug fixed: restriction of already restricted contexts...
2004-02-04 Claudio Sacerdoti... We no longer apply the subst to a Meta in force_does_no...
2004-02-04 Andrea Aspertidelift no longer apply the substitution when a Meta...
2004-02-04 Claudio Sacerdoti... Patch to delift withdrawn.
2004-02-04 Claudio Sacerdoti... Bug fixed: when a variable not instantiated yet was...
2004-02-02 Stefano Zacchiroli- refine's type_of no longer return a substitution
2004-02-02 Stefano Zacchiroli- removed unwind: every substitution is now _not_ unwinded
2004-01-29 Claudio Sacerdoti... - lift added to CicMetaSubst
2004-01-27 Stefano Zacchiroli- occur check test anticipated to the delift phase
2004-01-22 Stefano Zacchiroliadded to CicMetaSubst subst wrapper for CicReduction...
2004-01-22 Stefano Zacchiroliadded CicMetaSubst module for metavariable instantiatiation