diff options
| author | herbelin | 2002-12-21 11:51:33 +0000 |
|---|---|---|
| committer | herbelin | 2002-12-21 11:51:33 +0000 |
| commit | 0dece739c580b39d77708bb8117442e7e1cd560b (patch) | |
| tree | 3db834fd12224590c4feddd213a41a0edd7c4986 /tactics/tacinterp.ml | |
| parent | 094b40758cb4278b33a87e5633cf4ac716f348b4 (diff) | |
Légère amélioration des messages d'erreur des with-bindings et des Rewrite
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3474 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/tacinterp.ml')
| -rw-r--r-- | tactics/tacinterp.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 05b26cbb64..64bf9371fd 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -353,8 +353,8 @@ let glob_constr ist c = in c (* Globalize bindings *) -let glob_binding ist (b,c) = - (glob_quantified_hypothesis ist b,glob_constr ist c) +let glob_binding ist (loc,b,c) = + (loc,glob_quantified_hypothesis ist b,glob_constr ist c) let glob_bindings ist = function | NoBindings -> NoBindings @@ -1065,8 +1065,8 @@ let interp_induction_arg ist = function (* (constr_interp ist (Termast.ast_of_qualid (make_short_qualid id)))*) (constr_interp ist (CRef (Ident (loc,id)))) -let binding_interp ist (b,c) = - (interp_quantified_hypothesis ist b,constr_interp ist c) +let binding_interp ist (loc,b,c) = + (loc,interp_quantified_hypothesis ist b,constr_interp ist c) let bindings_interp ist = function | NoBindings -> NoBindings |