diff options
| author | sacerdot | 2004-10-07 08:38:44 +0000 |
|---|---|---|
| committer | sacerdot | 2004-10-07 08:38:44 +0000 |
| commit | 4e0be2f1b29182ac8b6aed5b5937f500b6f943f2 (patch) | |
| tree | 25acad178a3e25dd0288ce7090856ab2443d98a1 | |
| parent | f553c6d79ce30381d9354f68638be3230dd9e5cb (diff) | |
Now Print Setoids prints also the transitivity justification of transitive
relations.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6191 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | tactics/setoid_replace.ml | 14 |
1 files changed, 8 insertions, 6 deletions
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml index 49d7b9ad6f..e25c261f60 100644 --- a/tactics/setoid_replace.ml +++ b/tactics/setoid_replace.ml @@ -423,9 +423,9 @@ let morphism_table_add (m,c) = ppnl (str "Warning: The morphism " ++ prmorphism m old_morph ++ str " is redeclared. " ++ - str "The new declaration whose compatibility is granted by " ++ + str "The new declaration whose compatibility is proved by " ++ prterm c.lem ++ str " replaces the old declaration whose" ++ - str " compatibility was granted by " ++ + str " compatibility was proved by " ++ prterm old_morph.lem ++ str ".") with Not_found -> morphism_table := Gmap.add m (c::old) !morphism_table @@ -491,21 +491,23 @@ let print_setoids () = (fun k relation -> assert (k=relation.rel_aeq) ; (*CSC: still "Setoid" in the error message *) -(*CSCXX: aggiungere transitivity granted by e ridenominare granted in proved*) ppnl (str"Setoid " ++ prrelation relation ++ str";" ++ (match relation.rel_refl with None -> str "" - | Some t -> str" reflexivity granted by " ++ prterm t) ++ + | Some t -> str" reflexivity proved by " ++ prterm t) ++ (match relation.rel_sym with None -> str "" - | Some t -> str " symmetry granted by " ++ prterm t))) + | Some t -> str " symmetry proved by " ++ prterm t) ++ + (match relation.rel_trans with + None -> str "" + | Some t -> str " transitivity proved by " ++ prterm t))) !relation_table ; Gmap.iter (fun k l -> List.iter (fun ({lem=lem} as mor) -> ppnl (str "Morphism " ++ prmorphism k mor ++ - str ". Compatibility granted by " ++ + str ". Compatibility proved by " ++ prterm lem ++ str ".")) l) !morphism_table ;; |