From 3ef7797ef6fc605dfafb32523261fe1b023aeecb Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Fri, 28 Apr 2006 14:59:16 +0000
Subject: Imported Upstream version 8.0pl3+8.1alpha

---
 contrib/funind/tacinvutils.ml | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

(limited to 'contrib/funind/tacinvutils.ml')

diff --git a/contrib/funind/tacinvutils.ml b/contrib/funind/tacinvutils.ml
index a125b9a7..2877c19d 100644
--- a/contrib/funind/tacinvutils.ml
+++ b/contrib/funind/tacinvutils.ml
@@ -21,9 +21,9 @@ open Reductionops
 (*s printing of constr -- debugging *)
 
 (* comment this line to see debug msgs *)
-let msg x = () ;; let prterm c = str ""
+let msg x = () ;; let pr_lconstr c = str ""
   (* uncomment this to see debugging *)
-let prconstr c =  msg (str"  " ++ prterm c ++ str"\n")
+let prconstr c =  msg (str"  " ++ pr_lconstr c ++ str"\n")
 let prlistconstr lc = List.iter prconstr lc
 let prstr s = msg(str s)
 
@@ -31,7 +31,7 @@ let prchr () = msg (str" (ret) \n")
 let prNamedConstr s c = 
   begin
     msg(str "");
-    msg(str(s^"==>\n ") ++ prterm c ++ str "\n<==\n");
+    msg(str(s^"==>\n ") ++ pr_lconstr c ++ str "\n<==\n");
     msg(str "");
   end
 
@@ -74,7 +74,7 @@ let  rec mkevarmap_from_listex lex =
 		  let _ = prconstr typ in*)
 		  let info ={
 			 evar_concl = typ;
-			 evar_hyps = empty_named_context;
+			 evar_hyps = empty_named_context_val;
 			 evar_body = Evar_empty} in
 		  Evd.add (mkevarmap_from_listex lex') ex info
 
@@ -126,7 +126,7 @@ let apply_leqtrpl_t t leq =
 
 
 let apply_refl_term eq t =
-  let _,arr = destApplication eq in
+  let _,arr = destApp eq in
   let reli= (Array.get arr 1) in
   let by_t= (Array.get arr 2) in
   substitterm 0 reli by_t t
@@ -144,7 +144,7 @@ let apply_eq_leqtrpl leq eq =
 let constr_head_match u t=
   if isApp u 
   then 
-	 let uhd,args= destApplication u in
+	 let uhd,args= destApp u in
     uhd=t
   else false
 
@@ -187,7 +187,7 @@ let rec buildrefl_from_eqs eqs =
   match eqs with 
     | []  ->  []
     | cstr::eqs' -> 
-        let eq,args = destApplication cstr in
+        let eq,args = destApp cstr in
         (mkRefl (Array.get args 0) (Array.get args 2))
 	:: (buildrefl_from_eqs eqs')
 
@@ -237,7 +237,7 @@ let rec substit_red prof t by_t in_u =
 (* [exchange_reli_arrayi t=(reli x y ...) tarr (d,f)] exchange each
 	reli by tarr.(f-i). *) 
 let exchange_reli_arrayi tarr (d,f) t =
-  let hd,args= destApplication t in 
+  let hd,args= destApp t in 
   let i = destRel hd in
   let res = whd_beta (mkApp (tarr.(f-i) ,args)) in
   res
@@ -269,7 +269,7 @@ let def_of_const t =
 (* nom d'une constante. Must be a constante. x*)
 let name_of_const t =
     match (kind_of_term t) with
-        Const cst -> Names.string_of_label (Names.label cst)
+        Const cst -> Names.string_of_label (Names.con_label cst)
 		|_ -> assert false
  ;;
 
-- 
cgit v1.2.3