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, 25 insertions, 15 deletions

diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml
index ce2ee1e7da..bec24af1be 100644
--- a/contrib/interface/showproof.ml
+++ b/contrib/interface/showproof.ml
@@ -156,16 +156,16 @@ let seq_to_lnhyp sign sign' cl =
 
 let rule_is_complex r =
    match r with
-      Tactic (TacArg (Tacexp t),_) -> true  
-   |  Tactic (TacAtom (_,TacAuto _), _) -> true
-   |  Tactic (TacAtom (_,TacSymmetry _), _) -> true 
+       Nested (Tactic 
+		 (TacArg (Tacexp _)
+		 |TacAtom (_,(TacAuto _|TacSymmetry _))),_) -> true
    |_ -> false
 ;;
 
 let rule_to_ntactic r =
    let rt =
      (match r with
-       Tactic (t,_) -> t
+       Nested(Tactic t,_) -> t
      | Prim (Refine h) -> TacAtom (dummy_loc,TacExact h)
      | _ -> TacAtom (dummy_loc, TacIntroPattern [])) in
    if rule_is_complex r
@@ -234,17 +234,17 @@ let  to_nproof sigma osign pf =
               (List.map (fun x -> (to_nproof_rec sigma sign x).t_proof)
 		 spfl) in
 	  (match r with
-	    Tactic (TacAtom (_, TacAuto _),_) ->
-	      if spfl=[]
-	      then
-	      	{t_info="to_prove";
-	    	  t_goal= {newhyp=[];
-			    t_concl=concl ntree;
-			    t_full_concl=ntree.t_goal.t_full_concl;
-			    t_full_env=ntree.t_goal.t_full_env};
-		  t_proof= Proof (TacAtom (dummy_loc,TacExtend (dummy_loc,"InfoAuto",[])), [ntree])}
-	      else ntree
-	  | _ -> ntree))
+	       Nested(Tactic (TacAtom (_, TacAuto _)),_) ->
+		 if spfl=[]
+		 then
+	      	   {t_info="to_prove";
+	    	    t_goal= {newhyp=[];
+			     t_concl=concl ntree;
+			     t_full_concl=ntree.t_goal.t_full_concl;
+			     t_full_env=ntree.t_goal.t_full_env};
+		    t_proof= Proof (TacAtom (dummy_loc,TacExtend (dummy_loc,"InfoAuto",[])), [ntree])}
+		 else ntree
+	     | _ -> ntree))
       	else
 	  {t_info="to_prove";
 	    t_goal=(seq_to_lnhyp oldsign nsign cl);
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 88a9014eec..292a428739 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1641,6 +1641,15 @@ let rec xlate_vernac =
 	CT_solve (CT_int n, xlate_tactic tac,
 		  if b then CT_dotdot
                   else CT_coerce_NONE_to_DOTDOT_OPT CT_none)
+
+(* MMode *)
+
+    | (VernacDeclProof | VernacReturn | VernacProofInstr _) -> 
+	anomaly "No MMode in CTcoq"
+
+
+(* /MMode *)
+
     | VernacFocus nopt -> CT_focus (xlate_int_opt nopt)
     | VernacUnfocus -> CT_unfocus
     |VernacExtend("Extraction", [f;l]) ->
@@ -1784,6 +1793,7 @@ let rec xlate_vernac =
   | VernacShow ShowExistentials -> CT_show_existentials
   | VernacShow ShowScript -> CT_show_script
   | VernacShow(ShowMatch _) -> xlate_error "TODO: VernacShow(ShowMatch _)"
+  | VernacShow(ShowThesis) -> xlate_error "TODO: VernacShow(ShowThesis _)"
   | VernacGo arg -> CT_go (xlate_locn arg)
   | VernacShow (ExplainProof l) -> CT_explain_proof (nums_to_int_list l)
   | VernacShow (ExplainTree l) ->