summaryrefslogtreecommitdiff
path: root/proofs/tacmach.ml
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/tacmach.ml')
-rw-r--r--proofs/tacmach.ml24
1 files changed, 10 insertions, 14 deletions
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)