matita.cs.unibo.it Git - helm.git/history - helm/ocaml/cic

]> matita.cs.unibo.it Git - helm.git/history - helm/ocaml/cic_unification/cicMetaSubst.ml

[helm.git] / helm / ocaml / cic_unification / cicMetaSubst.ml

2004-11-12	Stefano Zacchiroli	Fixed an hidden occur check problem: when a Meta is...	blob \| commitdiff \| raw
2004-10-22	Andrea Asperti	- ported to typed explicit substitutions	blob \| commitdiff \| raw \| diff to current
2004-07-20	Andrea Asperti	Subst has been added to the kernel.	blob \| commitdiff \| raw \| diff to current
2004-07-05	Stefano Zacchiroli	commeted out some debugging instructions	blob \| commitdiff \| raw \| diff to current
2004-07-01	Stefano Zacchiroli	New handling of substitution:	blob \| commitdiff \| raw \| diff to current
2004-06-28	Andrea Asperti	- new implementation of the apply case in fo_unif using...	blob \| commitdiff \| raw \| diff to current
2004-06-18	Claudio Sacerdoti...	- In the case (?i args) vs term the term is now eta...	blob \| commitdiff \| raw \| diff to current
2004-03-05	Claudio Sacerdoti...	Debugging message removed.	blob \| commitdiff \| raw \| diff to current
2004-03-05	Claudio Sacerdoti...	apply_subst did not apply the substitution to the expli...	blob \| commitdiff \| raw \| diff to current
2004-03-05	Claudio Sacerdoti...	List.nth not guarded by try ... with. Fixed.	blob \| commitdiff \| raw \| diff to current
2004-03-02	Claudio Sacerdoti...	- Improved error messaging.	blob \| commitdiff \| raw \| diff to current
2004-02-11	Stefano Zacchiroli	use debug_print in a debugging message	blob \| commitdiff \| raw \| diff to current
2004-02-11	Claudio Sacerdoti...	Big changes:	blob \| commitdiff \| raw \| diff to current
2004-02-06	Stefano Zacchiroli	added annotations to Cic.Implicit	blob \| commitdiff \| raw \| diff to current
2004-02-06	Claudio Sacerdoti...	Comments (notes) removed.	blob \| commitdiff \| raw \| diff to current
2004-02-06	Claudio Sacerdoti...	Code riorganization.	blob \| commitdiff \| raw \| diff to current
2004-02-06	Stefano Zacchiroli	added Format-library-friendly pretty printers defined...	blob \| commitdiff \| raw \| diff to current
2004-02-05	Claudio Sacerdoti...	Final answer: the local context MUST be normalized...	blob \| commitdiff \| raw \| diff to current
2004-02-05	Claudio Sacerdoti...	Restrict reimplemented to avoid generating lists of...	blob \| commitdiff \| raw \| diff to current
2004-02-05	Claudio Sacerdoti...	Bug fixed: the canonical contexts were traversed in...	blob \| commitdiff \| raw \| diff to current
2004-02-04	Claudio Sacerdoti...	ppcontext (and thus also ppmetasenv) were buggy: the...	blob \| commitdiff \| raw \| diff to current
2004-02-04	Claudio Sacerdoti...	Bug fixed: restriction of already restricted contexts...	blob \| commitdiff \| raw \| diff to current
2004-02-04	Claudio Sacerdoti...	We no longer apply the subst to a Meta in force_does_no...	blob \| commitdiff \| raw \| diff to current
2004-02-04	Andrea Asperti	delift no longer apply the substitution when a Meta...	blob \| commitdiff \| raw \| diff to current
2004-02-04	Claudio Sacerdoti...	Patch to delift withdrawn.	blob \| commitdiff \| raw \| diff to current
2004-02-04	Claudio Sacerdoti...	Bug fixed: when a variable not instantiated yet was...	blob \| commitdiff \| raw \| diff to current
2004-02-02	Stefano Zacchiroli	- refine's type_of no longer return a substitution	blob \| commitdiff \| raw \| diff to current
2004-02-02	Stefano Zacchiroli	- removed unwind: every substitution is now _not_ unwinded	blob \| commitdiff \| raw \| diff to current
2004-01-29	Claudio Sacerdoti...	- lift added to CicMetaSubst	blob \| commitdiff \| raw \| diff to current
2004-01-27	Stefano Zacchiroli	- occur check test anticipated to the delift phase	blob \| commitdiff \| raw \| diff to current
2004-01-22	Stefano Zacchiroli	added to CicMetaSubst subst wrapper for CicReduction...	blob \| commitdiff \| raw \| diff to current
2004-01-22	Stefano Zacchiroli	added CicMetaSubst module for metavariable instantiatiation	blob \| commitdiff \| raw \| diff to current

Unnamed repository; edit this file 'description' to name the repository.

RSS Atom