{"push_id":2447152836,"size":1,"distinct_size":1,"ref":"refs/heads/evar+strict_to_constr","head":"6d939ffcb500588ef3c19030ebd9a9516569a71c","before":"6b1b78791be313ab3be623adef2755644b31d6e5","commits":[{"sha":"6d939ffcb500588ef3c19030ebd9a9516569a71c","author":{"name":"Emilio Jesus Gallego Arias","email":"74bd03b9fa5ba9425c7ecadbbbb4d58aa6999825@x80.org"},"message":"[econstr] Forbid calling `to_constr` in open terms.\n\nWe forbid calling `EConstr.to_constr` on terms that are not evar-free,\nas to progress towards enforcing the invariant that `Constr.t` is\nevar-free. [c.f. #6308]\n\nDue to compatibility constraints we provide an optional parameter to\n`to_constr`, `abort` which can be used to overcome this restriction\nuntil we fix all parts of the code.\n\nNow, grepping for `~abort:false` should return the questionable\nparts of the system.\n\nNot a lot of places had to be fixed, some comments:\n\n- problems with the interface due to `Evd/Constr` [`Evd.define` being\n  the prime example] do seem real!\n- inductives also look bad with regards to `Constr/EConstr`.\n- code in plugins needs work.\n\nA notable user of this \"feature\" is `Obligations/Program` that seem to\nlike to generate kernel-level entries with free evars, then to scan\nthem and workaround this problem by generating constants.","distinct":true,"url":"https://api.github.com/repos/ejgallego/coq/commits/6d939ffcb500588ef3c19030ebd9a9516569a71c"}]}
{"actor":{"display_login":"ejgallego"}}