diff options
| author |  aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-12-06 17:36:14 +0000 |
|---|---|---|
| committer | aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-12-06 17:36:14 +0000 |
| commit | a59b644de4234fb7fe3fce28284979091f257130 (patch) | |
| tree | d5d8ff609aa9e4e582a06ca865a94eee1edbf182 /pretyping | |
| parent | 3e3fa18a066feae44c10fc6e072059f4e9914656 (diff) | |
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
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/classops.ml | 2 | ||||
| -rw-r--r-- | pretyping/coercion.ml | 2 | ||||
| -rw-r--r-- | pretyping/detyping.ml | 8 | ||||
| -rw-r--r-- | pretyping/indrec.ml | 2 | ||||
| -rw-r--r-- | pretyping/pattern.ml | 2 | ||||
| -rw-r--r-- | pretyping/tacred.ml | 4 |
6 files changed, 10 insertions, 10 deletions
diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 9a628b3fd..5b0c2eb36 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -10,7 +10,7 @@ open Util open Pp -open Options +open Flags open Names open Libnames open Nametab diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index f3468bcbf..729bd84f1 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -262,7 +262,7 @@ module Default = struct (* a little more effort to get products is needed *) try decompose_prod_n nabs t with _ -> - if !Options.debug then + if !Flags.debug then msg_warning (str "decompose_prod_n failed"); raise (Invalid_argument "Coercion.inh_conv_coerces_to") in diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 9dfe393be..2cfa7076a 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -108,7 +108,7 @@ module PrintingCasesLet = module PrintingIf = Goptions.MakeRefTable(PrintingCasesIf) module PrintingLet = Goptions.MakeRefTable(PrintingCasesLet) -(* Options for printing or not wildcard and synthetisable types *) +(* Flags.for printing or not wildcard and synthetisable types *) open Goptions @@ -299,7 +299,7 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl = let synth_type = synthetize_type () in let tomatch = detype c in let alias, aliastyp, pred= - if (not !Options.raw_print) & synth_type & computable & Array.length bl<>0 + if (not !Flags.raw_print) & synth_type & computable & Array.length bl<>0 then Anonymous, None, None else @@ -319,7 +319,7 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl = let eqnl = detype_eqns constructs consnargsl bl in let tag = try - if !Options.raw_print then + if !Flags.raw_print then RegularStyle else if PrintingLet.active (indsp,consnargsl) then LetStyle @@ -471,7 +471,7 @@ and share_names isgoal n l avoid env c t = and detype_eqns isgoal avoid env ci computable constructs consnargsl bl = try - if !Options.raw_print or not (reverse_matching ()) then raise Exit; + if !Flags.raw_print or not (reverse_matching ()) then raise Exit; let mat = build_tree Anonymous isgoal (avoid,env) ci bl in List.map (fun (pat,((avoid,env),c)) -> (dl,[],[pat],detype isgoal avoid env c)) mat diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 84f35241a..b894a9aae 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -157,7 +157,7 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs = (match dest_recarg ra with | Mrec j when is_rec -> (depPvect.(j),rest) | Imbr _ -> - Options.if_verbose warning "Ignoring recursive call"; + Flags.if_verbose warning "Ignoring recursive call"; (None,rest) | _ -> (None, rest)) in diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index d64e84fea..63dfbb2d9 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -234,7 +234,7 @@ let rec pat_of_raw metas vars = function | RHole _ -> PMeta None | RCast (_,c,_) -> - Options.if_verbose + Flags.if_verbose Pp.warning "Cast not taken into account in constr pattern"; pat_of_raw metas vars c | RIf (_,c,(_,None),b1,b2) -> diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index c4c9894cb..60664f199 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -755,11 +755,11 @@ let rec substlin env name n ol c = (n2,ol2,mkCast (c1',k,c2'))) | Fix _ -> - (Options.if_verbose + (Flags.if_verbose warning "do not consider occurrences inside fixpoints"; (n,ol,c)) | CoFix _ -> - (Options.if_verbose + (Flags.if_verbose warning "do not consider occurrences inside cofixpoints"; (n,ol,c)) | (Rel _|Meta _|Var _|Sort _ |