Merge PR #830: Moving assert (the "Cut" rule) to new proof engine

5 files changed, 10 insertions, 61 deletions

diff --git a/proofs/logic.ml b/proofs/logic.ml
index 17128b92e..20d075ae1 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 84a21044b..9d0756b33 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 11f1a13e6..2ad5f607f 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 2ed9416d1..a4d662e0a 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 40b6573a1..93bf428fd 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). } *)