Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 30 insertions, 31 deletions

diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index b740baa8..9e35abfc 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -6,12 +6,12 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: tacmach.ml 12168 2009-06-06 21:34:37Z herbelin $ *)
+(* $Id$ *)
 
 open Pp
 open Util
 open Names
-open Nameops
+open Namegen
 open Sign
 open Term
 open Termops
@@ -55,10 +55,10 @@ let pf_nth_hyp_id gls n = let (id,c,t) = List.nth (pf_hyps gls) (n-1) in id
 
 let pf_last_hyp gl = List.hd (pf_hyps gl)
 
-let pf_get_hyp gls id = 
-  try 
+let pf_get_hyp gls id =
+  try
     Sign.lookup_named id (pf_hyps gls)
-  with Not_found -> 
+  with Not_found ->
     error ("No such hypothesis: " ^ (string_of_id id))
 
 let pf_get_hyp_typ gls id =
@@ -67,7 +67,7 @@ let pf_get_hyp_typ gls id =
 
 let pf_ids_of_hyps gls = ids_of_named_context (pf_hyps gls)
 
-let pf_get_new_id id gls = 
+let pf_get_new_id id gls =
   next_ident_away id (pf_ids_of_hyps gls)
 
 let pf_get_new_ids ids gls =
@@ -77,19 +77,19 @@ let pf_get_new_ids ids gls =
     ids []
 
 let pf_interp_constr gls c =
-  let evc = project gls in 
+  let evc = project gls in
   Constrintern.interp_constr evc (pf_env gls) c
 
 let pf_interp_type gls c =
-  let evc = project gls in 
+  let evc = project gls in
   Constrintern.interp_type evc (pf_env gls) c
 
 let pf_global gls id = Constrintern.construct_reference (pf_hyps gls) id
 
 let pf_parse_const gls = compose (pf_global gls) id_of_string
 
-let pf_reduction_of_red_expr gls re c = 
-  (fst (reduction_of_red_expr re)) (pf_env gls) (project gls) c 
+let pf_reduction_of_red_expr gls re c =
+  (fst (reduction_of_red_expr re)) (pf_env gls) (project gls) c
 
 let pf_apply f gls = f (pf_env gls) (project gls)
 let pf_reduce = pf_apply
@@ -98,7 +98,7 @@ let pf_whd_betadeltaiota         = pf_reduce whd_betadeltaiota
 let pf_whd_betadeltaiota_stack   = pf_reduce whd_betadeltaiota_stack
 let pf_hnf_constr                = pf_reduce hnf_constr
 let pf_red_product               = pf_reduce red_product
-let pf_nf                        = pf_reduce nf
+let pf_nf                        = pf_reduce simpl
 let pf_nf_betaiota               = pf_reduce (fun _ -> nf_betaiota)
 let pf_compute                   = pf_reduce compute
 let pf_unfoldn ubinds            = pf_reduce (unfoldn ubinds)
@@ -111,11 +111,14 @@ let pf_const_value              = pf_reduce (fun env _ -> constant_value env)
 let pf_reduce_to_quantified_ind = pf_reduce reduce_to_quantified_ind
 let pf_reduce_to_atomic_ind     = pf_reduce reduce_to_atomic_ind
 
-let hnf_type_of gls = compose (pf_whd_betadeltaiota gls) (pf_get_type_of gls)
+let pf_hnf_type_of gls = compose (pf_whd_betadeltaiota gls) (pf_get_type_of gls)
 
-let pf_check_type gls c1 c2 = 
+let pf_check_type gls c1 c2 =
   ignore (pf_type_of gls (mkCast (c1, DEFAULTcast, c2)))
 
+let pf_is_matching              = pf_apply Matching.is_matching_conv
+let pf_matches                  = pf_apply Matching.matches_conv
+
 (************************************)
 (* Tactics handling a list of goals *)
 (************************************)
@@ -176,16 +179,16 @@ let refiner = refiner
 let introduction_no_check id =
   refiner (Prim (Intro id))
 
-let internal_cut_no_check replace 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 replace 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 = 
+let refine_no_check c gl =
   refiner (Prim (Refine c)) gl
 
-let convert_concl_no_check c sty gl = 
+let convert_concl_no_check c sty gl =
   refiner (Prim (Convert_concl (c,sty))) gl
 
 let convert_hyp_no_check d gl =
@@ -199,31 +202,27 @@ let thin_no_check ids gl =
 let thin_body_no_check ids gl =
   if ids = [] then tclIDTAC gl else refiner (Prim (ThinBody ids)) gl
 
-let move_hyp_no_check with_dep id1 id2 gl = 
+let move_hyp_no_check with_dep id1 id2 gl =
   refiner (Prim (Move (with_dep,id1,id2))) gl
 
 let order_hyps idl gl =
   refiner (Prim (Order idl)) gl
 
-let rec rename_hyp_no_check l gl = match l with 
-  | [] -> tclIDTAC gl 
-  | (id1,id2)::l -> 
-      tclTHEN (refiner (Prim (Rename (id1,id2)))) 
+let rec rename_hyp_no_check l gl = match l with
+  | [] -> tclIDTAC gl
+  | (id1,id2)::l ->
+      tclTHEN (refiner (Prim (Rename (id1,id2))))
 	(rename_hyp_no_check l) gl
 
-let mutual_fix_with_index f n others j gl =
+let mutual_fix f n others j gl =
   with_check (refiner (Prim (FixRule (f,n,others,j)))) gl
 
-let mutual_fix f n others = mutual_fix_with_index f n others 0
-
-let mutual_cofix_with_index f others j gl =
+let mutual_cofix f others j gl =
   with_check (refiner (Prim (Cofix (f,others,j)))) gl
 
-let mutual_cofix f others = mutual_cofix_with_index f others 0
-    
 (* Versions with consistency checks *)
 
-let introduction id    = with_check (introduction_no_check id) 
+let introduction id    = with_check (introduction_no_check id)
 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)
@@ -231,7 +230,7 @@ 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 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 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)
 
 (* Pretty-printers *)
@@ -250,4 +249,4 @@ let pr_gls gls =
 let pr_glls glls =
   hov 0 (pr_evar_map (sig_sig glls) ++ fnl () ++
          prlist_with_sep pr_fnl db_pr_goal (sig_it glls))
-  
+