aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Expand)AuthorAge
* Switch the few remaining iso-latin-1 files to utf8Gravatar Pierre Letouzey2014-12-09
* Fixing wrong evar_map in return clause inference, revealed by 48509b611.Gravatar Hugo Herbelin2014-12-08
* Improved criterion for evar restriction in the configurationGravatar Hugo Herbelin2014-12-08
* Improving evar restriction (this is a risky change, as I remember aGravatar Hugo Herbelin2014-12-07
* Improved tracking of the origin of evars.Gravatar Hugo Herbelin2014-12-07
* Had forgotten some debugging printer.Gravatar Hugo Herbelin2014-12-07
* More consistent printing of evars in evar_map debugging printer.Gravatar Hugo Herbelin2014-12-05
* Fix debugger Tactic Unification.Gravatar Hugo Herbelin2014-12-05
* Small cleaning and uniformization in unification flags:Gravatar Hugo Herbelin2014-12-05
* New approach to deal with evar-evar unification problems in differentGravatar Hugo Herbelin2014-12-04
* Occur-check in refine.Gravatar Arnaud Spiwack2014-12-04
* Reactivating option "Set Printing Existential Instances" for asking printing ...Gravatar Hugo Herbelin2014-12-04
* In solve_evar_evar, orient the heuristic over arities with differentGravatar Hugo Herbelin2014-12-03
* When solving ?id{args} = ?id'{args'}, give preference to ?id:=?id' ifGravatar Hugo Herbelin2014-12-02
* Postponing the "evar <= evar" problems instead of solving them in anGravatar Hugo Herbelin2014-12-02
* Being more scrupulous on preserving subtyping in evar-evar problems.Gravatar Hugo Herbelin2014-12-02
* Being consistent in making arbitrary choices in recursive calls toGravatar Hugo Herbelin2014-12-02
* Resolution of evar/evar problems: removed a test which should beGravatar Hugo Herbelin2014-12-02
* Reverting the following block of three commits:Gravatar Hugo Herbelin2014-11-27
* Fixing Coq compilation.Gravatar Pierre-Marie Pédrot2014-11-26
* Experimenting always forcing convertibility on strict implicit argumentsGravatar Hugo Herbelin2014-11-26
* A bit more information in debug tactic unification.Gravatar Hugo Herbelin2014-11-25
* Experimenting using unification when matching evar/meta free subtermsGravatar Hugo Herbelin2014-11-25
* Fix #3824. de Bruijn error in normalization of fixpoints.Gravatar Maxime Dénès2014-11-23
* Avoid compilation warning.Gravatar Matthieu Sozeau2014-11-21
* Probably useless use of a global-environment reading function in Indrec.Gravatar Pierre-Marie Pédrot2014-11-20
* Making map_union a standard function of the ML library.Gravatar Hugo Herbelin2014-11-19
* Option -type-in-type continued (deactivate test for inferred sort ofGravatar Hugo Herbelin2014-11-19
* Continuing fixing nested but convertible occurrences in find_subtermGravatar Hugo Herbelin2014-11-19
* Printing function for [uconstr].Gravatar Arnaud Spiwack2014-11-19
* uconstr: fix bug in interpretation of Ltac-bound name in let-tuple and patter...Gravatar Arnaud Spiwack2014-11-19
* Glob-ops: a name-mapping operation for pattern-matching binders.Gravatar Arnaud Spiwack2014-11-19
* Fixing a little bug with nested but convertible occurrences in "destruct at".Gravatar Hugo Herbelin2014-11-18
* Fixing detection of occurrences in the presence of nested subterms forGravatar Hugo Herbelin2014-11-18
* Enforcing a stronger difference between the two syntaxes "simplGravatar Hugo Herbelin2014-11-16
* Get rif of exit codes 120, 121, 123, and 124.Gravatar Xavier Clerc2014-11-14
* Accepting conversion on inner closed subterms while looking forGravatar Hugo Herbelin2014-11-11
* Evar normalization is now done eagerly.Gravatar Pierre-Marie Pédrot2014-11-10
* Fixing bug #3792.Gravatar Pierre-Marie Pédrot2014-11-09
* new: Optimize Proof, Optimize HeapGravatar Enrico Tassi2014-11-09
* Follow up to experimental eager evar unification in bcba6d1bc9:Gravatar Hugo Herbelin2014-11-08
* Fixing a bug in change of subst_defined_metas in bcba6d1bc9f769da:Gravatar Hugo Herbelin2014-11-08
* Experimentally applying eager evar substitution at the same time asGravatar Hugo Herbelin2014-11-04
* Fixing confused code for interpretations of evar instances.Gravatar Hugo Herbelin2014-11-03
* Fixing inefficiency in typeclass resolution.Gravatar Pierre-Marie Pédrot2014-11-03
* Fixing subterm matched for destruct when it is matched from prefix.Gravatar Hugo Herbelin2014-11-02
* Cosmetic changes.Gravatar Hugo Herbelin2014-11-02
* Fixing 1177da327 (reorganization of the test for generic selection ofGravatar Hugo Herbelin2014-11-02
* Reorganization of the test for generic selection of occurrences inGravatar Hugo Herbelin2014-10-31
* Enlarge the cases where the like first selection is used in destruct.Gravatar Hugo Herbelin2014-10-31
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 09:54:25 +0000