Plus de combinateurs sont passés de Util à Option. Le module Options

devient Flags.




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

5 files changed, 23 insertions, 28 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 8bce850dbb..480ca95609 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -230,7 +230,7 @@ let make_resolves env sigma eap c =
   let ents = 
     map_succeed 
       (fun f -> f (c,cty)) 
-      [make_exact_entry; make_apply_entry env sigma (eap,Options.is_verbose())]
+      [make_exact_entry; make_apply_entry env sigma (eap,Flags.is_verbose())]
   in 
   if ents = [] then
     errorlabstrm "Hint" 
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index f34c9e38d9..b43466e312 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -249,7 +249,7 @@ let add_inversion_lemma name env sigma t sort dep inv_op =
        { const_entry_body = invProof;
          const_entry_type = None;
          const_entry_opaque = false;
-	 const_entry_boxed = true && (Options.boxed_definitions())}, 
+	 const_entry_boxed = true && (Flags.boxed_definitions())}, 
      IsProof Lemma)
   in ()
 
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 307968116a..477beba4ab 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -259,7 +259,7 @@ let default_relation_for_carrier ?(filter=fun _ -> true) a =
     [] -> Leibniz (Some a)
   | relation::tl ->
      if tl <> [] then
-      Options.if_warn msg_warning
+      Flags.if_warn msg_warning
        (str "There are several relations on the carrier \"" ++
          pr_lconstr a ++ str "\". The relation " ++ prrelation relation ++
          str " is chosen.") ;
@@ -347,7 +347,7 @@ let (relation_to_obj, obj_to_relation)=
           match th.rel_sym with
              None -> old_relation.rel_sym
            | Some t -> Some t} in
-        Options.if_warn msg_warning 
+        Flags.if_warn msg_warning 
          (strbrk "The relation " ++ prrelation th' ++
           strbrk " is redeclared. The new declaration" ++
            (match th'.rel_refl with
@@ -412,7 +412,7 @@ let morphism_table_add (m,c) =
     List.find
      (function mor -> mor.args = c.args && mor.output = c.output) old
    in
-    Options.if_warn msg_warning
+    Flags.if_warn msg_warning
      (strbrk "The morphism " ++ prmorphism m old_morph ++
       strbrk " is redeclared. " ++
       strbrk "The new declaration whose compatibility is proved by " ++
@@ -427,7 +427,7 @@ let default_morphism ?(filter=fun _ -> true) m =
       [] -> raise Not_found
     | m1::ml ->
         if ml <> [] then
-          Options.if_warn msg_warning
+          Flags.if_warn msg_warning
             (strbrk "There are several morphisms associated to \"" ++
             pr_lconstr m ++ strbrk "\". Morphism " ++ prmorphism m m1 ++
             strbrk " is randomly chosen.");
@@ -689,7 +689,7 @@ let add_morphism lemma_infos mor_name (m,quantifiers_rev,args,output) =
                   apply_to_rels mext quantifiers_rev |]));
           const_entry_type = None;
           const_entry_opaque = false;
-          const_entry_boxed = Options.boxed_definitions()},
+          const_entry_boxed = Flags.boxed_definitions()},
 	IsDefinition Definition)) ;
      mext 
  in
@@ -705,7 +705,7 @@ let add_morphism lemma_infos mor_name (m,quantifiers_rev,args,output) =
         output = output_constr;
         lem = lem;
         morphism_theory = mmor }));
-   Options.if_verbose ppnl (pr_lconstr m ++ str " is registered as a morphism")
+   Flags.if_verbose ppnl (pr_lconstr m ++ str " is registered as a morphism")
 
 let error_cannot_unify_signature env k t t' =
   errorlabstrm "New Morphism"
@@ -923,7 +923,7 @@ let new_morphism m signature id hook =
 	Pfedit.start_proof id (Global, Proof Lemma) 
 	  (Declare.clear_proofs (Global.named_context ()))
 	  lem hook;
-	Options.if_verbose msg (Printer.pr_open_subgoals ());
+	Flags.if_verbose msg (Printer.pr_open_subgoals ());
       end
 
 let morphism_hook _ ref =
@@ -1043,7 +1043,7 @@ let int_add_relation id a aeq refl sym trans =
             a_quantifiers_rev);
        const_entry_type = None;
        const_entry_opaque = false;
-       const_entry_boxed = Options.boxed_definitions()},
+       const_entry_boxed = Flags.boxed_definitions()},
       IsDefinition Definition) in
   let id_precise = id_of_string (string_of_id id ^ "_precise_relation_class") in
   let xreflexive_relation_class =
@@ -1060,14 +1060,14 @@ let int_add_relation id a aeq refl sym trans =
         Sign.it_mkLambda_or_LetIn xreflexive_relation_class a_quantifiers_rev;
        const_entry_type = None;
        const_entry_opaque = false;
-       const_entry_boxed = Options.boxed_definitions() },
+       const_entry_boxed = Flags.boxed_definitions() },
       IsDefinition Definition) in
   let aeq_rel =
    { aeq_rel with
       rel_X_relation_class = current_constant id;
       rel_Xreflexive_relation_class = current_constant id_precise } in
   Lib.add_anonymous_leaf (relation_to_obj (aeq, aeq_rel)) ;
-  Options.if_verbose ppnl (pr_lconstr aeq ++ str " is registered as a relation");
+  Flags.if_verbose ppnl (pr_lconstr aeq ++ str " is registered as a relation");
   match trans with
      None -> ()
    | Some trans ->
@@ -1120,7 +1120,7 @@ let int_add_relation id a aeq refl sym trans =
           {const_entry_body = Sign.it_mkLambda_or_LetIn lemma a_quantifiers_rev;
            const_entry_type = None;
            const_entry_opaque = false;
-          const_entry_boxed = Options.boxed_definitions()},
+          const_entry_boxed = Flags.boxed_definitions()},
           IsDefinition Definition)
       in
        let a_quantifiers_rev =
@@ -1580,7 +1580,7 @@ let mark_occur gl ~new_goals t in_c input_relation input_direction =
           (fun i (_,_,mc) -> pr_new_goals i mc) res)
    | [he] -> he
    | he::_ ->
-      Options.if_warn msg_warning
+      Flags.if_warn msg_warning
        (strbrk "The application of the tactic is subject to one of " ++
         strbrk "the following set of side conditions that the user needs " ++
         strbrk "to prove:" ++
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 09d9fe8d79..3211cc6cf1 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -612,16 +612,11 @@ let rec intern_match_context_hyps sigma env lfun = function
   | (Hyp ((_,na) as locna,mp))::tl ->
       let ido, metas1, pat = intern_pattern sigma env lfun mp in
       let lfun, metas2, hyps = intern_match_context_hyps sigma env lfun tl in
-      let lfun' = name_cons na (option_cons ido lfun) in
+      let lfun' = name_cons na (Option.List.cons ido lfun) in
       lfun', metas1@metas2, Hyp (locna,pat)::hyps
   | [] -> lfun, [], []
 
 (* Utilities *)
-let rec filter_some = function
-  | None :: l -> filter_some l
-  | Some a :: l -> a :: filter_some l
-  | [] -> []
-
 let extract_names lrc =
   List.fold_right 
     (fun ((loc,name),_) l ->
@@ -833,7 +828,7 @@ and intern_tactic_seq ist = function
 
 and intern_tactic_fun ist (var,body) = 
   let (l1,l2) = ist.ltacvars in
-  let lfun' = List.rev_append (filter_some var) l1 in
+  let lfun' = List.rev_append (Option.List.flatten var) l1 in
   (var,intern_tactic { ist with ltacvars = (lfun',l2) } body)
 
 and intern_tacarg strict ist = function
@@ -872,7 +867,7 @@ and intern_match_rule ist = function
       let lfun',metas1,hyps = intern_match_context_hyps sigma env lfun rl in
       let ido,metas2,pat = intern_pattern sigma env lfun mp in
       let metas = list_uniquize (metas1@metas2) in
-      let ist' = { ist with ltacvars = (metas@(option_cons ido lfun'),l2) } in
+      let ist' = { ist with ltacvars = (metas@(Option.List.cons ido lfun'),l2) } in
       Pat (hyps,pat,intern_tactic ist' tc) :: (intern_match_rule ist tl)
   | [] -> []
 
@@ -2635,18 +2630,18 @@ let make_absolute_name (loc,id) =
   kn
 
 let add_tacdef isrec tacl =
-(*  let isrec = if !Options.p1 then isrec else true in*)
+(*  let isrec = if !Flags.p1 then isrec else true in*)
   let rfun = List.map (fun ((loc,id as locid),_) -> (id,make_absolute_name locid)) tacl in
   let ist =
     {(make_empty_glob_sign()) with ltacrecvars = if isrec then rfun else []} in
   let gtacl =
     List.map (fun ((_,id),def) ->
-      (id,Options.with_option strict_check (intern_tactic ist) def))
+      (id,Flags.with_option strict_check (intern_tactic ist) def))
       tacl in
   let id0 = fst (List.hd rfun) in
   let _ = Lib.add_leaf id0 (inMD gtacl) in
   List.iter
-    (fun (id,_) -> Options.if_verbose msgnl (pr_id id ++ str " is defined"))
+    (fun (id,_) -> Flags.if_verbose msgnl (pr_id id ++ str " is defined"))
     rfun
 
 (***************************************************************************)
@@ -2655,7 +2650,7 @@ let add_tacdef isrec tacl =
 let glob_tactic x = intern_tactic (make_empty_glob_sign ()) x
 
 let glob_tactic_env l env x = 
-  Options.with_option strict_check
+  Flags.with_option strict_check
   (intern_tactic
     { ltacvars = (l,[]); ltacrecvars = []; gsigma = Evd.empty; genv = env })
     x
@@ -2674,7 +2669,7 @@ let _ = Auto.set_extern_interp
     interp_tactic {lfun=l;avoid_ids=[];debug=get_debug(); last_loc=dloc})
 let _ = Auto.set_extern_intern_tac 
   (fun l ->
-    Options.with_option strict_check
+    Flags.with_option strict_check
     (intern_tactic {(make_empty_glob_sign()) with ltacvars=(l,[])}))
 let _ = Auto.set_extern_subst_tactic subst_tactic
 let _ = Dhyp.set_extern_interp eval_tactic
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 782f2a4c15..f1f169394b 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1298,7 +1298,7 @@ let unfold_all x gl =
  *)
 
 let check_unused_names names =
-  if names <> [] & Options.is_verbose () then
+  if names <> [] & Flags.is_verbose () then
     let s = if List.tl names = [] then " " else "s " in
     msg_warning 
       (str"Unused introduction pattern" ++ str s ++