diff options
| author |  sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-05-19 14:15:57 +0000 |
|---|---|---|
| committer | sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-05-19 14:15:57 +0000 |
| commit | 67bae3dcedbfe1c7ab4377fc4623b337fe4277b6 (patch) | |
| tree | aaf66aa933684bb13d121b0555563ab9ec6a987c | |
| parent | d55637238606e1f3eba48219266782d691e021ad (diff) | |
Setoid_replace: improved error message when trying to replace a term in a
non-applicative context.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7040 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | tactics/setoid_replace.ml | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml index 11e1545a5..c304afda9 100644 --- a/tactics/setoid_replace.ml +++ b/tactics/setoid_replace.ml @@ -1503,7 +1503,13 @@ let mark_occur gl ~new_goals t in_c input_relation input_direction = aux output_relation output_direction (mkApp ((Lazy.force coq_impl), [| c1 ; subst1 (mkRel 1 (*dummy*)) c2 |])) - | _ -> [ToKeep (in_c,output_relation,output_direction)] + | _ -> + if occur_term t in_c then + errorlabstrm "Setoid_replace" + (str "Trying to replace " ++ prterm t ++ str " in " ++ prterm in_c ++ + str " that is not an applicative context.") + else + [ToKeep (in_c,output_relation,output_direction)] in let aux2 output_relation output_direction = List.map |