diff options
| author | sacerdot | 2004-10-06 18:54:05 +0000 |
|---|---|---|
| committer | sacerdot | 2004-10-06 18:54:05 +0000 |
| commit | 9af983945cb1f2b7bcee95cab3ca55927b614b38 (patch) | |
| tree | af62e432788714941ca6eba9a05d851ad4a80422 /tactics/setoid_replace.mli | |
| parent | c29aa4ce8fe8090ca1a84d0be020e40787149c38 (diff) | |
* New syntactic sugar: Add Relation ... transitivity proved by ...
now declares both the relation and the relation as a morphism, computing
the appropriate signature (depending on the reflexivity of the relation).
* New parameter "as ..." to Add Relation (to be able to compute the
morphism name).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6189 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/setoid_replace.mli')
| -rw-r--r-- | tactics/setoid_replace.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/tactics/setoid_replace.mli b/tactics/setoid_replace.mli index 1fa80953c2..0fd0548c29 100644 --- a/tactics/setoid_replace.mli +++ b/tactics/setoid_replace.mli @@ -59,7 +59,8 @@ val general_s_rewrite_in : identifier -> bool -> constr -> new_goals:constr list -> tactic val add_relation : - constr_expr -> constr_expr -> constr_expr option -> constr_expr option -> unit + Names.identifier -> constr_expr -> constr_expr -> constr_expr option -> + constr_expr option -> constr_expr option -> unit val add_setoid : Names.identifier -> constr_expr -> constr_expr -> constr_expr -> unit |