Abstraction de constr

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@604 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 13 insertions, 23 deletions

diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index af2f73b130..8991286092 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -91,20 +91,11 @@ let ident_of_nvar loc s =
     user_err_loc (loc,"ident_of_nvar", [< 'sTR "Unexpected wildcard" >])
   else (id_of_string s)
 
-(*
-let rctxt_of_ctxt =
-  Array.map
-    (function
-       | VAR id -> RRef (dummy_loc,RVar id)
-       | _ ->
-     error "Astterm: arbitrary substitution of references not yet implemented")
-*)
-
 let ids_of_ctxt ctxt =
   Array.to_list
     (Array.map
-       (function
-	  | VAR id -> id
+       (function c -> match kind_of_term c with
+	  | IsVar id -> id
 	  | _ ->
       error
 	"Astterm: arbitrary substitution of references not yet implemented")
@@ -132,8 +123,8 @@ let dbize_ctxt ctxt =
 
 let dbize_constr_ctxt =
   Array.map
-    (function
-       | VAR id ->
+    (function c -> match kind_of_term c with
+       | IsVar id ->
 	   (* RRef (dummy_loc,RVar (ident_of_nvar loc s)) *)
 	   RRef (dummy_loc, RVar id)
        | _ -> anomaly "Bad ast for local ctxt of a global reference")
@@ -141,7 +132,7 @@ let dbize_constr_ctxt =
 let dbize_rawconstr_ctxt =
   Array.map
     (function
-       | RRef (_, RVar id) -> VAR id
+       | RRef (_, RVar id) -> mkVar id
        | _ -> anomaly "Bad ast for local ctxt of a global reference")
 
 let dbize_global loc = function
@@ -584,8 +575,7 @@ let interp_casted_constr1 sigma env lvar lmeta com typ =
 (* To process patterns, we need a translation from AST to term
    without typing at all. *)
 
-let ctxt_of_ids ids =
-  Array.of_list (List.map (function id -> VAR id) ids)
+let ctxt_of_ids ids = Array.of_list (List.map mkVar ids)
 
 let rec pat_of_ref metas vars = function
   | RConst (sp,ctxt) -> RConst (sp, dbize_rawconstr_ctxt ctxt)
diff --git a/parsing/pattern.ml b/parsing/pattern.ml
index 47c1d5716d..2d989fafc6 100644
--- a/parsing/pattern.ml
+++ b/parsing/pattern.ml
@@ -73,7 +73,7 @@ let head_of_constr_reference c = match kind_of_term c with
 
 
 (* Second part : Given a term with second-order variables in it,
-   represented by Meta's, and possibly applied using XTRA[$SOAPP] to
+   represented by Meta's, and possibly applied using [SOAPP] to
    terms, this function will perform second-order, binding-preserving,
    matching, in the case where the pattern is a pattern in the sense
    of Dale Miller.
diff --git a/parsing/pretty.ml b/parsing/pretty.ml
index a6f4bdb0e6..cbfacf1388 100644
--- a/parsing/pretty.ml
+++ b/parsing/pretty.ml
@@ -437,7 +437,7 @@ let print_opaque_name name =
 	  let cb = Global.lookup_constant sp in
           if is_defined cb then
 	    let typ = constant_type env Evd.empty cst in
-            print_typed_value (constant_value env x, typ)
+            print_typed_value (constant_value env cst, typ)
           else 
 	    anomaly "print_opaque_name"
       | IsMutInd ((sp,_),_) ->
@@ -491,7 +491,7 @@ let fprint_judge {uj_val=trm;uj_type=typ} =
 
 let unfold_head_fconst = 
   let rec unfrec k = match kind_of_term k with
-    | IsConst _ -> constant_value (Global.env ()) k 
+    | IsConst cst -> constant_value (Global.env ()) cst 
     | IsLambda (na,t,b) -> mkLambda (na,t,unfrec b)
     | IsAppL (f,v) -> appvect (unfrec f,v)
     | _ -> k
@@ -526,8 +526,8 @@ let print_extracted_name name =
           let cont = snd(infexecute sigma (sign,fsign) a.body) in 
 	  (match cont with  (* Cradingue *)
              | Inf {_VAL=t;_TYPE=k} -> 
-		 (match whd_betadeltaiota sigma k with
-		    | DOP0 (Sort s) ->
+		 (match kind_of_term (whd_betadeltaiota sigma k) with
+		    | IsSort s ->
 			fprint_var (string_of_id name) {body=t;typ=s})
              | _  -> error "Non informative term")
 	  
diff --git a/parsing/termast.ml b/parsing/termast.ml
index b8a39e37fa..ca948f9ef1 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -70,8 +70,8 @@ let ids_of_rctxt ctxt =
 let ids_of_ctxt ctxt =
   Array.to_list
     (Array.map
-       (function
-	  | VAR id -> id
+       (function c -> match kind_of_term c with
+	  | IsVar id -> id
 	  | _ ->
        error
        "Termast: arbitrary substitution of references not yet implemented")