Réforme de l'interprétation des termes :

- Le parsing se fait maintenant via "constr_expr" au lieu de "Coqast.t"
- "Coqast.t" reste pour l'instant pour le pretty-printing. Un deuxième
  pretty-printer dans ppconstr.ml est basé sur "constr_expr".
- Nouveau répertoire "interp" qui hérite de la partie interprétation qui
  se trouvait avant dans "parsing" (constrintern.ml remplace astterm.ml;
  constrextern.ml est l'équivalent de termast.ml pour le nouveau
  printer; topconstr.ml; contient la définition de "constr_expr";
  modintern.ml remplace astmod.ml)
- Libnames.reference tend à remplacer Libnames.qualid


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

1 files changed, 0 insertions, 119 deletions

diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index 86ec64c76d..34e9a06e78 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -248,122 +248,3 @@ let pr_subgoals_existential sigma = function
       let prest = pr_rec 2 rest in
       v 0 (int(List.length rest+1) ++ str" subgoals" ++ cut () 
 	   ++ pg1 ++ prest ++ fnl ())
-
-(*
-open Ast
-open Termast
-open Tacexpr
-open Rawterm
-
-let ast_of_cvt_bind f = function
-  | (NoDepBinding n,c) -> ope ("BINDING", [(num n); ope ("CONSTR",[(f c)])])
-  | (DepBinding  id,c) -> ope ("BINDING", [nvar id; ope  ("CONSTR",[(f c)])]) 
-  | (AnonymousBinding,c) -> ope ("BINDING", [ope ("CONSTR",[(f c)])])
-
-let rec ast_of_cvt_intro_pattern = function
-  | WildPat   -> ope ("WILDCAR",[])
-  | IdPat id  -> nvar id
-(*  | DisjPat l -> ope ("DISJPATTERN",  (List.map ast_of_cvt_intro_pattern l))*)
-  | ConjPat l -> ope ("CONJPATTERN",  (List.map ast_of_cvt_intro_pattern l))
-*)
-(*
-(* Gives the ast list corresponding to a reduction flag *)
-open RedFlags
-
-let last_of_cvt_flags red =
-  (if (red_set red fBETA) then [ope("Beta",[])]
-   else [])@
-  (let (n_unf,lconst) = red_get_const red in
-   let lqid =
-     List.map
-       (function
-	  | EvalVarRef id -> nvar id
-	  | EvalConstRef kn ->
-	      ast_of_qualid
-                (shortest_qualid_of_global None (ConstRef kn)))
-       lconst in
-   if lqid = [] then []
-   else if n_unf then [ope("Delta",[]);ope("UnfBut",lqid)]
-   else [ope("Delta",[]);ope("Unf",lqid)])@
-  (if (red_set red fIOTA) then [ope("Iota",[])]
-   else [])
-*)
-(*
-(* Gives the ast corresponding to a reduction expression *)
-open Rawterm
-
-let ast_of_cvt_redexp = function
-  | Red _ -> ope ("Red",[])
-  | Hnf -> ope("Hnf",[])
-  | Simpl -> ope("Simpl",[])
-(*
-  | Cbv flg -> ope("Cbv",last_of_cvt_flags flg)
-  | Lazy flg -> ope("Lazy",last_of_cvt_flags flg)
-*)
-  | Unfold l ->
-    ope("Unfold",List.map (fun (locc,sp) -> ope("UNFOLD",
-      [match sp with
-	| EvalVarRef id -> nvar id
-	| EvalConstRef kn -> 					
-	    ast_of_qualid
-	      (shortest_qualid_of_global None (ConstRef kn))]
-      @(List.map num locc))) l)
-  | Fold l ->
-    ope("Fold",List.map (fun c -> ope ("CONSTR",
-      [ast_of_constr false (Global.env ()) c])) l)
-  | Pattern l ->
-    ope("Pattern",List.map (fun (locc,csr) -> ope("PATTERN",
-      [ope ("CONSTR",[ast_of_constr false (Global.env ()) csr])]@
-      (List.map num locc))) l)
-*)
-(* Gives the ast corresponding to a tactic argument *)
-(*
-let ast_of_cvt_arg = function
-  | Identifier id   -> nvar id
-(*
-  | Qualid qid      -> ast_of_qualid qid
-*)
-  | Quoted_string s -> string s
-  | Integer n       -> num n 
-(*  | Command c       -> ope ("CONSTR",[c])*)
-  | Constr  c       -> 
-    ope ("CONSTR",[ast_of_constr false (Global.env ()) c])
-  | OpenConstr  (_,c)       -> 
-    ope ("CONSTR",[ast_of_constr false (Global.env ()) c])
-  | Constr_context _ ->
-    anomalylabstrm "ast_of_cvt_arg" (str
-      "Constr_context argument could not be used")
-  | Clause idl      -> 
-      let transl = function
-	| InHyp id -> ope ("INHYP", [nvar id])
-	| InHypType id -> ope ("INHYPTYPE", [nvar id]) in
-      ope ("CLAUSE", List.map transl idl)
-(*
-  | Bindings bl     -> ope ("BINDINGS", 
-			    List.map (ast_of_cvt_bind (fun x -> x)) bl)
-  | Cbindings bl    -> 
-      ope ("BINDINGS", 
-	   List.map 
-	     (ast_of_cvt_bind
-		(ast_of_constr false (Global.env ()))) bl)
-*)
-(* TODO
-  | Tacexp ast      -> ope ("TACTIC",[ast])
-  | Tac (tac,ast) -> ast
-*)
-  | Redexp red -> ope("REDEXP",[ast_of_cvt_redexp red])
-  | Fixexp (id,n,c) -> ope ("FIXEXP",[nvar id; num n; ope ("CONSTR",[ast_of_constr false (Global.env ()) c])])
-  | Cofixexp (id,c) -> ope ("COFIXEXP",[nvar id; ope ("CONSTR",[ast_of_constr false (Global.env ()) c])])
-(*  | Intropattern p ->  ast_of_cvt_intro_pattern p*)
-  | Letpatterns (gl_occ_opt,hyp_occ_list) ->
-     let hyps_pats =
-       List.map
-	 (fun (id,l) ->
-	    ope ("HYPPATTERN", nvar id :: (List.map num l)))
-	 hyp_occ_list in
-     let all_pats =
-       match gl_occ_opt with
-	 | None -> hyps_pats
-	 | Some l -> hyps_pats @ [ope ("CCLPATTERN", List.map num l)] in
-     ope ("LETPATTERNS", all_pats)
-*)