diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/evar_refiner.ml | 3 | ||||
| -rw-r--r-- | proofs/evar_refiner.mli | 4 | ||||
| -rw-r--r-- | proofs/logic.ml | 50 | ||||
| -rw-r--r-- | proofs/logic.mli | 6 | ||||
| -rw-r--r-- | proofs/proof_type.ml | 2 | ||||
| -rw-r--r-- | proofs/tacmach.ml | 10 | ||||
| -rw-r--r-- | proofs/tacmach.mli | 3 |
7 files changed, 16 insertions, 62 deletions
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index cc81adb853..48fa2202ee 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -13,11 +13,14 @@ open Evd open Evarutil open Evarsolve open Pp +open Glob_term (******************************************) (* Instantiation of existential variables *) (******************************************) +type glob_constr_ltac_closure = ltac_var_map * glob_constr + let depends_on_evar sigma evk _ (pbty,_,t1,t2) = let t1 = EConstr.of_constr t1 in let t2 = EConstr.of_constr t2 in diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli index b65ffb1bee..5d69715967 100644 --- a/proofs/evar_refiner.mli +++ b/proofs/evar_refiner.mli @@ -7,9 +7,11 @@ (************************************************************************) open Evd -open Pretyping +open Glob_term (** Refinement of existential variables. *) +type glob_constr_ltac_closure = ltac_var_map * glob_constr + val w_refine : evar * evar_info -> glob_constr_ltac_closure -> evar_map -> evar_map diff --git a/proofs/logic.ml b/proofs/logic.ml index 17128b92e1..20d075ae14 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -22,7 +22,6 @@ open Proof_type open Type_errors open Retyping open Misctypes -open Context.Named.Declaration module NamedDecl = Context.Named.Declaration @@ -93,15 +92,6 @@ let check_typability env sigma c = (* Implementation of the structural rules (moving and deleting hypotheses around) *) -(* The Clear tactic: it scans the context for hypotheses to be removed - (instead of iterating on the list of identifier to be removed, which - forces the user to give them in order). *) - -let clear_hyps2 env sigma ids sign t cl = - let evdref = ref (Evd.clear_metas sigma) in - let (hyps,t,cl) = Evarutil.clear_hyps2_in_evi env evdref sign t cl ids in - (hyps, t, cl, !evdref) - (* The ClearBody tactic *) (* Reordering of the context *) @@ -200,14 +190,6 @@ let move_location_eq m1 m2 = match m1, m2 with | MoveFirst, MoveFirst -> true | _ -> false -let rec get_hyp_after h = function - | [] -> error_no_such_hypothesis h - | d :: right -> - if Id.equal (NamedDecl.get_id d) h then - match right with d' ::_ -> MoveBefore (NamedDecl.get_id d') | [] -> MoveFirst - else - get_hyp_after h right - let split_sign hfrom hto l = let rec splitrec left toleft = function | [] -> error_no_such_hypothesis hfrom @@ -282,6 +264,10 @@ let move_hyp_in_named_context sigma hfrom hto sign = split_sign hfrom hto (named_context_of_val sign) in move_hyp sigma toleft (left,declfrom,right) hto +let insert_decl_in_named_context sigma decl hto sign = + let open EConstr in + move_hyp sigma false ([],decl,named_context_of_val sign) hto + (**********************************************************************) @@ -535,37 +521,9 @@ let convert_hyp check sign sigma d = (* Primitive tactics are handled here *) let prim_refiner r sigma goal = - 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 mk_goal hyps concl = - Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal) - in - let open EConstr in match r with (* Logical rules *) - | Cut (b,replace,id,t) -> -(* if !check && not (Retyping.get_sort_of env sigma t) then*) - let t = EConstr.of_constr t in - let (sg1,ev1,sigma) = mk_goal sign (nf_betaiota sigma t) in - let sign,t,cl,sigma = - if replace then - let nexthyp = get_hyp_after id (named_context_of_val sign) in - let sign,t,cl,sigma = clear_hyps2 env sigma (Id.Set.singleton id) sign t cl in - move_hyp sigma false ([], LocalAssum (id,t),named_context_of_val sign) - nexthyp, - t,cl,sigma - else - (if !check && mem_named_context_val id sign then - user_err ~hdr:"Logic.prim_refiner" - (str "Variable " ++ pr_id id ++ str " is already declared."); - push_named_context_val (LocalAssum (id,t)) sign,t,cl,sigma) in - let (sg2,ev2,sigma) = - Goal.V82.mk_goal sigma sign cl (Goal.V82.extra sigma goal) in - let oterm = mkLetIn (Name id, ev1, t, EConstr.Vars.subst_var id ev2) in - let sigma = Goal.V82.partial_solution_to sigma goal sg2 oterm in - if b then ([sg1;sg2],sigma) else ([sg2;sg1],sigma) - | Refine c -> let cl = EConstr.Unsafe.to_constr cl in check_meta_variables c; diff --git a/proofs/logic.mli b/proofs/logic.mli index 84a21044b2..9d0756b332 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -52,6 +52,8 @@ type refiner_error = exception RefinerError of refiner_error +val error_no_such_hypothesis : Id.t -> 'a + val catchable_exception : exn -> bool val convert_hyp : bool -> Environ.named_context_val -> evar_map -> @@ -59,3 +61,7 @@ val convert_hyp : bool -> Environ.named_context_val -> evar_map -> val move_hyp_in_named_context : Evd.evar_map -> Id.t -> Id.t Misctypes.move_location -> Environ.named_context_val -> Environ.named_context_val + +val insert_decl_in_named_context : Evd.evar_map -> + EConstr.named_declaration -> Id.t Misctypes.move_location -> + Environ.named_context_val -> Environ.named_context_val diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index 11f1a13e6e..2ad5f607f2 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -9,14 +9,12 @@ (** Legacy proof engine. Do not use in newly written code. *) open Evd -open Names open Term (** This module defines the structure of proof tree and the tactic type. So, it is used by [Proof_tree] and [Refiner] *) type prim_rule = - | Cut of bool * bool * Id.t * types | Refine of constr (** Nowadays, the only rules we'll consider are the primitive rules *) diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 2ed9416d10..a4d662e0ae 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -115,22 +115,12 @@ let pf_matches gl p c = pf_apply Constr_matching.matches_conv gl p c let refiner = refiner -let internal_cut_no_check replace id t gl = - let t = EConstr.Unsafe.to_constr t in - refiner (Cut (true,replace,id,t)) gl - -let internal_cut_rev_no_check replace id t gl = - let t = EConstr.Unsafe.to_constr t in - refiner (Cut (false,replace,id,t)) gl - let refine_no_check c gl = let c = EConstr.Unsafe.to_constr c in refiner (Refine c) gl (* Versions with consistency checks *) -let internal_cut b d t = with_check (internal_cut_no_check b d t) -let internal_cut_rev b d t = with_check (internal_cut_rev_no_check b d t) let refine c = with_check (refine_no_check c) (* Pretty-printers *) diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 40b6573a15..93bf428fdc 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -84,13 +84,10 @@ val pf_is_matching : goal sigma -> constr_pattern -> constr -> bool (** {6 The most primitive tactics. } *) val refiner : rule -> tactic -val internal_cut_no_check : bool -> Id.t -> types -> tactic val refine_no_check : constr -> tactic (** {6 The most primitive tactics with consistency and type checking } *) -val internal_cut : bool -> Id.t -> types -> tactic -val internal_cut_rev : bool -> Id.t -> types -> tactic val refine : constr -> tactic (** {6 Pretty-printing functions (debug only). } *) |