summaryrefslogtreecommitdiff
path: root/plugins/extraction/mlutil.ml
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2010-10-14 17:58:31 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2010-10-14 17:58:31 +0200
commitd06cea3ce4526736b5d32ba1780dbbc87c37c981 (patch)
tree2c2ea5a4633a41cfd4451e1eefb79c171312c881 /plugins/extraction/mlutil.ml
parentaae7cec8d7f5048215b7ed06a8e94cb032bfd21a (diff)
parent8f4d4c66134804bbf2d2fe65c893b68387272d31 (diff)
Merge commit 'upstream/8.3+dfsg' into experimental/master
Diffstat (limited to 'plugins/extraction/mlutil.ml')
-rw-r--r--plugins/extraction/mlutil.ml12
1 files changed, 6 insertions, 6 deletions
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 745a78fe..a079aacc 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: mlutil.ml 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: mlutil.ml 13420 2010-09-16 15:47:08Z letouzey $ i*)
(*i*)
open Pp
@@ -656,10 +656,10 @@ let rec tmp_head_lams = function
let rec ast_glob_subst s t = match t with
| MLapp ((MLglob ((ConstRef kn) as refe)) as f, a) ->
let a = List.map (fun e -> tmp_head_lams (ast_glob_subst s e)) a in
- (try linear_beta_red a (Refmap.find refe s)
+ (try linear_beta_red a (Refmap'.find refe s)
with Not_found -> MLapp (f, a))
| MLglob ((ConstRef kn) as refe) ->
- (try Refmap.find refe s with Not_found -> t)
+ (try Refmap'.find refe s with Not_found -> t)
| _ -> ast_map (ast_glob_subst s) t
@@ -1259,7 +1259,7 @@ let con_of_string s =
| [] -> assert false
let manual_inline_set =
- List.fold_right (fun x -> Cset.add (con_of_string x))
+ List.fold_right (fun x -> Cset_env.add (con_of_string x))
[ "Coq.Init.Wf.well_founded_induction_type";
"Coq.Init.Wf.well_founded_induction";
"Coq.Init.Wf.Acc_iter";
@@ -1271,10 +1271,10 @@ let manual_inline_set =
"Coq.Init.Logic.eq_rect_r";
"Coq.Init.Specif.proj1_sig";
]
- Cset.empty
+ Cset_env.empty
let manual_inline = function
- | ConstRef c -> Cset.mem c manual_inline_set
+ | ConstRef c -> Cset_env.mem c manual_inline_set
| _ -> false
(* If the user doesn't say he wants to keep [t], we inline in two cases: