Imported Upstream version 8.2.pl1+dfsgupstream/8.2.pl1+dfsg

6 files changed, 55 insertions, 31 deletions

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 7bebf6db..ad093507 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -8,7 +8,7 @@
 
 (*i camlp4use: "pa_extend.cmo" i*)
 
-(* $Id: g_tactic.ml4 11741 2009-01-03 14:34:39Z herbelin $ *)
+(* $Id: g_tactic.ml4 12009 2009-03-23 22:55:37Z herbelin $ *)
 
 open Pp
 open Pcoq
@@ -72,15 +72,16 @@ let test_lpar_id_colon =
 let check_for_coloneq =
   Gram.Entry.of_parser "lpar_id_colon"
     (fun strm ->
-      let rec skip_to_rpar n =
+      let rec skip_to_rpar p n =
 	match list_last (Stream.npeek n strm) with
-        | ("",")") -> n+1
+        | ("","(") -> skip_to_rpar (p+1) (n+1)
+        | ("",")") -> if p=0 then n+1 else skip_to_rpar (p-1) (n+1)
 	| ("",".") -> raise Stream.Failure
-	| _ -> skip_to_rpar (n+1) in
+	| _ -> skip_to_rpar p (n+1) in
       let rec skip_names n =
 	match list_last (Stream.npeek n strm) with
         | ("IDENT",_) | ("","_") -> skip_names (n+1)
-	| ("",":") -> skip_to_rpar (n+1) (* skip a constr *)
+	| ("",":") -> skip_to_rpar 0 (n+1) (* skip a constr *)
 	| _ -> raise Stream.Failure in
       let rec skip_binders n =
 	match list_last (Stream.npeek n strm) with
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index f960492e..b2d67e1c 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -9,7 +9,7 @@
 (*i camlp4deps: "parsing/grammar.cma" i*)
 (*i camlp4use: "pa_extend.cmo" i*)
 
-(* $Id: g_vernac.ml4 11809 2009-01-20 11:39:55Z aspiwack $ *)
+(* $Id: g_vernac.ml4 12187 2009-06-13 19:36:59Z msozeau $ *)
 
 
 open Pp
@@ -447,10 +447,13 @@ GEXTEND Gram
 	  CWith_Module (fqid,qid)
       ] ]
   ;
-  module_type:
+  module_type_atom:
     [ [ qid = qualid -> CMTEident qid
-(* ... *)
-      | mty = module_type; me = module_expr_atom -> CMTEapply (mty,me) 
+      | mty = module_type_atom; me = module_expr_atom -> CMTEapply (mty,me) 
+      ] ]
+  ;
+  module_type:
+    [ [ mty = module_type_atom -> mty
       | mty = module_type; "with"; decl = with_declaration -> CMTEwith (mty,decl)
       ] ]
   ;
@@ -700,7 +703,8 @@ GEXTEND Gram
       | IDENT "Visibility"; s = OPT IDENT -> PrintVisibility s
       | IDENT "Implicit"; qid = global -> PrintImplicit qid
       | IDENT "Universes"; fopt = OPT ne_string -> PrintUniverses fopt
-      | IDENT "Assumptions"; qid = global -> PrintAssumptions qid ] ]
+      | IDENT "Assumptions"; qid = global -> PrintAssumptions (false, qid)
+      | IDENT "Opaque"; IDENT "Dependencies"; qid = global -> PrintAssumptions (true, qid) ] ]
   ;
   class_rawexpr:
     [ [ IDENT "Funclass" -> FunClass
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index d0a9c3d8..d2d81cd1 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -8,7 +8,7 @@
 
 (*i camlp4use: "pa_extend.cmo pa_macro.cmo" i*)
 
-(*i $Id: pcoq.ml4 11784 2009-01-14 11:36:32Z herbelin $ i*)
+(*i $Id: pcoq.ml4 12055 2009-04-07 18:19:05Z herbelin $ i*)
 
 open Pp
 open Util
@@ -735,7 +735,10 @@ let is_binder_level from e =
 
 let rec symbol_of_production assoc from forpat typ =
   if is_binder_level from typ then
-    Gramext.Snterml (Gram.Entry.obj Constr.operconstr,"200")
+    if forpat then
+      Gramext.Snterml (Gram.Entry.obj Constr.pattern,"200")
+    else
+      Gramext.Snterml (Gram.Entry.obj Constr.operconstr,"200")
   else if is_self from typ then
     Gramext.Sself
   else
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 78c63ca2..5f4ea5a6 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: ppvernac.ml 11809 2009-01-20 11:39:55Z aspiwack $ *)  
+(* $Id: ppvernac.ml 12187 2009-06-13 19:36:59Z msozeau $ *)  
 
 open Pp
 open Names
@@ -897,7 +897,8 @@ let rec pr_vernac = function
 	| PrintImplicit qid -> str"Print Implicit" ++ spc()  ++ pr_reference qid
 (* spiwack: command printing all the axioms and section variables used in a 
          term *)
-	| PrintAssumptions qid -> str"Print Assumptions"++spc()++pr_reference qid
+	| PrintAssumptions (b,qid) -> (if b then str"Print Assumptions" else str"Print Opaque Dependencies")
+	    ++spc()++pr_reference qid
       in pr_printable p
   | VernacSearch (sea,sea_r) -> pr_search sea sea_r pr_constr_pattern_expr
   | VernacLocate loc -> 
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 5543a31c..1e50bc51 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -10,7 +10,7 @@
  * on May-June 2006 for implementation of abstraction of pretty-printing of objects.
  *)
 
-(* $Id: prettyp.ml 11622 2008-11-23 08:45:56Z herbelin $ *)
+(* $Id: prettyp.ml 12187 2009-06-13 19:36:59Z msozeau $ *)
 
 open Pp
 open Util
@@ -107,8 +107,9 @@ let need_expansion impl ref =
   let typ = Global.type_of_global ref in
   let ctx = fst (decompose_prod_assum typ) in
   let nprods = List.length (List.filter (fun (_,b,_) -> b=None) ctx) in
-  impl <> [] & let _,lastimpl = list_chop nprods impl in
-  List.filter is_status_implicit lastimpl <> []
+  impl <> [] & List.length impl >= nprods &
+    let _,lastimpl = list_chop nprods impl in
+      List.filter is_status_implicit lastimpl <> []
 
 type opacity =
   | FullyOpaque
diff --git a/parsing/printer.ml b/parsing/printer.ml
index 10034dd9..0c673fbd 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: printer.ml 11739 2009-01-02 19:33:19Z herbelin $ *)
+(* $Id: printer.ml 12187 2009-06-13 19:36:59Z msozeau $ *)
 
 open Pp
 open Util
@@ -431,10 +431,11 @@ let pr_prim_rule = function
        (str"cut " ++ pr_constr t ++ 
         str ";[" ++ cl ++ str"intro " ++ pr_id id ++ str"|idtac]")
 	
-  | FixRule (f,n,[]) ->
+  | FixRule (f,n,[],_) ->
       (str"fix " ++ pr_id f ++ str"/" ++ int n)
       
-  | FixRule (f,n,others) -> 
+  | FixRule (f,n,others,j) -> 
+      if j<>0 then warning "Unsupported printing of \"fix\"";
       let rec print_mut = function
 	| (f,n,ar)::oth -> 
            pr_id f ++ str"/" ++ int n ++ str" : " ++ pr_lconstr ar ++ print_mut oth
@@ -442,10 +443,11 @@ let pr_prim_rule = function
       (str"fix " ++ pr_id f ++ str"/" ++ int n ++
          str" with " ++ print_mut others)
 
-  | Cofix (f,[]) ->
+  | Cofix (f,[],_) ->
       (str"cofix " ++ pr_id f)
 
-  | Cofix (f,others) ->
+  | Cofix (f,others,j) ->
+      if j<>0 then warning "Unsupported printing of \"fix\"";
       let rec print_mut = function
 	| (f,ar)::oth ->
 	  (pr_id f ++ str" : " ++ pr_lconstr ar ++ print_mut oth)
@@ -499,10 +501,10 @@ let pr_assumptionset env s =
   if (Environ.ContextObjectMap.is_empty s) then
     str "Closed under the global context"
   else
-    let (vars,axioms) =
-      Environ.ContextObjectMap.fold (fun o typ r ->
-	let (v,a) = r in
-	match o with
+    let (vars,axioms,opaque) =
+      Environ.ContextObjectMap.fold (fun t typ r ->
+	let (v,a,o) = r in
+	match t with
 	| Variable id -> (  Some (
 	                      Option.default (fnl ()) v 
 			   ++ str (string_of_id id)
@@ -511,7 +513,7 @@ let pr_assumptionset env s =
 	                   ++ fnl ()
 			    )
 	                 ,
-	                   a )
+	                   a, o)
 	| Axiom kn    -> ( v ,
 			     Some (
 			      Option.default (fnl ()) a
@@ -520,16 +522,28 @@ let pr_assumptionset env s =
 	                   ++ pr_ltype typ
 	                   ++ fnl ()
 			     )
+			 , o
 			 )
-	)
-	s (None,None)
+	| Opaque kn    -> ( v , a ,
+			     Some (
+			      Option.default (fnl ()) o
+			   ++ (pr_constant env kn)
+	                   ++ str " : "
+	                   ++ pr_ltype typ
+	                   ++ fnl ()
+			     )
+			 )
+      )
+	s (None,None,None)
     in
-    let (vars,axioms) = 
+    let (vars,axioms,opaque) = 
       ( Option.map (fun p -> str "Section Variables:" ++ p) vars ,
-	Option.map (fun p -> str "Axioms:" ++ p) axioms 
+	Option.map (fun p -> str "Axioms:" ++ p) axioms ,
+	Option.map (fun p -> str "Opaque constants:" ++ p) opaque
       )
     in
     (Option.default (mt ()) vars) ++ (Option.default (mt ()) axioms)
+      ++ (Option.default (mt ()) opaque)
 
 let cmap_to_list m = Cmap.fold (fun k v acc -> v :: acc) m []