diff options
| author |  mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-12-12 14:39:05 +0000 |
|---|---|---|
| committer | mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-12-12 14:39:05 +0000 |
| commit | 18ff5c1f279194fd55033744b733a32291d0bba9 (patch) | |
| tree | de4f240f9e6e3a658420fb5577d07e73ee0f0779 /tactics | |
| parent | 165550bc635b930721a3b3233059a96dbb4c35f5 (diff) | |
Reparation Intro sans nom qui ne reduisait pas le but quand celui-ci
n'etait pas un produit
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1085 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tactics.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index b54fd0a63..158a625e6 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -265,7 +265,7 @@ let default_id gl = | IsSort (Type _) -> (id_of_name_with_default "X" name) | _ -> anomaly "Wrong sort") | IsLetIn (name,b,_,_) -> id_of_name_using_hdchar (pf_env gl) b name - | _ -> error "Introduction needs a product" + | _ -> raise (RefinerError IntroNeedsProduct) (* Non primitive introduction tactics are treated by central_intro There is possibly renaming, with possibly names to avoid and |