diff options
Diffstat (limited to 'proofs/goal.ml')
| -rw-r--r-- | proofs/goal.ml | 48 |
1 files changed, 23 insertions, 25 deletions
diff --git a/proofs/goal.ml b/proofs/goal.ml index 111a947a..ba7e458f 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -1,28 +1,28 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Util open Pp -open Term -open Sigma.Notations -open Context.Named.Declaration + +module NamedDecl = Context.Named.Declaration (* This module implements the abstract interface to goals *) (* A general invariant of the module, is that a goal whose associated evar is defined in the current evar_map, should not be accessed. *) (* type of the goals *) -type goal = Evd.evar +type goal = Evar.t let pr_goal e = str "GOAL:" ++ Pp.int (Evar.repr e) let uid e = string_of_int (Evar.repr e) -let get_by_uid u = Evar.unsafe_of_int (int_of_string u) (* Layer to implement v8.2 tactic engine ontop of the new architecture. Types are different from what they used to be due to a change of the @@ -48,7 +48,7 @@ module V82 = struct (* Access to ".evar_concl" *) let concl evars gl = let evi = Evd.find evars gl in - evi.Evd.evar_concl + EConstr.of_constr evi.Evd.evar_concl (* Access to ".evar_extra" *) let extra evars gl = @@ -61,24 +61,22 @@ module V82 = struct be shelved. It must not appear as a future_goal, so the future goals are restored to their initial value after the evar is created. *) - let prev_future_goals = Evd.future_goals evars in - let prev_principal_goal = Evd.principal_future_goal evars in + let concl = EConstr.Unsafe.to_constr concl in + let prev_future_goals = Evd.save_future_goals evars in let evi = { Evd.evar_hyps = hyps; Evd.evar_concl = concl; Evd.evar_filter = Evd.Filter.identity; Evd.evar_body = Evd.Evar_empty; - Evd.evar_source = (Loc.ghost,Evar_kinds.GoalEvar); + Evd.evar_source = (Loc.tag Evar_kinds.GoalEvar); Evd.evar_candidates = None; Evd.evar_extra = extra } in let evi = Typeclasses.mark_unresolvable evi in - let evars = Sigma.Unsafe.of_evar_map evars in - let Sigma (evk, evars, _) = Evarutil.new_pure_evar_full evars evi in - let evars = Sigma.to_evar_map evars in - let evars = Evd.restore_future_goals evars prev_future_goals prev_principal_goal in + let (evars, evk) = Evarutil.new_pure_evar_full evars evi in + let evars = Evd.restore_future_goals evars prev_future_goals in let ctxt = Environ.named_context_of_val hyps in - let inst = Array.map_of_list (mkVar % get_id) ctxt in - let ev = Term.mkEvar (evk,inst) in + let inst = Array.map_of_list (NamedDecl.get_id %> EConstr.mkVar) ctxt in + let ev = EConstr.mkEvar (evk,inst) in (evk, ev, evars) (* Instantiates a goal with an open term *) @@ -88,7 +86,7 @@ module V82 = struct if not (Evarutil.occur_evar_upto sigma evk c) then () else Pretype_errors.error_occur_check Environ.empty_env sigma evk c in - Evd.define evk c sigma + Evd.define evk (EConstr.Unsafe.to_constr c) sigma (* Instantiates a goal with an open term, using name of goal for evk' *) let partial_solution_to sigma evk evk' c = @@ -102,7 +100,7 @@ module V82 = struct let same_goal evars1 gl1 evars2 gl2 = let evi1 = Evd.find evars1 gl1 in let evi2 = Evd.find evars2 gl2 in - Term.eq_constr evi1.Evd.evar_concl evi2.Evd.evar_concl && + Constr.equal evi1.Evd.evar_concl evi2.Evd.evar_concl && Environ.eq_named_context_val evi1.Evd.evar_hyps evi2.Evd.evar_hyps let weak_progress glss gls = @@ -130,9 +128,7 @@ module V82 = struct let new_evi = { evi with Evd.evar_hyps = new_hyps; Evd.evar_filter = new_filter } in let new_evi = Typeclasses.mark_unresolvable new_evi in - let sigma = Sigma.Unsafe.of_evar_map Evd.empty in - let Sigma (evk, sigma, _) = Evarutil.new_pure_evar_full sigma new_evi in - let sigma = Sigma.to_evar_map sigma in + let (sigma, evk) = Evarutil.new_pure_evar_full Evd.empty new_evi in { Evd.it = evk ; sigma = sigma; } (* Used by the compatibility layer and typeclasses *) @@ -144,14 +140,16 @@ module V82 = struct (* Goal represented as a type, doesn't take into account section variables *) let abstract_type sigma gl = + let open EConstr in let (gl,sigma) = nf_evar sigma gl in let env = env sigma gl in let genv = Global.env () in let is_proof_var decl = - try ignore (Environ.lookup_named (get_id decl) genv); false + try ignore (Environ.lookup_named (NamedDecl.get_id decl) genv); false with Not_found -> true in Environ.fold_named_context_reverse (fun t decl -> if is_proof_var decl then + let decl = Termops.map_named_decl EConstr.of_constr decl in mkNamedProd_or_LetIn decl t else t |