diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-02-03 00:42:23 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-02-03 00:42:23 +0000 |
| commit | 36fa70885150234159b0a6d8a1deb2d9fb3d2b8a (patch) | |
| tree | a16ec5f253ee4fbc529c59e22abab2a46d8c28ab /theories/Program/Program.v | |
| parent | c3f187d2eee5a99bf1a903059a3f18ff77560c98 (diff) | |
Add new files theories/Program/Basics.v and theories/Classes/Relations.v
for basic functional programming and relation
definitions respectively.
Classes.Relations also includes the definition of Morphism
and instances for the standard morphisms and relations (eq, iff, impl,
inverse and complement). The class_setoid.ml4 [setoid_rewrite] tactic
has been reimplemented on top of these definitions, hence it doesn't
require a setoid implementation anymore. It also generates obligations
for missing reflexivity proofs, like the current setoid_rewrite. It has
not been tested on large examples but it should handle directions and
occurences. Works with in if no obligations are generated at this time.
What's missing is being able to rewrite by a lemma instead of a simple
hypothesis with no premises.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10502 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Program/Program.v')
| -rw-r--r-- | theories/Program/Program.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/theories/Program/Program.v b/theories/Program/Program.v index fb172db84..4d92be3c5 100644 --- a/theories/Program/Program.v +++ b/theories/Program/Program.v @@ -2,3 +2,4 @@ Require Export Coq.Program.Utils. Require Export Coq.Program.Wf. Require Export Coq.Program.Equality. Require Export Coq.Program.Subset. +Require Export Coq.Program.Basics.
\ No newline at end of file |