diff options
| author | Pierre-Marie Pédrot | 2016-11-11 17:48:47 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-02-14 17:28:39 +0100 |
| commit | 7267dfafe9215c35275a39814c8af451961e997c (patch) | |
| tree | c9b8f5f882aa92e529c4ce0789a8a9981efc2689 /plugins/decl_mode | |
| parent | 536026f3e20f761e8ef366ed732da7d3b626ac5e (diff) | |
Goal API using EConstr.
Diffstat (limited to 'plugins/decl_mode')
| -rw-r--r-- | plugins/decl_mode/decl_proof_instr.ml | 6 | ||||
| -rw-r--r-- | plugins/decl_mode/g_decl_mode.ml4 | 2 |
2 files changed, 4 insertions, 4 deletions
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index 44cd22c8bb..3bb6f1b5d5 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -41,7 +41,7 @@ let clear ids { it = goal; sigma } = let ids = List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty ids in let env = Goal.V82.env sigma goal in let sign = Goal.V82.hyps sigma goal in - let cl = Goal.V82.concl sigma goal in + let cl = EConstr.Unsafe.to_constr (Goal.V82.concl sigma goal) in let evdref = ref (Evd.clear_metas sigma) in let (hyps, concl) = try Evarutil.clear_hyps_in_evi env evdref sign cl ids @@ -49,7 +49,7 @@ let clear ids { it = goal; sigma } = user_err (str "Cannot clear " ++ pr_id id) in let sigma = !evdref in - let (gl,ev,sigma) = Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal) in + let (gl,ev,sigma) = Goal.V82.mk_goal sigma hyps (EConstr.of_constr concl) (Goal.V82.extra sigma goal) in let sigma = Goal.V82.partial_solution_to sigma goal gl ev in { it = [gl]; sigma } @@ -74,7 +74,7 @@ let tcl_change_info_gen info_gen = let concl = pf_concl gls in let hyps = Goal.V82.hyps (project gls) it in let extra = Goal.V82.extra (project gls) it in - let (gl,ev,sigma) = Goal.V82.mk_goal (project gls) hyps concl (info_gen extra) in + let (gl,ev,sigma) = Goal.V82.mk_goal (project gls) hyps (EConstr.of_constr concl) (info_gen extra) in let sigma = Goal.V82.partial_solution sigma it ev in { it = [gl] ; sigma= sigma; } ) diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4 index 18a35c6cfb..9e2c9f5973 100644 --- a/plugins/decl_mode/g_decl_mode.ml4 +++ b/plugins/decl_mode/g_decl_mode.ml4 @@ -25,7 +25,7 @@ open Ppdecl_proof let pr_goal gs = let (g,sigma) = Goal.V82.nf_evar (Tacmach.project gs) (Evd.sig_it gs) in let env = Goal.V82.env sigma g in - let concl = Goal.V82.concl sigma g in + let concl = EConstr.Unsafe.to_constr (Goal.V82.concl sigma g) in let goal = Printer.pr_context_of env sigma ++ cut () ++ str "============================" ++ cut () ++ |