A version of convert_concl and convert_hyp in new proof engine.

Not very optimized though (if we apply convert_hyp on any hyp, a new
evar will be generated for every different hyp...).

4 files changed, 14 insertions, 29 deletions

diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index a21447fbb..470dc9d9c 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -580,7 +580,7 @@ let assume_tac hyps gls =
        tclTHEN
 	 (push_intro_tac
 	    (fun id ->
-	       convert_hyp (id,None,st.st_it)) st.st_label))
+	       Proofview.V82.of_tactic (convert_hyp (id,None,st.st_it))) st.st_label))
 	 hyps tclIDTAC gls
 
 let assume_hyps_or_theses hyps gls =
@@ -590,7 +590,7 @@ let assume_hyps_or_theses hyps gls =
 	   tclTHEN
 	     (push_intro_tac
 		(fun id ->
-		   convert_hyp (id,None,c)) nam)
+		   Proofview.V82.of_tactic (convert_hyp (id,None,c))) nam)
        | Hprop {st_label=nam;st_it=Thesis (tk)} ->
 	   tclTHEN
 	     (push_intro_tac
@@ -602,7 +602,7 @@ let assume_st hyps gls =
     (fun st ->
        tclTHEN
 	 (push_intro_tac
-	    (fun id -> convert_hyp (id,None,st.st_it)) st.st_label))
+	    (fun id -> Proofview.V82.of_tactic (convert_hyp (id,None,st.st_it))) st.st_label))
 	 hyps tclIDTAC gls
 
 let assume_st_letin hyps gls =
@@ -611,7 +611,7 @@ let assume_st_letin hyps gls =
        tclTHEN
 	 (push_intro_tac
 	    (fun id ->
-	       convert_hyp (id,Some (fst st.st_it),snd st.st_it)) st.st_label))
+	       Proofview.V82.of_tactic (convert_hyp (id,Some (fst st.st_it),snd st.st_it))) st.st_label))
 	 hyps tclIDTAC gls
 
 (* suffices *)
@@ -705,7 +705,7 @@ let rec consider_match may_intro introduced available expected gls =
 	  error "Not enough sub-hypotheses to match statements."
 	    (* should tell which ones *)
     | id::rest_ids,(Hvar st | Hprop st)::rest ->
-	tclIFTHENELSE (convert_hyp (id,None,st.st_it))
+	tclIFTHENELSE (Proofview.V82.of_tactic (convert_hyp (id,None,st.st_it)))
 	  begin
 	    match st.st_label with
 		Anonymous ->
@@ -774,11 +774,11 @@ let cast_tac id_or_thesis typ gls =
   match id_or_thesis with
       This id ->
 	let (_,body,_) = pf_get_hyp gls id in
-	  convert_hyp (id,body,typ) gls
+	  Proofview.V82.of_tactic (convert_hyp (id,body,typ)) gls
     | Thesis (For _ ) ->
 	error "\"thesis for ...\" is not applicable here."
     | Thesis Plain ->
-          convert_concl typ DEFAULTcast gls
+          Proofview.V82.of_tactic (convert_concl typ DEFAULTcast) gls
 
 (* per cases *)
 
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index f8fd71ae2..847fda8cd 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -566,7 +566,7 @@ let abstract_path typ path t =
 
 let focused_simpl path gl =
   let newc = context (fun i t -> pf_nf gl t) (List.rev path) (pf_concl gl) in
-  convert_concl_no_check newc DEFAULTcast gl
+  Proofview.V82.of_tactic (convert_concl_no_check newc DEFAULTcast) gl
 
 let focused_simpl path = focused_simpl path
 
@@ -1806,15 +1806,15 @@ let destructure_hyps =
 		    match destructurate_type (pf_nf typ) with
 		    | Kapp(Nat,_) ->
                         (Tacticals.New.tclTHEN
-			   (Proofview.V82.tactic (convert_hyp_no_check
+			   (convert_hyp_no_check
                                                     (i,body,
-				                     (mkApp (Lazy.force coq_neq, [| t1;t2|])))))
+				                     (mkApp (Lazy.force coq_neq, [| t1;t2|]))))
 			   (loop lit))
 		    | Kapp(Z,_) ->
                         (Tacticals.New.tclTHEN
-			   (Proofview.V82.tactic (convert_hyp_no_check
+			   (convert_hyp_no_check
                                                     (i,body,
-				                     (mkApp (Lazy.force coq_Zne, [| t1;t2|])))))
+				                     (mkApp (Lazy.force coq_Zne, [| t1;t2|]))))
 			   (loop lit))
 		    | _ -> loop lit
                   end
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index ed7f18001..64166a0de 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -457,8 +457,8 @@ let quote f lid =
       | _ -> assert false
     in
     match ivs.variable_lhs with
-    | None -> Proofview.V82.tactic (Tactics.convert_concl (mkApp (f, [| p |])) DEFAULTcast)
-    | Some _ -> Proofview.V82.tactic (Tactics.convert_concl (mkApp (f, [| vm; p |])) DEFAULTcast)
+    | None -> Tactics.convert_concl (mkApp (f, [| p |])) DEFAULTcast
+    | Some _ -> Tactics.convert_concl (mkApp (f, [| vm; p |])) DEFAULTcast
   end
 
 let gen_quote cont c f lid =
diff --git a/plugins/xml/README b/plugins/xml/README
deleted file mode 100644
index e3bcdaf05..000000000
--- a/plugins/xml/README
+++ /dev/null
@@ -1,15 +0,0 @@
-The xml export plugin for Coq has been discontinued for lack of users:
-it was most certainly broken while imposing a non-negligible cost on
-Coq development. Its purpose was to give export Coq's kernel objects
-in xml form for treatment by external tools.
-
-If you are looking for such a tool, you may want to look at commit
-7cfe0a70eda671ada6a46cd779ef9308f7e0fdb9 responsible for the deletion
-of this plugin (for instance, git checkout
-7cfe0a70eda671ada6a46cd779ef9308f7e0fdb9^ including the "^", will lead
-you to the last commit before the xml plugin was deleted).
-
-Bear in mind, however, that the plugin was not working properly at the
-time. You may want instead to write to the original author of the
-plugin, Claudio Sacerdoti-Coen at sacerdot@cs.unibo.it. He has a
-stable version of the plugin for an old version of Coq.