diff options
| author |  Stephane Glondu <steph@glondu.net> | 2010-10-14 17:58:31 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2010-10-14 17:58:31 +0200 |
| commit | d06cea3ce4526736b5d32ba1780dbbc87c37c981 (patch) | |
| tree | 2c2ea5a4633a41cfd4451e1eefb79c171312c881 /plugins/extraction/mlutil.ml | |
| parent | aae7cec8d7f5048215b7ed06a8e94cb032bfd21a (diff) | |
| parent | 8f4d4c66134804bbf2d2fe65c893b68387272d31 (diff) | |
Merge commit 'upstream/8.3+dfsg' into experimental/master
Diffstat (limited to 'plugins/extraction/mlutil.ml')
| -rw-r--r-- | plugins/extraction/mlutil.ml | 12 |
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: |