From 870075f34dd9fa5792bfbf413afd3b96f17e76a0 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Fri, 8 Aug 2008 13:18:42 +0200
Subject: Imported Upstream version 8.2~beta4+dfsg

---
 proofs/tacmach.ml | 24 ++++++++++--------------
 1 file changed, 10 insertions(+), 14 deletions(-)

(limited to 'proofs/tacmach.ml')

diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 213cc13f..6bbaff08 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -6,8 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: tacmach.ml 10544 2008-02-09 11:31:35Z herbelin $ *)
+(* $Id: tacmach.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
 
+open Pp
 open Util
 open Names
 open Nameops
@@ -58,7 +59,7 @@ let pf_get_hyp gls id =
   try 
     Sign.lookup_named id (pf_hyps gls)
   with Not_found -> 
-    error ("No such hypothesis : " ^ (string_of_id id))
+    error ("No such hypothesis: " ^ (string_of_id id))
 
 let pf_get_hyp_typ gls id =
   let (_,_,ty)= (pf_get_hyp gls id) in
@@ -175,15 +176,11 @@ let refiner = refiner
 let introduction_no_check id =
   refiner (Prim (Intro id))
 
-(* This does not check that the dependencies are correct *)
-let intro_replacing_no_check whereid gl = 
-  refiner (Prim (Intro_replacing whereid)) gl
-
-let internal_cut_no_check id t gl = 
-  refiner (Prim (Cut (true,id,t))) gl
+let internal_cut_no_check replace id t gl = 
+  refiner (Prim (Cut (true,replace,id,t))) gl
 
-let internal_cut_rev_no_check id t gl = 
-  refiner (Prim (Cut (false,id,t))) gl
+let internal_cut_rev_no_check replace id t gl = 
+  refiner (Prim (Cut (false,replace,id,t))) gl
 
 let refine_no_check c gl = 
   refiner (Prim (Refine c)) gl
@@ -220,13 +217,12 @@ let mutual_cofix f others gl =
 (* Versions with consistency checks *)
 
 let introduction id    = with_check (introduction_no_check id) 
-let intro_replacing id = with_check (intro_replacing_no_check id)
-let internal_cut d t     = with_check (internal_cut_no_check d t)
-let internal_cut_rev d t = with_check (internal_cut_rev_no_check d t)
+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)
 let convert_concl d sty = with_check (convert_concl_no_check d sty)
 let convert_hyp d      = with_check (convert_hyp_no_check d)
-let thin l             = with_check (thin_no_check l)
+let thin c             = with_check (thin_no_check c)
 let thin_body c        = with_check (thin_body_no_check c)
 let move_hyp b id id'  = with_check (move_hyp_no_check b id id') 
 let rename_hyp l       = with_check (rename_hyp_no_check l)
-- 
cgit v1.2.3