diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/base_include | 4 | ||||
| -rw-r--r-- | dev/doc/changes.txt | 56 | ||||
| -rw-r--r-- | dev/printers.mllib | 6 | ||||
| -rw-r--r-- | dev/top_printers.ml | 8 |
4 files changed, 65 insertions, 9 deletions
diff --git a/dev/base_include b/dev/base_include index 86f34b2ac9..b09b6df2de 100644 --- a/dev/base_include +++ b/dev/base_include @@ -66,7 +66,7 @@ open Univ open Inductive open Indtypes open Cooking -open Closure +open CClosure open Reduction open Safe_typing open Declare @@ -170,7 +170,7 @@ open Tacticals open Tactics open Eqschemes -open Cerrors +open ExplainErr open Class open Command open Indschemes diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index f7c8fbb304..3cd371bfdc 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -2,6 +2,62 @@ = CHANGES BETWEEN COQ V8.5 AND COQ V8.6 = ========================================= +** Files ** + +To avoid clashes with OCaml's compiler libs, the following files were renamed: +kernel/closure.ml{,i} -> kernel/cClosure.ml{,i} +lib/errors.ml{,i} -> lib/cErrors.ml{,i} +toplevel/cerror.ml{,i} -> toplevel/explainErr.mli{,i} + +** Reduction functions ** + +In closure.ml, we introduced the more precise reduction flags fMATCH, fFIX, +fCOFIX. + +We renamed the following functions: + +Closure.betadeltaiota -> Closure.all +Closure.betadeltaiotanolet -> Closure.allnolet +Reductionops.beta -> Closure.beta +Reductionops.zeta -> Closure.zeta +Reductionops.betaiota -> Closure.betaiota +Reductionops.betaiotazeta -> Closure.betaiotazeta +Reductionops.delta -> Closure.delta +Reductionops.betalet -> Closure.betazeta +Reductionops.betadelta -> Closure.betadeltazeta +Reductionops.betadeltaiota -> Closure.all +Reductionops.betadeltaiotanolet -> Closure.allnolet +Closure.no_red -> Closure.nored +Reductionops.nored -> Closure.nored +Reductionops.nf_betadeltaiota -> Reductionops.nf_all +Reductionops.whd_betadelta -> Reductionops.whd_betadeltazeta +Reductionops.whd_betadeltaiota -> Reductionops.whd_all +Reductionops.whd_betadeltaiota_nolet -> Reductionops.whd_allnolet +Reductionops.whd_betadelta_stack -> Reductionops.whd_betadeltazeta_stack +Reductionops.whd_betadeltaiota_stack -> Reductionops.whd_all_stack +Reductionops.whd_betadeltaiota_nolet_stack -> Reductionops.whd_allnolet_stack +Reductionops.whd_betadelta_state -> Reductionops.whd_betadeltazeta_state +Reductionops.whd_betadeltaiota_state -> Reductionops.whd_all_state +Reductionops.whd_betadeltaiota_nolet_state -> Reductionops.whd_allnolet_state +Reductionops.whd_eta -> Reductionops.shrink_eta +Tacmach.pf_whd_betadeltaiota -> Tacmach.pf_whd_all +Tacmach.New.pf_whd_betadeltaiota -> Tacmach.New.pf_whd_all + +And removed the following ones: + +Reductionops.whd_betaetalet +Reductionops.whd_betaetalet_stack +Reductionops.whd_betaetalet_state +Reductionops.whd_betadeltaeta_stack +Reductionops.whd_betadeltaeta_state +Reductionops.whd_betadeltaeta +Reductionops.whd_betadeltaiotaeta_stack +Reductionops.whd_betadeltaiotaeta_state +Reductionops.whd_betadeltaiotaeta + +In intf/genredexpr.mli, fIota was replaced by FMatch, FFix and +FCofix. Similarly, rIota was replaced by rMatch, rFix and rCofix. + ** Notation_ops ** Use Glob_ops.glob_constr_eq instead of Notation_ops.eq_glob_constr. diff --git a/dev/printers.mllib b/dev/printers.mllib index e15855ef26..3165495488 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -37,7 +37,7 @@ Feedback Segmenttree Unicodetable Unicode -Errors +CErrors CWarnings Bigint CUnix @@ -86,7 +86,7 @@ Nativecode Nativelib Cbytegen Environ -Closure +CClosure Reduction Nativeconv Type_errors @@ -208,7 +208,7 @@ Dn Btermdn Hints Himsg -Cerrors +ExplainErr Locality Assumptions Vernacinterp diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 6074acea46..023835af76 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -80,7 +80,7 @@ let ppconstr_univ x = Constrextern.with_universes ppconstr x let ppglob_constr = (fun x -> pp(pr_lglob_constr x)) let pppattern = (fun x -> pp(pr_constr_pattern x)) let pptype = (fun x -> try pp(pr_ltype x) with e -> pp (str (Printexc.to_string e))) -let ppfconstr c = ppconstr (Closure.term_of_fconstr c) +let ppfconstr c = ppconstr (CClosure.term_of_fconstr c) let ppbigint n = pp (str (Bigint.to_string n));; @@ -457,7 +457,7 @@ let print_pure_constr csr = print_string (Printexc.to_string e);print_flush (); raise e -let ppfconstr c = ppconstr (Closure.term_of_fconstr c) +let ppfconstr c = ppconstr (CClosure.term_of_fconstr c) let pploc x = let (l,r) = Loc.unloc x in print_string"(";print_int l;print_string",";print_int r;print_string")" @@ -514,7 +514,7 @@ let _ = (fun () -> in_current_context constr_display c) | _ -> failwith "Vernac extension: cannot occur") with - e -> Feedback.msg_notice (Errors.print e) + e -> Feedback.msg_notice (CErrors.print e) let _ = extend_vernac_command_grammar ("PrintConstr", 0) None [GramTerminal "PrintConstr"; @@ -530,7 +530,7 @@ let _ = (fun () -> in_current_context print_pure_constr c) | _ -> failwith "Vernac extension: cannot occur") with - e -> Feedback.msg_notice (Errors.print e) + e -> Feedback.msg_notice (CErrors.print e) let _ = extend_vernac_command_grammar ("PrintPureConstr", 0) None [GramTerminal "PrintPureConstr"; |