diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-05-29 11:09:01 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-05-29 11:09:01 +0000 |
| commit | a3ab8b07b912afd1b883ed60bd532b5a29bccd8f (patch) | |
| tree | 8f5755d4bca03047baa9cebf41d8157b0380d92c /interp/constrextern.ml | |
| parent | 525090840aa3cd661bdac013860766fcc3886731 (diff) | |
Stuff about notation_constr (ex-aconstr) now in notation_ops.ml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15381 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/constrextern.ml')
| -rw-r--r-- | interp/constrextern.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 299ea8d79..c8a43c866 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -23,6 +23,7 @@ open Libnames open Impargs open Constrexpr open Notation_term +open Notation_ops open Topconstr open Glob_term open Glob_ops @@ -470,7 +471,7 @@ let rec extern_symbol_ind_pattern allscopes vars ind args = function | (keyrule,pat,n as _rule)::rules -> try apply_notation_to_pattern dummy_loc - (match_aconstr_ind_pattern ind args pat) allscopes vars keyrule + (match_notation_constr_ind_pattern ind args pat) allscopes vars keyrule with No_match -> extern_symbol_ind_pattern allscopes vars ind args rules @@ -763,7 +764,7 @@ let rec extern inctx scopes vars r = (sub_extern false scopes vars tm, (na',Option.map (fun (loc,ind,nal) -> let args = List.map (fun x -> PatVar (dummy_loc, x)) nal in - let fullargs = Topconstr.add_patterns_for_params ind args in + let fullargs = Notation_ops.add_patterns_for_params ind args in extern_ind_pattern_in_scope scopes vars ind fullargs ) x))) tml in let eqns = List.map (extern_eqn inctx scopes vars) eqns in |