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/constrexpr_ops.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/constrexpr_ops.ml')
| -rw-r--r-- | interp/constrexpr_ops.ml | 14 |
1 files changed, 1 insertions, 13 deletions
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index c8a0e5638..85ad1cee7 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -10,7 +10,6 @@ open Pp open Util open Names open Libnames -open Glob_term open Constrexpr open Misctypes open Decl_kinds @@ -150,7 +149,7 @@ let rec constr_expr_eq e1 e2 = Evar.equal ev1 ev2 && Option.equal (List.equal constr_expr_eq) c1 c2 | CSort(_,s1), CSort(_,s2) -> - Glob_ops.glob_sort_eq s1 s2 + Miscops.glob_sort_eq s1 s2 | CCast(_,a1,(CastConv b1|CastVM b1)), CCast(_,a2,(CastConv b2|CastVM b2)) -> constr_expr_eq a1 a2 && constr_expr_eq b1 b2 @@ -336,14 +335,3 @@ let coerce_to_name = function | a -> Errors.user_err_loc (constr_loc a,"coerce_to_name", str "This expression should be a name.") - -let rec raw_cases_pattern_expr_of_glob_constr 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 (raw_cases_pattern_expr_of_glob_constr looked_for) l,[]) - | _ -> raise Not_found |