Moving "assert" (internally "Cut") to the new proof engine.

It allows in particular to have "Info" on tactic "assert" and
derivatives not to give an "<unknown>".

4 files changed, 0 insertions, 61 deletions

diff --git a/proofs/logic.ml b/proofs/logic.ml
index 0621af4e80..db9e847c06 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
@@ -539,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/proof_type.mli b/proofs/proof_type.mli
index e59db9e427..ec4af86b9c 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -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 f9d9f25ccf..bdfa399aa4 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 3d2fa72c17..aac7b90ee4 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). } *)