aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Expand)AuthorAge
* When pretyping [uconstr] closures, don't use the local Ltac variable environm...Gravatar Arnaud Spiwack2014-12-19
* Back to the preferred ?n1:=?n2 order of evar-evar unification which got accid...Gravatar Hugo Herbelin2014-12-19
* Getting rid of Exninfo hacks.Gravatar Pierre-Marie Pédrot2014-12-16
* Fix for #3154: use CUnix.sys_command to call native compiler.Gravatar Maxime Dénès2014-12-16
* Tentatively starting to use heuristics for evar-evar resolution: firstGravatar Hugo Herbelin2014-12-15
* New try on Fixing an evar_map bug revealed by commit 603b66f81 onGravatar Hugo Herbelin2014-12-15
* Documenting check_record + changing a possibly undefined int into int option.Gravatar Hugo Herbelin2014-12-15
* Fix merging of name maps in union of universe contexts.Gravatar Matthieu Sozeau2014-12-14
* Extend the syntax of simpl with a delta flag.Gravatar Arnaud Spiwack2014-12-12
* Two fixes in unification (bugs #3782 and #3709)Gravatar Matthieu Sozeau2014-12-12
* Commit not ready. Sorry.Gravatar Hugo Herbelin2014-12-11
* Added a CannotSolveConstraint unification error and made experimentsGravatar Hugo Herbelin2014-12-11
* Fine-tuning unification error (using OccurCheck in evarconv).Gravatar Hugo Herbelin2014-12-11
* Tentatively more informative report of failure when inferringGravatar Hugo Herbelin2014-12-11
* Fixing an evar_map bug revealed by commit 603b66f81 on unification flags.Gravatar Hugo Herbelin2014-12-11
* Fixing orientation of postponed subtyping problems.Gravatar Hugo Herbelin2014-12-10
* Using a more aggressive test for resolving pattern equations ?n = ?p:Gravatar Hugo Herbelin2014-12-10
* Setup hook to change the unification algorithm used by evarconv,Gravatar Matthieu Sozeau2014-12-09
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-30 06:15:33 +0000