diff options
| author | letouzey | 2012-05-29 11:08:50 +0000 |
|---|---|---|
| committer | letouzey | 2012-05-29 11:08:50 +0000 |
| commit | 392300a73bc4e57d2be865d9a8d77c608ef02f59 (patch) | |
| tree | 44b4f39e7f92f29f4626d4aa8265fe68eb129111 /interp/implicit_quantifiers.ml | |
| parent | a936f2e879ac1f9b2e7e9d8a5376469e3d53c606 (diff) | |
New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15375 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/implicit_quantifiers.ml')
| -rw-r--r-- | interp/implicit_quantifiers.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 3384d79a52..a39347d556 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -18,7 +18,7 @@ open Mod_subst open Errors open Util open Glob_term -open Topconstr +open Constrexpr open Libnames open Typeclasses open Typeclasses_errors @@ -111,8 +111,8 @@ let free_vars_of_constr_expr c ?(bound=Idset.empty) l = let rec aux bdvars l c = match c with | CRef (Ident (loc,id)) -> found loc id bdvars l | CNotation (_, "{ _ : _ | _ }", (CRef (Ident (_, id)) :: _, [], [])) when not (Idset.mem id bdvars) -> - fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux (Idset.add id bdvars) l c - | c -> fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux bdvars l c + Topconstr.fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux (Idset.add id bdvars) l c + | c -> Topconstr.fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux bdvars l c in aux bound l c let ids_of_names l = @@ -246,7 +246,7 @@ let combine_params avoid fn applied needed = aux (t' :: ids) avoid' app need | (x,_) :: _, [] -> - user_err_loc (constr_loc x,"",str "Typeclass does not expect more arguments") + user_err_loc (Topconstr.constr_loc x,"",str "Typeclass does not expect more arguments") in aux [] avoid applied needed let combine_params_freevar = |