diff options
| author | sacerdot | 2004-10-18 14:53:30 +0000 |
|---|---|---|
| committer | sacerdot | 2004-10-18 14:53:30 +0000 |
| commit | 3c76f306c68a0ea4f02700043c4b4b1be877f4e9 (patch) | |
| tree | 43e14323f2ecf6e0a047f42d25f730fed5444512 /tactics/setoid_replace.mli | |
| parent | 5da0ac62b272c7595da16222e8e9004dc4d459a9 (diff) | |
The "lem" field of a morphism used to be the compatibility proof, but it
became the whole structure of type Morphism_Theory. A new field morphism_theory
has now been added to record both informations. Print Setoids now prints again
the right information.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6235 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/setoid_replace.mli')
| -rw-r--r-- | tactics/setoid_replace.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/tactics/setoid_replace.mli b/tactics/setoid_replace.mli index 917b3e02fb..3469d0cd44 100644 --- a/tactics/setoid_replace.mli +++ b/tactics/setoid_replace.mli @@ -30,6 +30,7 @@ type 'a morphism = { args : (bool option * 'a relation_class) list; output : 'a relation_class; lem : constr; + morphism_theory : constr } type morphism_signature = (bool option * constr_expr) list * constr_expr |