Declarative Proof Language: main commit

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

2 files changed, 18 insertions, 9 deletions

diff --git a/contrib/xml/proof2aproof.ml b/contrib/xml/proof2aproof.ml
index 678b650cc8..92cbf6df52 100644
--- a/contrib/xml/proof2aproof.ml
+++ b/contrib/xml/proof2aproof.ml
@@ -63,21 +63,24 @@ let nf_evar sigma ~preserve =
 (* Warning: statuses, goals, prim_rules and tactic_exprs are not unshared! *)
 let rec unshare_proof_tree =
  let module PT = Proof_type in
-  function {PT.open_subgoals = status ; PT.goal = goal ; PT.ref = ref} ->
+  function {PT.open_subgoals = status ; 
+	    PT.goal = goal ; 
+	    PT.ref = ref} ->
    let unshared_ref =
     match ref with
        None -> None
      | Some (rule,pfs) ->
         let unshared_rule =
          match rule with
-            PT.Prim prim -> PT.Prim prim
-          | PT.Change_evars -> PT.Change_evars
-          | PT.Tactic (tactic_expr, pf) ->
-             PT.Tactic (tactic_expr, unshare_proof_tree pf)
-        in
+             PT.Nested (cmpd, pf) ->
+               PT.Nested (cmpd, unshare_proof_tree pf)
+	   | other -> other
+	in
          Some (unshared_rule, List.map unshare_proof_tree pfs)
    in
-    {PT.open_subgoals = status ; PT.goal = goal ; PT.ref = unshared_ref}
+    {PT.open_subgoals = status ; 
+     PT.goal = goal ; 
+     PT.ref = unshared_ref}
 ;;
 
 module ProofTreeHash =
@@ -103,7 +106,7 @@ let extract_open_proof sigma pf =
        {PT.ref=Some(PT.Prim _,_)} as pf ->
         L.prim_extractor proof_extractor vl pf
 	  
-     | {PT.ref=Some(PT.Tactic (_,hidden_proof),spfl)} ->
+     | {PT.ref=Some(PT.Nested (_,hidden_proof),spfl)} ->
 	 let sgl,v = Refiner.frontier hidden_proof in
 	 let flat_proof = v spfl in
          ProofTreeHash.add proof_tree_to_flattened_proof_tree node flat_proof ;
diff --git a/contrib/xml/proofTree2Xml.ml4 b/contrib/xml/proofTree2Xml.ml4
index 578c1ed2f3..d382ef955c 100644
--- a/contrib/xml/proofTree2Xml.ml4
+++ b/contrib/xml/proofTree2Xml.ml4
@@ -141,7 +141,7 @@ Pp.ppnl (Pp.(++) (Pp.str
               (fun i n -> [< i ; (aux n old_hyps) >]) [<>] nodes)
 
      | {PT.goal=goal;
-        PT.ref=Some(PT.Tactic (tactic_expr,hidden_proof),nodes)} ->
+        PT.ref=Some(PT.Nested (PT.Tactic tactic_expr,hidden_proof),nodes)} ->
          (* [hidden_proof] is the proof of the tactic;                     *)
          (* [nodes] are the proof of the subgoals generated by the tactic; *)
          (* [flat_proof] if the proof-tree obtained substituting [nodes]   *)
@@ -194,6 +194,12 @@ Pp.ppnl (Pp.(++) (Pp.str
           (List.fold_left
             (fun i n -> [< i ; (aux n old_hyps) >]) [<>] nodes)
 
+     | {PT.ref=Some((PT.Nested(PT.Proof_instr (_,_),_)|PT.Decl_proof _),nodes)} ->
+         Util.anomaly "Not Implemented" 
+
+     | {PT.ref=Some(PT.Daimon,_)} ->
+         X.xml_empty "Hidden_open_goal" of_attribute
+
      | {PT.ref=None;PT.goal=goal} ->
          X.xml_empty "Open_goal" of_attribute
   in