search

mit-plv / fiat

Mostly Automated Synthesis of Correct-by-Construction Programs
http://plv.csail.mit.edu/fiat/
Other
147 stars 31 forks source link

overlay for coq/coq#12162 #38

Closed olaure01 closed 4 years ago

olaure01 commented 4 years ago

The PR coq/coq#12162 renames Bool.leb into Bool.le which is more coherent with the rest of the standard library since it has type bool -> bool -> Prop. This generates possible clashes with Nat.le or Peano.le so that additional qualification is required.