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 /Makefile.common | |
| 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 'Makefile.common')
| -rw-r--r-- | Makefile.common | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/Makefile.common b/Makefile.common index 0e6c3925c..4a60b251a 100644 --- a/Makefile.common +++ b/Makefile.common @@ -708,8 +708,8 @@ SETOIDSVO:= theories/Setoids/Setoid_tac.vo theories/Setoids/Setoid_Prop.vo theor UNICODEVO:= theories/Unicode/Utf8.vo -CLASSESVO:= theories/Classes/Init.vo theories/Classes/SetoidClass.vo theories/Classes/SetoidTactics.vo \ - theories/Classes/SetoidDec.vo +CLASSESVO:= theories/Classes/Init.vo theories/Classes/Relations.vo theories/Classes/SetoidClass.vo \ + theories/Classes/SetoidTactics.vo theories/Classes/SetoidDec.vo THEORIESVO:=\ $(INITVO) $(LOGICVO) $(ARITHVO) $(BOOLVO) $(NARITHVO) $(ZARITHVO) \ @@ -766,7 +766,7 @@ DPVO:=contrib/dp/Dp.vo SUBTACVO:=theories/Program/Tactics.vo theories/Program/Equality.vo theories/Program/Subset.vo \ theories/Program/Utils.vo theories/Program/Wf.vo theories/Program/Program.vo \ - theories/Program/FunctionalExtensionality.vo + theories/Program/FunctionalExtensionality.vo theories/Program/Basics.vo RTAUTOVO:= \ contrib/rtauto/Bintree.vo contrib/rtauto/Rtauto.vo |