diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2014-03-01 19:50:59 +0100 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2014-03-02 20:00:02 +0100 |
| commit | 4b68dbe3428740a61cda825d3a45047571d9f299 (patch) | |
| tree | 487dff0e37d819e7de07196eac6f4699f8ab1f96 /interp/notation.ml | |
| parent | 412f848e681e3c94c635f65638310a13d675449e (diff) | |
Grammar.cma with less deps (Glob_ops and Nameops) after moving minor code
NB: new file miscprint.ml deserves to be part of printing.cma,
but should be part of proofs.cma for the moment, due to use in logic.ml
Diffstat (limited to 'interp/notation.ml')
| -rw-r--r-- | interp/notation.ml | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index 867e23395..262cbab2f 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -449,8 +449,18 @@ let interp_prim_token_gen g loc p local_scopes = let interp_prim_token = interp_prim_token_gen (fun x -> x) +(** [rcp_of_glob] : from [glob_constr] to [raw_cases_pattern_expr] *) + +let rec rcp_of_glob looked_for = function + | GVar (loc,id) -> RCPatAtom (loc,Some id) + | GHole (loc,_,_) -> RCPatAtom (loc,None) + | GRef (loc,g) -> looked_for g; RCPatCstr (loc, g,[],[]) + | GApp (loc,GRef (_,g),l) -> + looked_for g; RCPatCstr (loc, g, List.map (rcp_of_glob looked_for) l,[]) + | _ -> raise Not_found + let interp_prim_token_cases_pattern_expr loc looked_for p = - interp_prim_token_gen (Constrexpr_ops.raw_cases_pattern_expr_of_glob_constr looked_for) loc p + interp_prim_token_gen (rcp_of_glob looked_for) loc p let interp_notation loc ntn local_scopes = let scopes = make_current_scopes local_scopes in |