Skip to content
Snippets Groups Projects
Select Git revision
  • master default protected
1 result
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.029Jan27252423222120191816131211107331Dec30292322212019181514131211108765432130Nov292827262423222120181615141312119876543231Oct302928272625242019181210975429Sep282726252421201918171598628Aug262423update emacs snippetSupport framing pure facts and equalities under an embedding.Add test.Make it possible to introduce an hypothesis which is behind an embedding.Define monPred_ex and monPred_all in terms of the embedding, for better support in the proof mode.Make iStartProof convert Coq universals into bi universals.Make sure all the itactics fail if the do not go through the proof mode.Move the AsValid typeclass in classes.v and class_instances.vdocument editor configuration for unicode input/outputMerge branch 'robbert/invariant_weaken' into 'master'Show that non-atomic invariants are closed under logical equivalence.Make invariants closed under logical equivalence.Merge branch 'robbert/wp_value_inv' into 'master'Merge branch 'robbert/iEval' into 'master'CHANGELOG for total WPMake `iEval` more robust by using a let binding internally.Add comment about `iSsrRewrite`.Documentation.Use `iEval ... in ...` somewhere.Version of `iEval ... in ...`.Make `iEval` fail in case it is not a proof mode goal.Use entailment in `iEval` so that setoid rewriting works.actually no need to set COQBIN default, it turns outquery COQBIN like coq_makefile doeshonor COQBINImprove iStartProof.MakeMorphism -> MakeEmbed.Fix error message.Make AsValid TC search not loop when there is no instance to be found.Update comment.Merge branch 'master' into gen_proofmodeFix priorities of IntoLaterN instances.Test cases for issue #141.Fix issue #141.Fix some comments.Consistently name `wp_value_inv`.Update Coq bug in comment.update .gitignoreMerge branch 'total_weakestpre'The types of propositions for monPred lemma need to be [monPred I PROP] and not [bi_car (monPredI I PROP)], otherwise iIntoValid fails in a very weird way. Seems to be related to a Coq bug.