From 48af8fc25bdad1b8c2f475db67ff574e2311d641 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 6 Sep 2000 12:54:15 +0000
Subject: code mort

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@585 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/astterm.ml | 48 ------------------------------------------------
 1 file changed, 48 deletions(-)

diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index 9065d565c7..3b881b5169 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -604,54 +604,6 @@ let interp_casted_constr1 sigma env lvar lmeta com typ =
   and rtype=fun lst -> retype_list sigma env lst in 
   ise_resolve_casted_gen true sigma env (rtype lvar) (rtype lmeta) typ c;;
 
-(*
-let dbize_fw  sigma env com = dbize FW sigma env com
-
-let raw_fconstr_of_com sigma env com = dbize_fw sigma (unitize_env (context env)) com
-let raw_constr_of_compattern sigma env com = 
-  dbize_cci sigma (unitize_env env) com
-
-let fconstr_of_com1 is_ass sigma env com = 
-  let c = raw_fconstr_of_com sigma env com in
-  try 
-    ise_resolve1 is_ass sigma env c
-  with e -> 
-    Stdpp.raise_with_loc (Ast.loc com) e
- 
-let fconstr_of_com sigma hyps com =
-  fconstr_of_com1 false sigma hyps com 
-
-*)
-(* Typing with Trad, and re-checking with Mach *)
-(* Should be done in two passes by library commands ...
-let fconstruct_type sigma sign com =
-  let c = constr_of_com1 true sigma sign com in 
-  Mach.fexecute_type sigma sign c
-
-let fconstruct sigma sign com =
-  let c = constr_of_com1 false sigma sign com in 
-  Mach.fexecute sigma sign c
-
-let infconstruct_type sigma (sign,fsign) cmd =
-  let c = constr_of_com1 true sigma sign cmd in 
-  Mach.infexecute_type sigma (sign,fsign) c
-
-let infconstruct sigma (sign,fsign) cmd =
-  let c = constr_of_com1 false sigma sign cmd in 
-  Mach.infexecute sigma (sign,fsign) c
-
-(* Type-checks a term with the current universe constraints, the resulting
-   constraints are dropped. *)
-
-let univ_sp = make_path ["univ"] (id_of_string "dummy") OBJ
-
-let fconstruct_with_univ sigma sign com =
-  let c = constr_of_com sigma sign com in
-  let (_,j) = with_universes (Mach.fexecute sigma sign)
-		(univ_sp, Constraintab.current_constraints(), c) in 
-  j
-*)
-
 (* To process patterns, we need a translation from AST to term
    without typing at all. *)
 
-- 
cgit v1.2.3