Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg

9 files changed, 151 insertions, 76 deletions

diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml
index bd335d30..9f3e412a 100644
--- a/contrib/funind/functional_principles_proofs.ml
+++ b/contrib/funind/functional_principles_proofs.ml
@@ -136,7 +136,7 @@ let change_hyp_with_using msg hyp_id t tac : tactic =
   fun g -> 
     let prov_id = pf_get_new_id hyp_id g in 
     tclTHENS
-      ((* observe_tac msg *) (forward (Some  (tclCOMPLETE tac)) (dummy_loc,Genarg.IntroIdentifier prov_id) t))
+      ((* observe_tac msg *) (assert_by (Name prov_id) t (tclCOMPLETE tac)))
       [tclTHENLIST 
       [	
 	(* observe_tac "change_hyp_with_using thin" *) (thin [hyp_id]);
@@ -388,7 +388,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
 		     in
 (* 		     observe_tac "rec hyp " *)
 		       (tclTHENS
-		       (assert_as true (dummy_loc, Genarg.IntroIdentifier rec_pte_id) t_x)
+		       (assert_tac (Name rec_pte_id) t_x)
 		       [
 			 (* observe_tac "prove rec hyp" *) (prove_rec_hyp eq_hyps);
 (* 			observe_tac "prove rec hyp" *)
@@ -571,7 +571,7 @@ let instanciate_hyps_with_args (do_prove:identifier list -> tactic) hyps args_id
 	fun g -> 
 	  let prov_hid = pf_get_new_id hid g in
 	  tclTHENLIST[
-	    forward None (dummy_loc,Genarg.IntroIdentifier prov_hid) (mkApp(mkVar hid,args));
+	    pose_proof (Name prov_hid) (mkApp(mkVar hid,args));
 	    thin [hid];
 	    h_rename [prov_hid,hid]
 	  ] g
@@ -1347,7 +1347,7 @@ let build_clause eqs =
   {
     Tacexpr.onhyps = 
       Some (List.map 
-	      (fun id -> (Rawterm.all_occurrences_expr,id),Tacexpr.InHyp)
+	      (fun id -> (Rawterm.all_occurrences_expr,id),InHyp)
 	      eqs
 	   );
     Tacexpr.concl_occs = Rawterm.no_occurrences_expr 
@@ -1399,7 +1399,7 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic =
 				      false
 				      (true,5)
 				      [Lazy.force refl_equal]
-				      [Auto.Hint_db.empty false]
+				      [Auto.Hint_db.empty empty_transparent_state false]
 				  )
 			   )
 			)
@@ -1495,10 +1495,9 @@ let prove_principle_for_gen
       ((* observe_tac "prove_rec_arg_acc"  *)
 	 (tclCOMPLETE
 	    (tclTHEN
-	       (forward 
-		  (Some ((fun g -> (* observe_tac "prove wf" *) (tclCOMPLETE (wf_tac is_mes)) g)))
-		  (dummy_loc,Genarg.IntroIdentifier wf_thm_id)
-		  (mkApp (delayed_force well_founded,[|input_type;relation|])))
+	       (assert_by (Name wf_thm_id)  
+		  (mkApp (delayed_force well_founded,[|input_type;relation|]))
+		  (fun g -> (* observe_tac "prove wf" *) (tclCOMPLETE (wf_tac is_mes)) g))
 	       (
 		 (* observe_tac  *)
 (* 		   "apply wf_thm"  *)
@@ -1559,10 +1558,10 @@ let prove_principle_for_gen
 	(List.rev_map (fun (na,_,_) -> Nameops.out_name na) 
 	   (princ_info.args@princ_info.branches@princ_info.predicates@princ_info.params)
 	);
-      (* observe_tac "" *) (forward
-	 (Some (prove_rec_arg_acc))
-	 (dummy_loc,Genarg.IntroIdentifier acc_rec_arg_id)
+      (* observe_tac "" *) (assert_by
+	 (Name acc_rec_arg_id)
  	 (mkApp (delayed_force acc_rel,[|input_type;relation;mkVar rec_arg_id|]))
+	 (prove_rec_arg_acc)
       );
 (*       observe_tac "reverting" *) (revert (List.rev (acc_rec_arg_id::args_ids)));
 (*       (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl () ++  *)
diff --git a/contrib/funind/functional_principles_types.ml b/contrib/funind/functional_principles_types.ml
index 16076479..b03bdf31 100644
--- a/contrib/funind/functional_principles_types.ml
+++ b/contrib/funind/functional_principles_types.ml
@@ -552,13 +552,31 @@ let make_scheme (fas : (constant*Rawterm.rawsort) list) : Entries.definition_ent
       | _ -> anomaly ""
   in
   let (_,(const,_,_)) = 
-    build_functional_principle false
-      first_type
-      (Array.of_list sorts)
-      this_block_funs
-      0
-      (prove_princ_for_struct false 0 (Array.of_list funs))
-      (fun _ _ _ -> ())
+    try
+      build_functional_principle false
+	first_type
+	(Array.of_list sorts)
+	this_block_funs
+	0
+	(prove_princ_for_struct false 0 (Array.of_list funs))
+	(fun _ _ _ -> ())
+  with e -> 
+    begin
+      begin 
+	try 
+	  let id = Pfedit.get_current_proof_name () in 
+	  let s = string_of_id id in 
+	  let n = String.length "___________princ_________" in
+	  if String.length s >= n 
+	  then if String.sub s 0 n = "___________princ_________" 
+	  then Pfedit.delete_current_proof ()
+	  else ()
+	  else ()
+	with _ -> ()
+      end;
+      raise (Defining_principle e)
+    end
+
   in      
   incr i;
   let opacity = 
diff --git a/contrib/funind/g_indfun.ml4 b/contrib/funind/g_indfun.ml4
index d435f513..a79b46d9 100644
--- a/contrib/funind/g_indfun.ml4
+++ b/contrib/funind/g_indfun.ml4
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 (*i camlp4deps: "parsing/grammar.cma" i*)
+open Util
 open Term
 open Names
 open Pp
@@ -128,25 +129,52 @@ ARGUMENT EXTEND auto_using'
 | [ ] -> [ [] ]
 END
 
+let pr_rec_annotation2_aux s r id l =
+  str ("{"^s^" ") ++ Ppconstr.pr_constr_expr r ++ 
+    Util.pr_opt Nameops.pr_id id ++ 
+    Pptactic.pr_auto_using Ppconstr.pr_constr_expr l ++ str "}"
+
+let pr_rec_annotation2 = function
+  | Struct id -> str "{struct" ++ Nameops.pr_id id ++ str "}"
+  | Wf(r,id,l) -> pr_rec_annotation2_aux "wf" r id l
+  | Mes(r,id,l) -> pr_rec_annotation2_aux "measure" r id l
+
 VERNAC ARGUMENT EXTEND rec_annotation2
+PRINTED BY pr_rec_annotation2
   [ "{"  "struct" ident(id)  "}"] -> [ Struct id ]
 | [ "{" "wf" constr(r) ident_opt(id) auto_using'(l) "}" ] -> [ Wf(r,id,l) ]
 | [ "{" "measure" constr(r) ident_opt(id) auto_using'(l) "}" ] -> [ Mes(r,id,l) ] 
 END
 
+let pr_binder2 (idl,c) =
+  str "(" ++ Util.prlist_with_sep spc Nameops.pr_id idl ++ spc () ++ 
+    str ": " ++ Ppconstr.pr_lconstr_expr c ++ str ")"
 
 VERNAC ARGUMENT EXTEND binder2
-    [ "(" ne_ident_list(idl) ":" lconstr(c)  ")"] ->
-     [
-       LocalRawAssum (List.map (fun id -> (Util.dummy_loc,Name id)) idl,Topconstr.default_binder_kind,c) ]
+PRINTED BY pr_binder2
+    [ "(" ne_ident_list(idl) ":" lconstr(c)  ")"] -> [ (idl,c) ]
 END
 
+let make_binder2 (idl,c) =
+  LocalRawAssum (List.map (fun id -> (Util.dummy_loc,Name id)) idl,Topconstr.default_binder_kind,c)
+
+let pr_rec_definition2 (id,bl,annot,type_,def) =
+  Nameops.pr_id id ++ spc () ++ Util.prlist_with_sep spc pr_binder2 bl ++ 
+    Util.pr_opt pr_rec_annotation2 annot ++ spc () ++ str ":" ++ spc () ++
+    Ppconstr.pr_lconstr_expr type_ ++ str " :=" ++ spc () ++ 
+    Ppconstr.pr_lconstr_expr def
 
 VERNAC ARGUMENT EXTEND rec_definition2
- [ ident(id)  binder2_list( bl)
-     rec_annotation2_opt(annot) ":" lconstr( type_)
+PRINTED BY pr_rec_definition2
+ [ ident(id)  binder2_list(bl)
+     rec_annotation2_opt(annot) ":" lconstr(type_)
 	":=" lconstr(def)] ->
-    [let names = List.map snd (Topconstr.names_of_local_assums bl) in
+    [ (id,bl,annot,type_,def) ]
+END
+
+let make_rec_definitions2 (id,bl,annot,type_,def) =
+     let bl = List.map make_binder2 bl in
+     let names = List.map snd (Topconstr.names_of_local_assums bl) in
      let check_one_name () =
        if List.length names > 1 then
          Util.user_err_loc
@@ -173,52 +201,73 @@ VERNAC ARGUMENT EXTEND rec_definition2
 	 | Some an ->
 	     check_exists_args an
      in
-     ((Util.dummy_loc,id), ni, bl, type_, def) ]
-      END
-
-
-VERNAC ARGUMENT EXTEND rec_definitions2
-| [ rec_definition2(rd) ] -> [ [rd] ]
-| [ rec_definition2(hd) "with" rec_definitions2(tl) ] -> [ hd::tl ]
-END
+     ((Util.dummy_loc,id), ni, bl, type_, def)
 
 
 VERNAC COMMAND EXTEND Function
-   ["Function" rec_definitions2(recsl)] ->
+   ["Function" ne_rec_definition2_list_sep(recsl,"with")] ->
 	[ 
-	  do_generate_principle false  recsl; 
+	  do_generate_principle false (List.map make_rec_definitions2 recsl); 
 	  
 	]
 END
 
+let pr_fun_scheme_arg (princ_name,fun_name,s) = 
+  Nameops.pr_id princ_name ++ str " :=" ++ spc() ++ str "Induction for " ++ 
+  Libnames.pr_reference fun_name ++ spc() ++ str "Sort " ++ 
+  Ppconstr.pr_rawsort s
 
 VERNAC ARGUMENT EXTEND fun_scheme_arg
+PRINTED BY pr_fun_scheme_arg
 | [ ident(princ_name) ":=" "Induction" "for" reference(fun_name) "Sort" sort(s) ] -> [ (princ_name,fun_name,s) ] 
 END 
 
-VERNAC ARGUMENT EXTEND fun_scheme_args
-| [ fun_scheme_arg(fa) ] -> [ [fa] ] 
-| [ fun_scheme_arg(fa) "with" fun_scheme_args(fas) ] -> [fa::fas]
-END 
+
+let warning_error names e = 
+  match e with 
+    | Building_graph e -> 
+	Pp.msg_warning 
+	  (str "Cannot define graph(s) for " ++ 
+	     h 1 (prlist_with_sep (fun _ -> str","++spc ()) Libnames.pr_reference names) ++
+	     if do_observe () then (spc () ++ Cerrors.explain_exn e) else mt ())
+    | Defining_principle e -> 
+	Pp.msg_warning
+	  (str "Cannot define principle(s) for "++ 
+	     h 1 (prlist_with_sep (fun _ -> str","++spc ()) Libnames.pr_reference names) ++
+	     if do_observe () then Cerrors.explain_exn e else mt ())
+    | _ -> anomaly ""
+
 
 VERNAC COMMAND EXTEND NewFunctionalScheme
-   ["Functional" "Scheme" fun_scheme_args(fas) ] ->
+   ["Functional" "Scheme" ne_fun_scheme_arg_list_sep(fas,"with") ] ->
     [
-      try 
-	Functional_principles_types.build_scheme fas
-      with Functional_principles_types.No_graph_found -> 
-	match fas with 
-	  | (_,fun_name,_)::_ -> 
-	      begin
-		begin
-		    make_graph (Nametab.global fun_name)
-		end
-		;
-		try Functional_principles_types.build_scheme fas
-		with Functional_principles_types.No_graph_found -> 
-		  Util.error ("Cannot generate induction principle(s)")
-	      end
-	  | _ -> assert false (* we can only have non empty  list *)
+      begin
+	try 
+	  Functional_principles_types.build_scheme fas
+	with Functional_principles_types.No_graph_found -> 
+	  begin
+	    match fas with 
+	      | (_,fun_name,_)::_ -> 
+		  begin
+		    begin
+		      make_graph (Nametab.global fun_name)
+		    end
+		    ;
+		    try Functional_principles_types.build_scheme fas
+		    with Functional_principles_types.No_graph_found -> 
+		      Util.error ("Cannot generate induction principle(s)")
+    		      | e -> 
+			  let names = List.map (fun (_,na,_) -> na) fas in 
+			  warning_error names e
+			    
+		  end
+	      | _ -> assert false (* we can only have non empty  list *)
+	  end
+    	  | e -> 
+	      let names = List.map (fun (_,na,_) -> na) fas in 
+	      warning_error names e
+
+      end
     ]
 END
 (***** debug only ***)
@@ -307,9 +356,9 @@ let mkEq typ c1 c2 =
 let poseq_unsafe idunsafe cstr gl =
   let typ = Tacmach.pf_type_of gl cstr in
   tclTHEN
-    (Tactics.letin_tac None (Name idunsafe) cstr allClauses)
+    (Tactics.letin_tac None (Name idunsafe) cstr None allClauses)
     (tclTHENFIRST 
-      (Tactics.assert_as true (Util.dummy_loc,IntroAnonymous) (mkEq typ (mkVar idunsafe) cstr)) 
+      (Tactics.assert_tac Anonymous (mkEq typ (mkVar idunsafe) cstr)) 
       Tactics.reflexivity)
     gl
   
diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index 79ef0097..b6b2cbd1 100644
--- a/contrib/funind/indfun.ml
+++ b/contrib/funind/indfun.ml
@@ -168,7 +168,7 @@ let build_newrecursive
 	  if Impargs.is_implicit_args()
 	  then Impargs.compute_implicits  env0 arity
 	  else [] in
-	let impls' =(recname,([],impl,Notation.compute_arguments_scope arity))::impls in
+	let impls' =(recname,(Constrintern.Recursive,[],impl,Notation.compute_arguments_scope arity))::impls in
         (Environ.push_named (recname,None,arity) env, impls'))
       (env0,[]) lnameargsardef in
   let recdef =
@@ -612,7 +612,9 @@ let rec add_args id new_args b =
       CCast(loc,add_args id new_args b1,CastConv(ck,add_args id new_args b2))
   | CCast(loc,b1,CastCoerce) ->
       CCast(loc,add_args id new_args b1,CastCoerce)
+  | CRecord _ -> anomaly "add_args : CRecord"
   | CNotation _ -> anomaly "add_args : CNotation"
+  | CGeneralization _ -> anomaly "add_args : CGeneralization"
   | CPrim _ -> b
   | CDelimiters _ -> anomaly "add_args : CDelimiters"
   | CDynamic _ -> anomaly "add_args : CDynamic"
diff --git a/contrib/funind/indfun_common.ml b/contrib/funind/indfun_common.ml
index 4010b49d..a3c169b7 100644
--- a/contrib/funind/indfun_common.ml
+++ b/contrib/funind/indfun_common.ml
@@ -238,20 +238,19 @@ let with_full_print f a =
   and old_strict_implicit_args =  Impargs.is_strict_implicit_args ()
   and old_contextual_implicit_args = Impargs.is_contextual_implicit_args () in
   let old_rawprint = !Flags.raw_print in 
-  let old_dump = !Flags.dump in 
   Flags.raw_print := true;
   Impargs.make_implicit_args false;
   Impargs.make_strict_implicit_args false;
   Impargs.make_contextual_implicit_args false;
   Impargs.make_contextual_implicit_args false;
-  Flags.dump := false;
+  Dumpglob.pause ();
   try 
     let res = f a in 
     Impargs.make_implicit_args old_implicit_args;
     Impargs.make_strict_implicit_args old_strict_implicit_args;
     Impargs.make_contextual_implicit_args old_contextual_implicit_args;
     Flags.raw_print := old_rawprint;
-    Flags.dump := old_dump;
+    Dumpglob.continue ();
     res
   with  
     | e -> 
@@ -259,7 +258,7 @@ let with_full_print f a =
 	Impargs.make_strict_implicit_args old_strict_implicit_args;
 	Impargs.make_contextual_implicit_args old_contextual_implicit_args;
 	Flags.raw_print := old_rawprint;
-	Flags.dump := old_dump;
+	Dumpglob.continue ();
 	raise e
 
 
diff --git a/contrib/funind/invfun.ml b/contrib/funind/invfun.ml
index f62d70ab..5c8f0871 100644
--- a/contrib/funind/invfun.ml
+++ b/contrib/funind/invfun.ml
@@ -445,10 +445,10 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
     in
     tclTHENSEQ
       [ observe_tac "intro args_names" (tclMAP h_intro args_names);
-	observe_tac "principle" (forward
-	  (Some (h_exact f_principle))
-	  (dummy_loc,Genarg.IntroIdentifier principle_id)
-	  princ_type);
+	observe_tac "principle" (assert_by
+	  (Name principle_id)
+	  princ_type
+	  (h_exact f_principle));
 	tclTHEN_i
 	  (observe_tac "functional_induction" (
 	     fun g -> 
diff --git a/contrib/funind/merge.ml b/contrib/funind/merge.ml
index ec456aae..9bbd165d 100644
--- a/contrib/funind/merge.ml
+++ b/contrib/funind/merge.ml
@@ -855,7 +855,7 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) =
     [rawlist], named ident.
     FIXME: params et cstr_expr (arity) *)
 let rawterm_list_to_inductive_expr prms1 prms2 mib1 mib2 shift
-    (rawlist:(identifier * rawconstr) list):inductive_expr =
+    (rawlist:(identifier * rawconstr) list) =
   let lident = dummy_loc, shift.ident in
   let bindlist , cstr_expr = (* params , arities *)
     merge_rec_params_and_arity prms1 prms2 shift mkSet in
@@ -863,7 +863,7 @@ let rawterm_list_to_inductive_expr prms1 prms2 mib1 mib2 shift
     List.map (* zeta_normalize t ? *)
       (fun (id,t) -> false, ((dummy_loc,id),rawterm_to_constr_expr t))
       rawlist in  
-  lident , bindlist , cstr_expr , lcstor_expr
+  lident , bindlist , Some cstr_expr , lcstor_expr
 
 
 
diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml
index 08a97fd2..09b7fbdf 100644
--- a/contrib/funind/rawterm_to_relation.ml
+++ b/contrib/funind/rawterm_to_relation.ml
@@ -1192,7 +1192,7 @@ let do_build_inductive
   let rel_ind i ext_rel_constructors = 
     ((dummy_loc,relnames.(i)),
     rel_params,
-    rel_arities.(i),
+    Some rel_arities.(i),
     ext_rel_constructors),None
   in
   let ext_rel_constructors = (Array.mapi rel_ind ext_rels_constructors) in 
@@ -1224,9 +1224,14 @@ let do_build_inductive
     | UserError(s,msg) as e ->
 	let _time3 = System.get_time () in
 (* 	Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *)
+	let repacked_rel_inds = 
+	  List.map  (fun ((a , b , c , l),ntn) -> ((false,a) , b, c , Vernacexpr.Inductive_kw, Vernacexpr.Constructors l),ntn )
+	                  rel_inds
+	in
 	let msg = 		     
 	  str "while trying to define"++ spc () ++
-	    Ppvernac.pr_vernac (Vernacexpr.VernacInductive(true,rel_inds)) ++ fnl () ++
+	    Ppvernac.pr_vernac (Vernacexpr.VernacInductive(Decl_kinds.Finite,repacked_rel_inds))
+	    ++ fnl () ++
 	    msg
 	in
 	observe (msg);
@@ -1234,9 +1239,14 @@ let do_build_inductive
     | e -> 
 	let _time3 = System.get_time () in
 (* 	Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *)
+	let repacked_rel_inds = 
+	  List.map  (fun ((a , b , c , l),ntn) -> ((false,a) , b, c , Vernacexpr.Inductive_kw, Vernacexpr.Constructors l),ntn )
+	                  rel_inds
+	in
 	let msg = 		     
 	  str "while trying to define"++ spc () ++
-	    Ppvernac.pr_vernac (Vernacexpr.VernacInductive(true,rel_inds)) ++ fnl () ++
+	    Ppvernac.pr_vernac (Vernacexpr.VernacInductive(Decl_kinds.Finite,repacked_rel_inds)) 
+	    ++ fnl () ++
 	    Cerrors.explain_exn e
 	in
  	observe msg;
diff --git a/contrib/funind/recdef.ml b/contrib/funind/recdef.ml
index 5bd7a6b2..6dc0d5bf 100644
--- a/contrib/funind/recdef.ml
+++ b/contrib/funind/recdef.ml
@@ -8,7 +8,7 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(* $Id: recdef.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: recdef.ml 11671 2008-12-12 12:43:03Z herbelin $ *)
 
 open Term
 open Termops
@@ -740,7 +740,6 @@ let termination_proof_header is_mes input_type ids args_id relation
 	   (observe_tac 
 	      "first assert" 
 	      (assert_tac 
-		 true (* the assert thm is in first subgoal *)
 		 (Name wf_rec_arg) 
 		 (mkApp (delayed_force acc_rel,
 			 [|input_type;relation;mkVar rec_arg_id|])
@@ -753,7 +752,6 @@ let termination_proof_header is_mes input_type ids args_id relation
 	       (observe_tac 
 		  "second assert" 
 		  (assert_tac 
-		     true 
 		     (Name wf_thm)
 		     (mkApp (delayed_force well_founded,[|input_type;relation|]))
 		  )
@@ -1157,12 +1155,12 @@ let rec introduce_all_values_eq cont_tac functional termine
       [] ->
        let heq2 = next_global_ident_away true heq_id ids in
 	tclTHENLIST
-	  [forward None (dummy_loc,IntroIdentifier heq2)
+	  [pose_proof (Name heq2)
              (mkApp(mkVar heq1, [|f_S(f_S(mkVar pmax))|]));
            simpl_iter (onHyp heq2);
            unfold_in_hyp [((true,[1]), evaluable_of_global_reference 
                              (global_of_constr functional))]
-             ((all_occurrences_expr, heq2), Tacexpr.InHyp);
+             ((all_occurrences_expr, heq2), InHyp);
            tclTHENS
 	     (fun gls -> 
 		let t_eq = compute_renamed_type gls (mkVar heq2) in