diff options
| author |  sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-09-29 15:34:32 +0000 |
|---|---|---|
| committer | sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-09-29 15:34:32 +0000 |
| commit | 79c4772c5bd10cc023f86cd63a1e69a5ac459c5c (patch) | |
| tree | 5f6fe3c3d58652aeadd8de8a2080fc5eec8db25a | |
| parent | eff11708c082738bd8856ded63d63cac82fc7bb9 (diff) | |
Add Relation is now able to detect non well typed relation registrations.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6159 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | tactics/setoid_replace.ml | 13 |
1 files changed, 12 insertions, 1 deletions
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml index 33143b1dc..1ecb865ff 100644 --- a/tactics/setoid_replace.ml +++ b/tactics/setoid_replace.ml @@ -107,6 +107,8 @@ let coq_reflexive = lazy(gen_constant ["Relations"; "Relation_Definitions"] "reflexive") let coq_symmetric = lazy(gen_constant ["Relations"; "Relation_Definitions"] "symmetric") +let coq_relation = + lazy(gen_constant ["Relations"; "Relation_Definitions"] "relation") let coq_Relation_Class = lazy(constant ["Setoid"] "Relation_Class") let coq_Argument_Class = lazy(constant ["Setoid"] "Argument_Class") @@ -467,6 +469,15 @@ let print_setoids () = (************************** Adding a relation to the database *********************) +let check_eq env a aeq = + let typ = mkApp (Lazy.force coq_relation, [| a |]) in + if + not + (is_conv env Evd.empty (Typing.type_of env Evd.empty aeq) typ) + then + errorlabstrm "Add Relation Class" + (prterm aeq ++ str " should have type (" ++ prterm typ ++ str ")") + let check_refl env a aeq refl = if not @@ -475,7 +486,6 @@ let check_refl env a aeq refl = then errorlabstrm "Add Relation Class" (str "Not a valid proof of reflexivity") - else () let check_sym env a aeq sym = if @@ -488,6 +498,7 @@ let check_sym env a aeq sym = let int_add_relation a aeq refl sym = let env = Global.env () in + check_eq env a aeq ; option_iter (check_refl env a aeq) refl ; option_iter (check_sym env a aeq) sym ; Lib.add_anonymous_leaf |