Commits : Listings

  Analyzed 1 day ago based on code collected 1 day ago.
Showing page 1 of 690
Commit Message Contributor Files Modified Lines Added Lines Removed Code Location Date
Exporting field f_debug (needed for Ssreflect). Anon32 More... 4 days ago
Using an "extra" Store.t field in interp_sign instead of dedicated record fields. Anon32 More... 4 days ago
When doing setoid_rewrite through rewrite, do resolution of classes in w_unify_to_subterm, deactivated by previous patch (fixes RelationAlgebra). Anon32 More... 4 days ago
Normalizing exception raised by tactic coercions. Anon32 More... 5 days ago
Moving coercion functions out of Tacinterp. Anon32 More... 6 days ago
Totally replaced ad-hoc tactic values by generic arguments. Now only tactics results are special tactic values represented by the non-exported tacvalue type. Anon32 More... 6 days ago
Added Genarg as generic argument type. Anon32 More... 6 days ago
Changing the type of Ltac values. Now they are toplevel generic arguments. That way we will be able to define interpretation of tactics without referring to tactic values. Anon32 More... 6 days ago
Fixing a Not_found and evar not found anomaly found in ATBR, related to setoid_rewrite t where t containts evars, to be added to the goal evars. Anon32 More... 6 days ago
One more fix for rewrite: disallow resolving of the (partial) constraints happening silently in w_unify and handle this explicitely. Class resolution filters now can test the existential key. Fixes Ergo contrib. Anon32 More... 6 days ago
Hiding tactic value representations. Anon32 More... 8 days ago
Fix [setoid_rewrite] forgetting some evars that are produced when typechecking a lemma to apply, fixes test-suite test. Anon32 More... 8 days ago
Cleanup in rewrite.ml4, remove Evd.merge... replaced by an evars_reset_evd (to push the metas from a clenv into the current evars). Anon32 More... 11 days ago
Fixing bug #3030. Anon32 More... 12 days ago
Fixing #3056 Anon32 More... 12 days ago
More comments in Genarg. Anon32 More... 12 days ago
Uniformizing generic argument types. Anon32 More... 12 days ago
Document changes and add missing documentation for Program options. Anon32 More... 12 days ago
Add an option to shrink the context of program obligations to avoid unnecessary dependencies (applies to obligations defined by tactics only). Satisfies RFE #1984. Anon32 More... 12 days ago
Replacing lists by maps in matching interpretation. Anon32 More... 13 days ago
 
 
 

Creative Commons License Copyright © 2013 Black Duck Software, Inc. and its contributors, Some Rights Reserved. Unless otherwise marked, this work is licensed under a Creative Commons Attribution 3.0 Unported License . Ohloh ® and the Ohloh logo are trademarks of Black Duck Software, Inc. in the United States and/or other jurisdictions. All other trademarks are the property of their respective holders.