diff options
| author |  Pierre Boutillier <pierre.boutillier@ens-lyon.org> | 2014-01-30 12:21:05 +0100 |
|---|---|---|
| committer | Pierre Boutillier <pierre.boutillier@ens-lyon.org> | 2014-02-24 13:35:05 +0100 |
| commit | 97614d75a3ae8e515170d1c58c0cbbdf55346558 (patch) | |
| tree | 2d18af0abebdbccb662fb8ff3ed89918fbfbe7fc /plugins/decl_mode | |
| parent | c4370e5394cc9f678250150bd5bb407629b21913 (diff) | |
Stack operations of Reductionops in Reductionops.Stack
Diffstat (limited to 'plugins/decl_mode')
| -rw-r--r-- | plugins/decl_mode/decl_proof_instr.ml | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index 6e53ae6a2..45ffb450f 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -28,7 +28,6 @@ open Term open Vars open Termops open Namegen -open Reductionops open Goptions open Misctypes @@ -339,7 +338,7 @@ let rec nf_list evd = if meta_defined evd m then nf_list evd others else - (m,nf_meta evd typ)::nf_list evd others + (m,Reductionops.nf_meta evd typ)::nf_list evd others let find_subsubgoal c ctyp skip submetas gls = let env= pf_env gls in @@ -374,7 +373,7 @@ let find_subsubgoal c ctyp skip submetas gls = dfs n end in let nse= try dfs skip with Stack.Empty -> raise Not_found in - nf_list nse.se_evd nse.se_meta_list,nf_meta nse.se_evd (mkMeta 0) + nf_list nse.se_evd nse.se_meta_list,Reductionops.nf_meta nse.se_evd (mkMeta 0) let concl_refiner metas body gls = let concl = pf_concl gls in @@ -1044,7 +1043,7 @@ let thesis_for obj typ per_info env= ((Printer.pr_constr_env env obj) ++ spc () ++ str "cannot give an induction hypothesis (wrong parameters).") in let hd2 = (applist ((lift (List.length rc) per_info.per_pred),args@[obj])) in - compose_prod rc (whd_beta Evd.empty hd2) + compose_prod rc (Reductionops.whd_beta Evd.empty hd2) let rec build_product_dep pat_info per_info args body gls = match args with @@ -1174,7 +1173,7 @@ let hrec_for fix_id per_info gls obj_id = try List.for_all2 eq_constr params per_info.per_params with Invalid_argument _ -> false end; let hd2 = applist (mkVar fix_id,args@[obj]) in - compose_lam rc (whd_beta gls.sigma hd2) + compose_lam rc (Reductionops.whd_beta gls.sigma hd2) let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = |