Remove dead modules in Subtac.

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

7 files changed, 0 insertions, 214 deletions

diff --git a/contrib/subtac/context.ml b/contrib/subtac/context.ml
deleted file mode 100644
index 236b0ea534..0000000000
--- a/contrib/subtac/context.ml
+++ /dev/null
@@ -1,35 +0,0 @@
-open Term
-open Names
-
-type t = rel_declaration list (* name, optional coq interp, algorithmic type *)
-
-let assoc n t = 
-  let _, term, typ = List.find (fun (x, _, _) -> x = n) t in
-    term, typ
-
-let assoc_and_index x l =
-  let rec aux i = function
-      (y, term, typ) :: tl -> if x = y then i, term, typ else aux (succ i) tl
-    | [] -> raise Not_found
-  in aux 0 l
-
-let id_of_name = function
-    Name id -> id
-  | Anonymous -> raise (Invalid_argument "id_of_name")
-(*
-
-let subst_ctx ctx c = 
-  let rec aux ((ctx, n, c) as acc) = function
-      (name, None, typ) :: tl -> 
-	aux (((id_of_name name, None, rel_to_vars ctx typ) :: ctx), 
-	     pred n, c) tl
-    | (name, Some term, typ) :: tl ->
-	let t' = Term.substnl [term] n c in
-	  aux (ctx, n, t') tl
-    | [] -> acc
-  in 
-  let (x, _, z) = aux ([], pred (List.length ctx), c) (List.rev ctx) in 
-    (x, rel_to_vars x z)
-*)
-
-let subst_env env c = (env, c)
diff --git a/contrib/subtac/context.mli b/contrib/subtac/context.mli
deleted file mode 100644
index 671d6f3619..0000000000
--- a/contrib/subtac/context.mli
+++ /dev/null
@@ -1,5 +0,0 @@
-type t = Term.rel_declaration list
-val assoc : 'a -> ('a * 'b * 'c) list -> 'b * 'c
-val assoc_and_index : 'a -> ('a * 'b * 'c) list -> int * 'b * 'c
-val id_of_name : Names.name -> Names.identifier
-val subst_env : 'a -> 'b -> 'a * 'b
diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml
index 6583586737..e774dd127a 100644
--- a/contrib/subtac/subtac.ml
+++ b/contrib/subtac/subtac.ml
@@ -37,7 +37,6 @@ open Subtac_utils
 open Coqlib
 open Printer
 open Subtac_errors
-open Context
 open Eterm
 
 let require_library dirpath =
diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml
index d0d6dced11..743d239881 100644
--- a/contrib/subtac/subtac_coercion.ml
+++ b/contrib/subtac/subtac_coercion.ml
@@ -26,7 +26,6 @@ open Subtac_utils
 open Coqlib
 open Printer
 open Subtac_errors
-open Context
 open Eterm
 open Pp
 
diff --git a/contrib/subtac/subtac_interp_fixpoint.ml b/contrib/subtac/subtac_interp_fixpoint.ml
deleted file mode 100644
index bb35833f38..0000000000
--- a/contrib/subtac/subtac_interp_fixpoint.ml
+++ /dev/null
@@ -1,154 +0,0 @@
-open Global
-open Pp
-open Util
-open Names
-open Sign
-open Evd
-open Term
-open Termops
-open Reductionops
-open Environ
-open Type_errors
-open Typeops
-open Libnames
-open Classops
-open List
-open Recordops 
-open Evarutil
-open Pretype_errors
-open Rawterm
-open Evarconv
-open Pattern
-open Dyn
-open Topconstr
-
-open Subtac_coercion
-open Subtac_utils
-open Coqlib
-open Printer
-open Subtac_errors
-open Context
-open Eterm
-
-
-let mkAppExplC (f, args) = CAppExpl (dummy_loc, (None, f), args)
-
-let mkSubset name typ prop = 
-  mkAppExplC (sig_ref,
-	      [ typ; mkLambdaC ([name], typ, prop) ])
-	      
-let mkProj1 u p x = 
-  mkAppExplC (proj1_sig_ref, [ u; p; x ])
-
-let mkProj2 u p x = 
-  mkAppExplC (proj2_sig_ref, [ u; p; x ])
-
-let list_of_local_binders l = 
-  let rec aux acc = function
-      Topconstr.LocalRawDef (n, c) :: tl -> aux ((n, c) :: acc) tl
-    | Topconstr.LocalRawAssum (nl, c) :: tl -> 
-	aux (List.fold_left (fun acc n -> (n, c) :: acc) acc nl) tl
-    | [] -> List.rev acc
-  in aux [] l
-       
-let abstract_constr_expr_bl abs c bl =
-  List.fold_right (fun (n, t) c -> abs ([n], t, c)) bl c
-
-let pr_binder_list b = 
-  List.fold_right (fun ((loc, name), t) acc -> Nameops.pr_name name ++ str " : " ++
-		     Ppconstr.pr_constr_expr t ++ spc () ++ acc) b (mt ()) 
-
-
-let rec rewrite_rec_calls l c = c
-(*
-let rewrite_fixpoint env l (f, decl) = 
-  let (id, (n, ro), bl, typ, body) = f in
-  let body = rewrite_rec_calls l body in
-    match ro with
-	CStructRec -> ((id, (n, ro), bl, typ, body), decl)
-      | CWfRec wfrel -> 
-	  let bls = list_of_local_binders bl in
-	  let _ = trace (str "Rewriting fixpoint: " ++ Ppconstr.pr_id id ++ 
-			 Ppconstr.pr_binders bl ++ str " : " ++ 
-			 Ppconstr.pr_constr_expr typ ++ str " := " ++ spc () ++
-			 Ppconstr.pr_constr_expr body)
-	  in
-	  let before, after = list_chop n bls in
-	  let _ = trace (str "Binders before the recursion arg: " ++ spc () ++
-			 pr_binder_list before ++ str "; after the recursion arg: " ++
-			 pr_binder_list after)
-	  in
-	  let ((locn, name) as lnid, ntyp), after = match after with
-	      hd :: tl -> hd, tl
-	    | _ -> assert(false) (* Rec arg must be in after *)
-	  in
-	  let nid = match name with
-	      Name id -> id
-	    | Anonymous -> assert(false) (* Rec arg _must_ be named *)
-	  in
-	  let _wfproof = 
-	    let _wf_rel = mkAppExplC (well_founded_ref, [ntyp; wfrel]) in
-	      (*make_existential_expr dummy_loc before wf_rel*)
-	      mkRefC lt_wf_ref
-	  in
-	  let nid', accproofid = 
-	    let nid = string_of_id nid in
-	      id_of_string (nid ^ "'"), id_of_string ("Acc_" ^ nid)
-	  in
-	  let lnid', laccproofid = (dummy_loc, Name nid'), (dummy_loc, Name accproofid) in
-	  let wf_prop = (mkAppC (wfrel, [ mkIdentC nid'; mkIdentC nid ])) in
-	  let lam_wf_prop = mkLambdaC ([lnid'], ntyp, wf_prop) in
-	  let typnid' = mkSubset lnid' ntyp wf_prop in
-	  let internal_type = 
-	    abstract_constr_expr_bl mkProdC 
-	      (mkProdC ([lnid'], typnid', 
-			mkLetInC (lnid, mkProj1 ntyp lam_wf_prop (mkIdentC nid'), 
-				  abstract_constr_expr_bl mkProdC typ after)))
-	      before
-	  in
-	  let body' =
-	    let body =
-	      (* cast or we will loose some info at pretyping time as body
-		 is a function *)
-	      CCast (dummy_loc, body,  CastConv DEFAULTcast, typ) 
-	    in
-	    let body' = (* body abstracted by rec call *)
-	      mkLambdaC ([(dummy_loc, Name id)], internal_type, body)
-	    in
-	      mkAppC (body',
-		      [mkLambdaC 
-			 ([lnid'], typnid',
-			  mkAppC (mkIdentC id, 
-				  [mkProj1 ntyp lam_wf_prop (mkIdentC nid');
-				   (mkAppExplC (acc_inv_ref,
-						[ ntyp; wfrel;
-						  mkIdentC nid;
-						  mkIdentC accproofid;
-						  mkProj1 ntyp lam_wf_prop (mkIdentC nid');
-						  mkProj2 ntyp lam_wf_prop (mkIdentC nid') ])) ]))])
-	  in
-	  let acctyp = mkAppExplC (acc_ref, [ ntyp; wfrel; mkIdentC nid ]) in
-	  let bl' = 
-	    let rec aux acc = function
-		Topconstr.LocalRawDef _ as x :: tl -> 
-		  aux (x :: acc) tl
-	      | Topconstr.LocalRawAssum (bl, typ) as assum :: tl ->
-		  let rec aux' bl' = function
-		      ((loc, name') as x) :: tl ->
-			if name' = name then
-			  (if tl = [] then [] else [LocalRawAssum (tl, typ)]) @
-			  LocalRawAssum ([(dummy_loc, Name accproofid)], acctyp) ::
-			    [LocalRawAssum (List.rev (x :: bl'), typ)]
-			else aux' (x :: bl') tl
-		    | [] -> [assum]
-		  in aux (aux' [] bl @ acc) tl
-	      | [] -> List.rev acc
-	    in aux [] bl
-	  in
-	  let _ = trace (str "Rewrote fixpoint: " ++ Ppconstr.pr_id id ++ 
-			 Ppconstr.pr_binders bl' ++ str " : " ++ 
-			 Ppconstr.pr_constr_expr typ ++ str " := " ++ spc () ++
-			 Ppconstr.pr_constr_expr body')
-	  in (id, (succ n, ro), bl', typ, body'), decl
-
-*)
diff --git a/contrib/subtac/subtac_interp_fixpoint.mli b/contrib/subtac/subtac_interp_fixpoint.mli
deleted file mode 100644
index 149e758079..0000000000
--- a/contrib/subtac/subtac_interp_fixpoint.mli
+++ /dev/null
@@ -1,17 +0,0 @@
-val mkAppExplC :
-  Libnames.reference * Topconstr.constr_expr list -> Topconstr.constr_expr
-val mkSubset :
-  Names.name Util.located ->
-  Topconstr.constr_expr -> Topconstr.constr_expr -> Topconstr.constr_expr
-val mkProj1 :
-  Topconstr.constr_expr ->
-  Topconstr.constr_expr -> Topconstr.constr_expr -> Topconstr.constr_expr
-val mkProj2 :
-  Topconstr.constr_expr ->
-  Topconstr.constr_expr -> Topconstr.constr_expr -> Topconstr.constr_expr
-val list_of_local_binders :
-  Topconstr.local_binder list ->
-  (Names.name Util.located * Topconstr.constr_expr) list
-val pr_binder_list :
-  (('a * Names.name) * Topconstr.constr_expr) list -> Pp.std_ppcmds
-val rewrite_rec_calls : 'a -> 'b -> 'b
diff --git a/contrib/subtac/subtac_pretyping.ml b/contrib/subtac/subtac_pretyping.ml
index 1b4e2f3870..c6e099ac56 100644
--- a/contrib/subtac/subtac_pretyping.ml
+++ b/contrib/subtac/subtac_pretyping.ml
@@ -36,7 +36,6 @@ open Subtac_utils
 open Coqlib
 open Printer
 open Subtac_errors
-open Context
 open Eterm
 
 module Pretyping = Subtac_pretyping_F.SubtacPretyping_F(Subtac_coercion.Coercion)