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.024Jan23222120191816131211107331Dec30292322212019181514131211108765432130Nov292827262423222120181615141312119876543231Oct302928272625242019181210975429Sep282726252421201918171598628Aug262423222017CHANGELOG 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.BiIndexBottom class for bottom element in a bi index. monPred_all is a monoid morphism, and related big op lemmas.Reorganize bi.monpred. Add unfolding manual lemmas for monPred_at, and use them in proofmode.monpred. Add big op lemmas for monpred_at.Merge branch 'jh/generic_updates' into 'gen_proofmode'Add instances for eliminating modalities under monPred_at or an embedding.FUpdFacts and BUpdFacts instances for monPred.Add BUpdFacts and FUpdFacts.Merge branch 'master' into gen_proofmodeAddModal: fix priorities.Merge branch 'master' into gen_proofmodeAddModal instances for except0 and later, to recover the old behaviorMerge branch 'master' into gen_proofmodeMerge branch 'robbert/add_modal' into 'master'Special proof mode class for adding a modality to a goal.Fix wrong name.