Imported Upstream version 8.8.2upstream/8.8.2

1 files changed, 0 insertions, 1095 deletions

diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
deleted file mode 100644
index 3de938d7..00000000
--- a/dev/doc/changes.txt
+++ /dev/null
@@ -1,1095 +0,0 @@
-=========================================
-= CHANGES BETWEEN COQ V8.5 AND COQ V8.6 =
-=========================================
-
-** Parsing **
-
-Pcoq.parsable now takes an extra optional filename argument so as to
-bind locations to a file name when relevant.
-
-** 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}
-
-All IDE-specific files, including the XML protocol have been moved to ide/
-
-** 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.
-
-** Logging and Pretty Printing: **
-
-* Printing functions have been removed from `Pp.mli`, which is now a
-  purely pretty-printing interface. Functions affected are:
-
-```` ocaml
-val pp          : std_ppcmds -> unit
-val ppnl        : std_ppcmds -> unit
-val pperr       : std_ppcmds -> unit
-val pperrnl     : std_ppcmds -> unit
-val pperr_flush : unit -> unit
-val pp_flush    : unit -> unit
-val flush_all   : unit -> unit
-val msg         : std_ppcmds -> unit
-val msgnl       : std_ppcmds -> unit
-val msgerr      : std_ppcmds -> unit
-val msgerrnl    : std_ppcmds -> unit
-val message     : string -> unit
-````
-
-  which are no more available. Users of `Pp.pp msg` should now use the
-  proper `Feedback.msg_*` function. Clients also have no control over
-  flushing, the back end takes care of it.
-
-  Also, the `msg_*` functions now take an optional `?loc` parameter
-  for relaying location to the client.
-
-* Feedback related functions and definitions have been moved to the
-  `Feedback` module. `message_level` has been renamed to
-  level. Functions moved from Pp to Feedback are:
-
-```` ocaml
-val set_logger      : logger -> unit
-val std_logger      : logger
-val emacs_logger    : logger
-val feedback_logger : logger
-````
-
-* Changes in the Feedback format/Protocol.
-
-- The `Message` feedback type now carries an optional location, the main
-  payload is encoded using the richpp document format.
-
-- The `ErrorMsg` feedback type is thus unified now with `Message` at
-  level `Error`.
-
-* We now provide several loggers, `log_via_feedback` is removed in
-  favor of `set_logger feedback_logger`. Output functions are:
-
-```` ocaml
-val with_output_to_file : string -> ('a -> 'b) -> 'a -> 'b
-val msg_error   : ?loc:Loc.t -> Pp.std_ppcmds -> unit
-val msg_warning : ?loc:Loc.t -> Pp.std_ppcmds -> unit
-val msg_notice  : ?loc:Loc.t -> Pp.std_ppcmds -> unit
-val msg_info    : ?loc:Loc.t -> Pp.std_ppcmds -> unit
-val msg_debug   : ?loc:Loc.t -> Pp.std_ppcmds -> unit
-````
-
-  with the `msg_*` functions being just an alias for `logger $Level`.
-
-* The main feedback functions are:
-
-```` ocaml
-val set_feeder : (feedback -> unit) -> unit
-val feedback : ?id:edit_or_state_id -> ?route:route_id -> feedback_content -> unit
-val set_id_for_feedback : ?route:route_id -> edit_or_state_id -> unit
-````
-  Note that `feedback` doesn't take two parameters anymore. After
-  refactoring the following function has been removed:
-
-```` ocaml
-val get_id_for_feedback : unit -> edit_or_state_id * route_id
-````
-
-** Kernel API changes **
-
-- The interface of the Context module was changed.
-  Related types and functions were put in separate submodules.
-  The mapping from old identifiers to new identifiers is the following:
-
-    Context.named_declaration            --->  Context.Named.Declaration.t
-    Context.named_list_declaration       --->  Context.NamedList.Declaration.t
-    Context.rel_declaration              --->  Context.Rel.Declaration.t
-    Context.map_named_declaration        --->  Context.Named.Declaration.map_constr
-    Context.map_named_list_declaration   --->  Context.NamedList.Declaration.map
-    Context.map_rel_declaration          --->  Context.Rel.Declaration.map_constr
-    Context.fold_named_declaration       --->  Context.Named.Declaration.fold
-    Context.fold_rel_declaration         --->  Context.Rel.Declaration.fold
-    Context.exists_named_declaration     --->  Context.Named.Declaration.exists
-    Context.exists_rel_declaration       --->  Context.Rel.Declaration.exists
-    Context.for_all_named_declaration    --->  Context.Named.Declaration.for_all
-    Context.for_all_rel_declaration      --->  Context.Rel.Declaration.for_all
-    Context.eq_named_declaration         --->  Context.Named.Declaration.equal
-    Context.eq_rel_declaration           --->  Context.Rel.Declaration.equal
-    Context.named_context                --->  Context.Named.t
-    Context.named_list_context           --->  Context.NamedList.t
-    Context.rel_context                  --->  Context.Rel.t
-    Context.empty_named_context          --->  Context.Named.empty
-    Context.add_named_decl               --->  Context.Named.add
-    Context.vars_of_named_context        --->  Context.Named.to_vars
-    Context.lookup_named                 --->  Context.Named.lookup
-    Context.named_context_length         --->  Context.Named.length
-    Context.named_context_equal          --->  Context.Named.equal
-    Context.fold_named_context           --->  Context.Named.fold_outside
-    Context.fold_named_list_context      --->  Context.NamedList.fold
-    Context.fold_named_context_reverse   --->  Context.Named.fold_inside
-    Context.instance_from_named_context  --->  Context.Named.to_instance
-    Context.extended_rel_list            --->  Context.Rel.to_extended_list
-    Context.extended_rel_vect            --->  Context.Rel.to_extended_vect
-    Context.fold_rel_context             --->  Context.Rel.fold_outside
-    Context.fold_rel_context_reverse     --->  Context.Rel.fold_inside
-    Context.map_rel_context              --->  Context.Rel.map_constr
-    Context.map_named_context            --->  Context.Named.map_constr
-    Context.iter_rel_context             --->  Context.Rel.iter
-    Context.iter_named_context           --->  Context.Named.iter
-    Context.empty_rel_context            --->  Context.Rel.empty
-    Context.add_rel_decl                 --->  Context.Rel.add
-    Context.lookup_rel                   --->  Context.Rel.lookup
-    Context.rel_context_length           --->  Context.Rel.length
-    Context.rel_context_nhyps            --->  Context.Rel.nhyps
-    Context.rel_context_tags             --->  Context.Rel.to_tags
-
-- Originally, rel-context was represented as:
-
-    Context.rel_context = Names.Name.t * Constr.t option * Constr.t
-
-  Now it is represented as:
-
-    Context.Rel.Declaration.t = LocalAssum of Names.Name.t * Constr.t
-	                      | LocalDef of Names.Name.t * Constr.t * Constr.t
- 
-- Originally, named-context was represented as:
-
-    Context.named_context = Names.Id.t * Constr.t option * Constr.t
-
-  Now it is represented as:
-
-    Context.Named.Declaration.t = LocalAssum of Names.Id.t * Constr.t
-	                        | LocalDef of Names.Id.t * Constr.t * Constr.t
-
-- The various EXTEND macros do not handle specially the Coq-defined entries
-  anymore. Instead, they just output a name that have to exist in the scope
-  of the ML code. The parsing rules (VERNAC) ARGUMENT EXTEND will look for
-  variables "$name" of type Gram.entry, while the parsing rules of
-  (VERNAC COMMAND | TACTIC) EXTEND, as well as the various TYPED AS clauses will
-  look for variables "wit_$name" of type Genarg.genarg_type. The small DSL
-  for constructing compound entries still works over this scheme. Note that in
-  the case of (VERNAC) ARGUMENT EXTEND, the name of the argument entry is bound
-  in the parsing rules, so beware of recursive calls.
-  
-  For example, to get "wit_constr" you must "open Constrarg" at the top of the file.
-
-- Evarutil was split in two parts. The new Evardefine file exposes functions
-define_evar_* mostly used internally in the unification engine.
-
-- The Refine module was move out of Proofview.
-
-    Proofview.Refine.* --->  Refine.*
-
-- A statically monotonous evarmap type was introduced in Sigma. Not all the API
-  has been converted, so that the user may want to use compatibility functions
-  Sigma.to_evar_map and Sigma.Unsafe.of_evar_map or Sigma.Unsafe.of_pair when
-  needed. Code can be straightforwardly adapted in the following way:
-
-  let (sigma, x1) = ... in
-  ...
-  let (sigma, xn) = ... in
-  (sigma, ans)
-
-  should be turned into:
-
-  open Sigma.Notations
-
-  let Sigma (x1, sigma, p1) = ... in
-  ...
-  let Sigma (xn, sigma, pn) = ... in
-  Sigma (ans, sigma, p1 +> ... +> pn)
-  
-  Examples of `Sigma.Unsafe.of_evar_map` include:
-  
-  Evarutil.new_evar env (Tacmach.project goal) ty   ----> Evarutil.new_evar env (Sigma.Unsafe.of_evar_map (Tacmach.project goal)) ty
-
-- The Proofview.Goal.*enter family of functions now takes a polymorphic
-  continuation given as a record as an argument.
-
-  Proofview.Goal.enter begin fun gl -> ... end
-
-  should be turned into
-
-  open Proofview.Notations
-
-  Proofview.Goal.enter { enter = begin fun gl -> ... end }
-  
-- `Tacexpr.TacDynamic(Loc.dummy_loc, Pretyping.constr_in c)`      ---> `Tacinterp.Value.of_constr c`
-- `Vernacexpr.HintsResolveEntry(priority, poly, hnf, path, atom)` ---> `Vernacexpr.HintsResolveEntry(Vernacexpr.({hint_priority = priority; hint_pattern = None}), poly, hnf, path, atom)`
-- `Pretyping.Termops.mem_named_context`                           ---> `Engine.Termops.mem_named_context_val`
-  (`Global.named_context`                                         ---> `Global.named_context_val`)
-  (`Context.Named.lookup`                                         ---> `Environ.lookup_named_val`)
-
-** Search API **
-
-The main search functions now take a function iterating over the
-results. This allows for clients to use streaming or more economic
-printing.
-
-=========================================
-= CHANGES BETWEEN COQ V8.4 AND COQ V8.5 =
-=========================================
-
-** Refactoring : more mli interfaces and simpler grammar.cma **
-
-- A new directory intf/ now contains mli-only interfaces :
-
- Constrexpr : definition of constr_expr, was in Topconstr
- Decl_kinds : now contains binding_kind = Explicit | Implicit
- Evar_kinds : type Evar_kinds.t was previously Evd.hole_kind
- Extend : was parsing/extend.mli
- Genredexpr : regroup Glob_term.red_expr_gen and Tacexpr.glob_red_flag
- Glob_term  : definition of glob_constr
- Locus : definition of occurrences and stuff about clauses
- Misctypes : intro_pattern_expr, glob_sort, cast_type, or_var, ...
- Notation_term : contains notation_constr, was Topconstr.aconstr
- Pattern : contains constr_pattern
- Tacexpr : was tactics/tacexpr.ml
- Vernacexpr : was toplevel/vernacexpr.ml
-
-- Many files have been divided :
-
- vernacexpr: vernacexpr.mli + Locality
- decl_kinds: decl_kinds.mli + Kindops
- evd: evar_kinds.mli + evd
- tacexpr: tacexpr.mli + tacops
- glob_term: glob_term.mli + glob_ops + genredexpr.mli + redops
- topconstr: constrexpr.mli + constrexpr_ops
-            + notation_expr.mli + notation_ops + topconstr
- pattern: pattern.mli + patternops
- libnames: libnames (qualid, reference) + globnames (global_reference)
- egrammar: egramml + egramcoq
-
-- New utility files : miscops (cf. misctypes.mli) and
-  redops (cf genredexpr.mli).
-
-- Some other directory changes :
-  * grammar.cma and the source files specific to it are now in grammar/
-  * pretty-printing files are now in printing/
-
-- Inner-file changes :
-
-  * aconstr is now notation_constr, all constructors for this type
-    now start with a N instead of a A (e.g. NApp instead of AApp),
-    and functions about aconstr may have been renamed (e.g. match_aconstr
-    is now match_notation_constr).
-
-  * occurrences (now in Locus.mli) is now an algebraic type, with
-    - AllOccurrences instead of all_occurrences_expr = (false,[])
-    - (AllOccurrencesBut l) instead of (all_occurrences_expr_but l) = (false,l)
-    - NoOccurrences instead of no_occurrences_expr = (true,[])
-    - (OnlyOccurrences l) instead of (no_occurrences_expr_but l) = (true,l)
-
-  * move_location (now in Misctypes) has two new constructors
-    MoveFirst and MoveLast replacing (MoveToEnd false) and (MoveToEnd true)
-
-- API of pretyping.ml and constrintern.ml has been made more uniform
-  * Parametrization of understand_* functions is now made using
-    "inference flags"
-  * Functions removed:
-    - interp_constr_judgment (inline its former body if really needed)
-    - interp_casted_constr, interp_type: use instead interp_constr with
-      expected_type set to OfType or to IsType
-    - interp_gen: use any of interp_constr, interp_casted_constr, interp_type
-    - interp_open_constr_patvar
-    - interp_context: use interp_context_evars (with a "evar_map ref") and
-      call solve_remaining_evars afterwards with a failing flag
-      (e.g. all_and_fail_flags)
-    - understand_type, understand_gen: use understand with appropriate
-      parameters
-  * Change of semantics:
-    - Functions interp_*_evars_impls have a different interface and do
-      not any longer check resolution of evars by default; use
-      check_evars_are_solved explicitly to check that evars are solved.
-  See also the corresponding commit log.
-
-- Tactics API: new_induct -> induction; new_destruct -> destruct;
-  letin_pat_tac do not accept a type anymore
-
-- New file find_subterm.ml for gathering former functions
-  subst_closed_term_occ_modulo, subst_closed_term_occ_decl (which now
-  take and outputs also an evar_map), and
-  subst_closed_term_occ_modulo, subst_closed_term_occ_decl_modulo (now
-  renamed into replace_term_occ_modulo and
-  replace_term_occ_decl_modulo).
-
-- API of Inductiveops made more uniform (see commit log or file itself).
-
-- API of intros_pattern style tactic changed; "s" is dropped in
-  "intros_pattern" and "intros_patterns" is not anymore behaving like
-  tactic "intros" on the empty list.
-
-- API of cut tactics changed: for instance, cut_intro should be replaced by
-  "assert_after Anonymous"
-
-- All functions taking an env and a sigma (or an evdref) now takes the
-  env first.
-
-=========================================
-= CHANGES BETWEEN COQ V8.3 AND COQ V8.4 =
-=========================================
-
-** Functions in unification.ml have now the evar_map coming just after the env
-
-** Removal of Tacinterp.constr_of_id **
-
-Use instead either global_reference or construct_reference in constrintern.ml.
-
-** Optimizing calls to Evd functions **
-
-Evars are split into defined evars and undefined evars; for
-efficiency, when an evar is known to be undefined, it is preferable to
-use specific functions about undefined evars since these ones are
-generally fewer than the defined ones.
-
-** Type changes in TACTIC EXTEND rules **
-
-Arguments bound with tactic(_) in TACTIC EXTEND rules are now of type
-glob_tactic_expr, instead of glob_tactic_expr * tactic. Only the first
-component is kept, the second one can be obtained via
-Tacinterp.eval_tactic.
-
-** ARGUMENT EXTEND **
-
-It is now forbidden to use TYPED simultaneously with {RAW,GLOB}_TYPED
-in ARGUMENT EXTEND statements.
-
-** Renaming of rawconstr to glob_constr **
-
-The "rawconstr" type has been renamed to "glob_constr" for
-consistency. The "raw" in everything related to former rawconstr has
-been changed to "glob". For more details about the rationale and
-scripts to migrate code using Coq's internals, see commits 13743,
-13744, 13755, 13756, 13757, 13758, 13761 (by glondu, end of December
-2010) in Subversion repository. Contribs have been fixed too, and
-commit messages there might also be helpful for migrating.
-
-=========================================
-= CHANGES BETWEEN COQ V8.2 AND COQ V8.3 =
-=========================================
-
-** Light cleaning in evarutil.ml **
-
-whd_castappevar is now whd_head_evar
-obsolete whd_ise disappears
-
-** Restructuration of the syntax of binders **
-
-binders_let -> binders
-binders_let_fixannot -> binders_fixannot
-binder_let -> closed_binder (and now covers only bracketed binders)
-binder was already obsolete and has been removed
-
-** Semantical change of h_induction_destruct **
-
-Warning, the order of the isrec and evar_flag was inconsistent and has
-been permuted. Tactic induction_destruct in tactics.ml is unchanged.
-
-** Internal tactics renamed
-
-There is no more difference between bindings and ebindings. The
-following tactics are therefore renamed
-
-apply_with_ebindings_gen -> apply_with_bindings_gen
-left_with_ebindings -> left_with_bindings
-right_with_ebindings -> right_with_bindings
-split_with_ebindings -> split_with_bindings
-
-and the following tactics are removed
-
-apply_with_ebindings (use instead apply_with_bindings)
-eapply_with_ebindings (use instead eapply_with_bindings)
-
-** Obsolete functions in typing.ml
-
-For mtype_of, msort_of, mcheck, now use type_of, sort_of, check
-
-** Renaming functions renamed
-
-concrete_name -> compute_displayed_name_in
-concrete_let_name -> compute_displayed_let_name_in
-rename_rename_bound_var -> rename_bound_vars_as_displayed
-lookup_name_as_renamed -> lookup_name_as_displayed
-next_global_ident_away true -> next_ident_away_in_goal
-next_global_ident_away false -> next_global_ident_away
-
-** Cleaning in commmand.ml
-
-Functions about starting/ending a lemma are in lemmas.ml
-Functions about inductive schemes are in indschemes.ml
-
-Functions renamed:
-
-declare_one_assumption -> declare_assumption
-declare_assumption -> declare_assumptions
-Command.syntax_definition -> Metasyntax.add_syntactic_definition
-declare_interning_data merged with add_notation_interpretation
-compute_interning_datas -> compute_full_internalization_env
-implicits_env -> internalization_env
-full_implicits_env -> full_internalization_env
-build_mutual -> do_mutual_inductive
-build_recursive -> do_fixpoint
-build_corecursive -> do_cofixpoint
-build_induction_scheme -> build_mutual_induction_scheme
-build_indrec -> build_induction_scheme
-instantiate_type_indrec_scheme -> weaken_sort_scheme
-instantiate_indrec_scheme -> modify_sort_scheme
-make_case_dep, make_case_nodep -> build_case_analysis_scheme
-make_case_gen -> build_case_analysis_scheme_default
-
-Types:
-
-decl_notation -> decl_notation option
-
-** Cleaning in libnames/nametab interfaces
-
-Functions:
-
-dirpath_prefix -> pop_dirpath
-extract_dirpath_prefix pop_dirpath_n
-extend_dirpath -> add_dirpath_suffix
-qualid_of_sp -> qualid_of_path
-pr_sp -> pr_path
-make_short_qualid -> qualid_of_ident
-sp_of_syntactic_definition -> path_of_syntactic_definition 
-sp_of_global -> path_of_global
-id_of_global -> basename_of_global
-absolute_reference -> global_of_path
-locate_syntactic_definition -> locate_syndef
-path_of_syntactic_definition -> path_of_syndef
-push_syntactic_definition -> push_syndef
-
-Types:
-
-section_path -> full_path
-
-** Cleaning in parsing extensions (commit 12108)
-
-Many moves and renamings, one new file (Extrawit, that contains wit_tactic).
-
-** Cleaning in tactical.mli
-
-tclLAST_HYP -> onLastHyp
-tclLAST_DECL -> onLastDecl
-tclLAST_NHYPS -> onNLastHypsId
-tclNTH_DECL -> onNthDecl
-tclNTH_HYP -> onNthHyp
-onLastHyp -> onLastHypId
-onNLastHyps -> onNLastDecls
-onClauses -> onClause
-allClauses -> allHypsAndConcl
-
-+ removal of various unused combinators on type "clause"
-
-=========================================
-= CHANGES BETWEEN COQ V8.1 AND COQ V8.2 =
-=========================================
-
-A few differences in Coq ML interfaces between Coq V8.1 and V8.2
-================================================================
-
-** Datatypes
-
-List of occurrences moved from "int list" to "Termops.occurrences" (an
-  alias to "bool * int list")
-ETIdent renamed to ETName
-
-** Functions
-
-Eauto: e_resolve_constr, vernac_e_resolve_constr -> simplest_eapply
-Tactics: apply_with_bindings -> apply_with_bindings_wo_evars
-Eauto.simplest_apply -> Hiddentac.h_simplest_apply
-Evarutil.define_evar_as_arrow -> define_evar_as_product
-Old version of Tactics.assert_tac disappears
-Tactics.true_cut renamed into Tactics.assert_tac
-Constrintern.interp_constrpattern -> intern_constr_pattern
-Hipattern.match_with_conjunction is a bit more restrictive
-Hipattern.match_with_disjunction is a bit more restrictive
-
-** Universe names (univ.mli)
-
- base_univ -> type0_univ  (* alias of Set is the Type hierarchy *)
- prop_univ -> type1_univ  (* the type of Set in the Type hierarchy *)
- neutral_univ -> lower_univ (* semantic alias of Prop in the Type hierarchy *)
- is_base_univ -> is_type1_univ
- is_empty_univ -> is_lower_univ
-
-** Sort names (term.mli)
-
-  mk_Set -> set_sort
-  mk_Prop -> prop_sort
-  type_0 -> type1_sort
-
-=========================================
-= CHANGES BETWEEN COQ V8.0 AND COQ V8.1 =
-=========================================
-
-A few differences in Coq ML interfaces between Coq V8.0 and V8.1
-================================================================
-
-** Functions
-
-Util: option_app -> option_map
-Term: substl_decl -> subst_named_decl
-Lib: library_part -> remove_section_part
-Printer: prterm -> pr_lconstr
-Printer: prterm_env -> pr_lconstr_env
-Ppconstr: pr_sort -> pr_rawsort
-Evd: in_dom, etc got standard ocaml names (i.e. mem, etc)
-Pretyping: 
- - understand_gen_tcc and understand_gen_ltac merged into understand_ltac
- - type_constraints can now say typed by a sort (use OfType to get the
-   previous behavior)
-Library: import_library -> import_module
-
-** Constructors
-
-Declarations: mind_consnrealargs -> mind_consnrealdecls
-NoRedun -> NoDup
-Cast and RCast have an extra argument: you can recover the previous
-  behavior by setting the extra argument to "CastConv DEFAULTcast" and
-  "DEFAULTcast" respectively
-Names: "kernel_name" is now "constant" when argument of Term.Const
-Tacexpr: TacTrueCut and TacForward(false,_,_) merged into new TacAssert
-Tacexpr: TacForward(true,_,_) branched to TacLetTac
-
-** Modules
-
-module Decl_kinds: new interface
-module Bigint: new interface
-module Tacred spawned module Redexpr
-module Symbols -> Notation
-module Coqast, Ast, Esyntax, Termast, and all other modules related to old
-  syntax are removed
-module Instantiate: integrated to Evd
-module Pretyping now a functor: use Pretyping.Default instead
-
-** Internal names
-
-OBJDEF and OBJDEF1 -> CANONICAL-STRUCTURE
-
-** Tactic extensions
-
-- printers have an extra parameter which is a constr printer at high precedence
-- the tactic printers have an extra arg which is the expected precedence 
-- level is now a precedence in declare_extra_tactic_pprule
-- "interp" functions now of types the actual arg type, not its encapsulation
-  as a generic_argument
-
-=========================================
-= CHANGES BETWEEN COQ V7.4 AND COQ V8.0 =
-=========================================
-
-See files in dev/syntax-v8
-
-
-==============================================
-= MAIN CHANGES BETWEEN COQ V7.3 AND COQ V7.4 =
-==============================================
-
-CHANGES DUE TO INTRODUCTION OF MODULES
-======================================
-
-1.Kernel
---------
-
-  The module level has no effect on constr except for the structure of
-section_path. The type of unique names for constructions (what
-section_path served) is now called a kernel name and is defined by
- 
-type uniq_ident = int * string * dir_path (* int may be enough *)
-type module_path =
-  | MPfile of dir_path    (* reference to physical module, e.g. file *)
-  | MPbound of uniq_ident (* reference to a module parameter in a functor *)
-  | MPself of uniq_ident  (* reference to one of the containing module *)
-  | MPdot of module_path * label
-type label = identifier
-type kernel_name = module_path * dir_path * label
-                   ^^^^^^^^^^^   ^^^^^^^^   ^^^^^
-                        |           |         \
-                        |           |          the base name
-                        |           \
-                       /             the (true) section path
-   example:                          (non empty only inside open sections)
-   L = (* i.e. some file of logical name L *)
-   struct
-     module A = struct Def a = ... end
-   end
-   M = (* i.e. some file of logical name M *)
-   struct
-     Def t = ...
-     N = functor (X : sig module T = struct Def b = ... end end) -> struct
-       module O = struct
-         Def u = ...
-       end
-       Def x := ... <M>.t ... <N>.O.u ... X.T.b ... L.A.a
- 
-   <M> and <N> are self-references, X is a bound reference and L is a
-reference to a physical module.
- 
-  Notice that functor application is not part of a path: it must be
-named by a "module M = F(A)" declaration to be used in a kernel
-name.
- 
-  Notice that Jacek chose a practical approach, making directories not
-modules. Another approach could have been to replace the constructor
-MPfile by a constant constructor MProot representing the root of the
-world.
- 
-  Other relevant informations are in kernel/entries.ml (type
-module_expr) and kernel/declarations.ml (type module_body and
-module_type_body).                                                              
-
-2. Library
-----------
-
-i) tables 
-[Summaries] - the only change is the special treatment of the
-global environmet.
-
-ii) objects 
-[Libobject] declares persistent objects, given with methods:
-
-   * cache_function specifying how to add the object in the current
-       scope;
-   * load_function, specifying what to do when the module 
-       containing the object is loaded; 
-   * open_function, specifying what to do when the module 
-       containing the object is opened (imported);
-   * classify_function, specyfying what to do with the object,
-       when the current module (containing the object) is ended. 
-   * subst_function
-   * export_function, to signal end_section survival
-
-(Almost) Each of these methods is called with a parameter of type
-object_name = section_path * kernel_name
-where section_path is the full user name of the object (such as
-Coq.Init.Datatypes.Fst) and kernel_name is its substitutive internal
-version such as (MPself<Datatypes#1>,[],"Fst") (see above)
-
-
-What happens at the end of an interactive module ?
-==================================================
-(or when a file is stored and reloaded from disk)
-
-All summaries (except Global environment) are reverted to the state
-from before the beginning of the module, and:
-
-a) the objects (again, since last Declaremods.start_module or
-   Library.start_library) are classified using the classify_function.
-   To simplify consider only those who returned Substitute _ or Keep _.
-
-b) If the module is not a functor, the subst_function for each object of
-   the first group is called with the substitution 
-   [MPself "<Datatypes#1>" |-> MPfile "Coq.Init.Datatypes"].
-   Then the load_function is called for substituted objects and the
-   "keep" object. 
-   (If the module is a library the substitution is done at reloading).
-
-c) The objects which returned substitute are stored in the modtab
-   together with the self ident of the module, and functor argument
-   names if the module was a functor.
-
-   They will be used (substituted and loaded) when a command like 
-     Module M := F(N)    or
-     Module Z := N 
-   is evaluated
-
-
-The difference between "substitute" and "keep" objects
-========================================================
-i) The "keep" objects can _only_ reference other objects by section_paths
-and qualids. They do not need the substitution function.
-
-They will work after end_module (or reloading a compiled library),
-because these operations do not change section_path's
-
-They will obviously not work after Module Z:=N.
- 
-These would typically be grammar rules, pretty printing rules etc.
-
-
-
-ii) The "substitute" objects can _only_ reference objects by
-kernel_names. They must have a valid subst_function. 
-
-They will work after end_module _and_ after Module Z:=N or 
-Module Z:=F(M).
-
-
-
-Other kinds of objects:
-iii) "Dispose" - objects which do not survive end_module
-     As a consequence, objects which reference other objects sometimes
-     by kernel_names and sometimes by section_path must be of this kind...
-
-iv) "Anticipate" - objects which must be treated individually by
-    end_module (typically "REQUIRE" objects)
-
-
-
-Writing subst_thing functions
-=============================
-The subst_thing shoud not copy the thing if it hasn't actually
-changed. There are some cool emacs macros in dev/objects.el 
-to help writing subst functions this way quickly and without errors.
-Also there are *_smartmap functions in Util.
-
-The subst_thing functions are already written for many types,
-including constr (Term.subst_mps), 
-global_reference (Libnames.subst_global),
-rawconstr (Rawterm.subst_raw) etc
-
-They are all (apart from constr, for now) written in the non-copying
-way.
-
-
-Nametab
-=======
-
-Nametab has been made more uniform. For every kind of thing there is
-only one "push" function and one "locate" function. 
-
-
-Lib
-===
-
-library_segment is now a list of object_name * library_item, where
-object_name = section_path * kernel_name (see above)
-
-New items have been added for open modules and module types
-
-
-Declaremods
-==========
-Functions to declare interactive and noninteractive modules and module
-types.
-
-
-Library
-=======
-Uses Declaremods to actually communicate with Global and to register
-objects.
-
-
-OTHER CHANGES
-=============
-
-Internal representation of tactics bindings has changed (see type
-Rawterm.substitution).
-
-New parsing model for tactics and vernacular commands
-
-  - Introduction of a dedicated type for tactic expressions
-    (Tacexpr.raw_tactic_expr)
-  - Introduction of a dedicated type for vernac expressions
-    (Vernacexpr.vernac_expr)
-  - Declaration of new vernacular parsing rules by a new camlp4 macro
-    GRAMMAR COMMAND EXTEND ... END  to be used in ML files
-  - Declaration of new tactics parsing/printing rules by a new camlp4 macro
-    TACTIC EXTEND ... END  to be used in ML files
-
-New organisation of THENS:
-tclTHENS tac tacs : tacs is now an array
-tclTHENSFIRSTn tac1 tacs tac2 :
-  apply tac1 then, apply the array tacs on the first n subgoals and
-  tac2 on the remaining subgoals (previously tclTHENST)
-tclTHENSLASTn tac1 tac2 tacs :
-  apply tac1 then, apply tac2 on the first subgoals and apply the array
-  tacs on the last n subgoals
-tclTHENFIRSTn tac1 tacs = tclTHENSFIRSTn tac1 tacs tclIDTAC (prev. tclTHENSI)
-tclTHENLASTn tac1 tacs  = tclTHENSLASTn tac1 tclIDTAC tacs
-tclTHENFIRST tac1 tac2  = tclTHENFIRSTn tac1 [|tac2|]
-tclTHENLAST tac1 tac2   = tclTHENLASTn tac1 [|tac2|] (previously tclTHENL)
-tclTHENS tac1 tacs = tclTHENSFIRSTn tac1 tacs (fun _ -> error "wrong number")
-tclTHENSV same as tclTHENS but with an array
-tclTHENSi : no longer available
-
-Proof_type: subproof field in type proof_tree glued with the ref field
-
-Tacmach: no more echo from functions of module Refiner
-
-Files plugins/*/g_*.ml4 take the place of files plugins/*/*.v.
-Files parsing/{vernac,tac}extend.ml{4,i} implements TACTIC EXTEND andd
-  VERNAC COMMAND EXTEND macros
-File syntax/PPTactic.v moved to parsing/pptactic.ml
-Tactics about False and not now in tactics/contradiction.ml
-Tactics depending on Init now tactics/*.ml4 (no longer in tactics/*.v)
-File tacinterp.ml moved from proofs to directory tactics
-
-
-==========================================
-= MAIN CHANGES FROM COQ V7.1 TO COQ V7.2 =
-==========================================
-
-The core of Coq (kernel) has meen minimized with the following effects:
-
-kernel/term.ml      split into kernel/term.ml,      pretyping/termops.ml
-kernel/reduction.ml split into kernel/reduction.ml, pretyping/reductionops.ml
-kernel/names.ml     split into kernel/names.ml,     library/nameops.ml
-kernel/inductive.ml split into kernel/inductive.ml, pretyping/inductiveops.ml
-
-the prefixes "Is" ans "IsMut" have been dropped from kind_of_term constructors,
-e.g. IsRel is now Rel, IsMutCase is now Case, etc.
-
-
-=======================================================
-= PRINCIPAUX CHANGEMENTS ENTRE COQ V6.3.1 ET COQ V7.0 =
-=======================================================
-
-Changements d'organisation / modules :
---------------------------------------
-
-  Std, More_util		-> lib/util.ml
-
-  Names				-> kernel/names.ml et kernel/sign.ml
-    (les parties noms et signatures ont été séparées)
-
-  Avm,Mavm,Fmavm,Mhm  ->  utiliser plutôt Map (et freeze alors gratuit)
-  Mhb                 ->  Bij
-
-  Generic est intégré à Term (et un petit peu à Closure)
-
-Changements dans les types de données :
----------------------------------------
-  dans Generic: free_rels : constr -> int Listset.t
-                  devient : constr -> Intset.t
-
-  type_judgement ->  typed_type
-  environment    ->  context
-  context        ->  typed_type signature
-
-
-ATTENTION:
-----------
-
-  Il y a maintenant d'autres exceptions que UserError (TypeError,
-  RefinerError, etc.)
-
-  Il ne faut donc plus se contenter (pour rattraper) de faire
-  
-		try . .. with UserError _ -> ...
-
-  mais écrire à la place
- 
-                try ... with e when Logic.catchable_exception e -> ...
-
-
-Changements dans les fonctions :
---------------------------------
-
-	Vectops.
-	  it_vect          ->  Array.fold_left
-	  vect_it          ->  Array.fold_right
-	  exists_vect      ->  Util.array_exists
-	  for_all2eq_vect  ->  Util.array_for_all2
-	  tabulate_vect    ->  Array.init
-	  hd_vect          ->  Util.array_hd
-	  tl_vect          ->  Util.array_tl
-	  last_vect        ->  Util.array_last
-	  it_vect_from     ->  array_fold_left_from
-	  vect_it_from     ->  array_fold_right_from
-	  app_tl_vect	   ->  array_app_tl
-	  cons_vect	   ->  array_cons
-	  map_i_vect	   ->  Array.mapi
-	  map2_vect	   ->  array_map2
-	  list_of_tl_vect  ->  array_list_of_tl
-
-        Names
-          sign_it        -> fold_var_context (se fait sur env maintenant)
-	  it_sign        -> fold_var_context_reverse (sur env maintenant)
-
-        Generic
-	  noccur_bet     -> noccur_between
-          substn_many    -> substnl
-
-	Std 
-	  comp           ->  Util.compose
-	  rev_append	 ->  List.rev_append
-
-	Termenv
-	  mind_specif_of_mind  -> Global.lookup_mind_specif
-                ou Environ.lookup_mind_specif si on a un env sous la main
-	  mis_arity      ->  instantiate_arity
-	  mis_lc	 ->  instantiate_lc	
-
-	Ex-Environ	 
-	  mind_of_path      -> Global.lookup_mind
-
-	Printer
-	  gentermpr	->   gen_pr_term
-          term0	        ->   prterm_env	
-          pr_sign       ->   pr_var_context
-	  pr_context_opt -> pr_context_of
-          pr_ne_env      -> pr_ne_context_of
-
-	Typing, Machops
-	  type_of_type     ->  judge_of_type
-	  fcn_proposition  ->  judge_of_prop_contents
-	  safe_fmachine    ->  safe_infer
-
-	Reduction, Clenv
-          whd_betadeltat      -> whd_betaevar
-          whd_betadeltatiota  -> whd_betaiotaevar
-          find_mrectype       -> Inductive.find_mrectype
-          find_minductype     -> Inductive.find_inductive
-          find_mcoinductype   -> Inductive.find_coinductive
-
-        Astterm
-          constr_of_com_casted -> interp_casted_constr
-          constr_of_com_sort   -> interp_type
-          constr_of_com        -> interp_constr
-          rawconstr_of_com     -> interp_rawconstr
-          type_of_com          -> type_judgement_of_rawconstr
-	  judgement_of_com     -> judgement_of_rawconstr
-
-        Termast
-          bdize                -> ast_of_constr
-
-        Tacmach
-          pf_constr_of_com_sort -> pf_interp_type
-          pf_constr_of_com      -> pf_interp_constr
-	  pf_get_hyp            -> pf_get_hyp_typ
-          pf_hyps, pf_untyped_hyps -> pf_env (tout se fait sur env maintenant)
-
-        Pattern
-	  raw_sopattern_of_compattern -> Astterm.interp_constrpattern
-	  somatch               -> is_matching
-          dest_somatch          -> matches
-
-        Tacticals
-	  matches               -> gl_is_matching
-          dest_match            -> gl_matches
-	  suff                  -> utiliser sort_of_goal
-          lookup_eliminator     -> utiliser sort_of_goal pour le dernier arg
-
-        Divers
-          initial_sign     -> var_context
-
-        Sign
-          ids_of_sign      -> ids_of_var_context (or Environ.ids_of_context)
-          empty_sign       -> empty_var_context
-
-        Pfedit
-	  list_proofs      -> get_all_proof_names
-          get_proof        -> get_current_proof_name
-          abort_goal       -> abort_proof
-          abort_goals      -> abort_all_proofs
-          abort_cur_goal   -> abort_current_proof
-          get_evmap_sign   -> get_goal_context/get_current_goal_context
-          unset_undo       -> reset_undo
-
-        Proof_trees
-          mkGOAL           -> mk_goal
-
-        Declare
-  	  machine_constant ->   declare_constant (+ modifs)
-
-	ex-Trad, maintenant Pretyping
-          inh_cast_rel        -> Coercion.inh_conv_coerce_to
-          inh_conv_coerce_to  -> Coercion.inh_conv_coerce_to_fail
-	  ise_resolve1        -> understand, understand_type
-	  ise_resolve         -> understand_judgment, understand_type_judgment
-
-        ex-Tradevar, maintenant Evarutil
-          mt_tycon            -> empty_tycon
-
-        Recordops
-          struc_info          -> find_structure
-
-Changements dans les inductifs
-------------------------------
-Nouveaux types "constructor" et "inductive" dans Term
-La plupart des fonctions de typage des inductives prennent maintenant
-un inductive au lieu d'un oonstr comme argument. Les seules fonctions
-à traduire un constr en inductive sont les find_rectype and co.
-
-Changements dans les grammaires
--------------------------------
-
- . le lexer (parsing/lexer.mll) est maintenant un lexer ocamllex
-
- . attention : LIDENT -> IDENT  (les identificateurs n'ont pas de
-                                 casse particulière dans Coq)
-
- . Le mot "command" est remplacé par "constr" dans les noms de
- fichiers, noms de modules et non-terminaux relatifs au parsing des
- termes; aussi les changements suivants "COMMAND"/"CONSTR" dans
- g_vernac.ml4, VARG_COMMAND/VARG_CONSTR dans vernac*.ml*
-
- . Les constructeurs d'arguments de tactiques IDENTIFIER, CONSTR, ...n
-   passent en minuscule Identifier, Constr, ...
- 
- . Plusieurs parsers ont changé de format (ex: sortarg)
-
-Changements dans le pretty-printing
------------------------------------
-
- . Découplage de la traduction de constr -> rawconstr (dans detyping)
-    et de rawconstr -> ast (dans termast)
- . Déplacement des options d'affichage de printer vers termast
- . Déplacement des réaiguillage d'univers du pp de printer vers esyntax
-
-	
-Changements divers
-------------------
-
- . il n'y a plus de script coqtop => coqtop et coqtop.byte sont
-   directement le résultat du link du code
-   => debuggage et profiling directs
-
- . il n'y a plus d'installation locale dans bin/$ARCH
- 
- . #use "include.ml"  =>  #use "include"
-   go()               =>  loop()
-
- . il y a "make depend" et "make dependcamlp4" car ce dernier prend beaucoup
-   de temps