diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-02-12 19:35:59 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-02-12 19:35:59 +0000 |
| commit | f03055b760f79e4e5a1efb4706823a2735a24048 (patch) | |
| tree | 6d6f90764c910086379fdec8ca982f7551014855 /interp/constrintern.ml | |
| parent | b847fcc99e35a09b862aa758c5e3f0b08a93202d (diff) | |
Localisation erreur interp_notation
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5329 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 821e9a26a..dfa6a1b94 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -502,7 +502,7 @@ let rec intern_cases_pattern scopes aliases tmp_scope = function | CPatNotation (loc, ntn, args) -> let ntn,args = contract_pat_notation ntn args in let scopes = option_cons tmp_scope scopes in - let ((ids,c),df) = Symbols.interp_notation ntn scopes in + let ((ids,c),df) = Symbols.interp_notation loc ntn scopes in if !dump then dump_notation_location (patntn_loc loc args ntn) ntn df; let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids args in subst_cases_pattern loc aliases intern_cases_pattern subst scopes c @@ -726,7 +726,7 @@ let internalise sigma env allow_soapp lvar c = | CNotation (loc,ntn,args) -> let ntn,args = contract_notation ntn args in let scopes = option_cons tmp_scope scopes in - let ((ids,c),df) = Symbols.interp_notation ntn scopes in + let ((ids,c),df) = Symbols.interp_notation loc ntn scopes in if !dump then dump_notation_location (ntn_loc loc args ntn) ntn df; let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids args in subst_rawconstr loc intern subst env c |