diff options
Diffstat (limited to 'dev/doc/changes.txt')
| -rw-r--r-- | dev/doc/changes.txt | 125 |
1 files changed, 112 insertions, 13 deletions
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index 322530e6..2f62be9a 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -1,4 +1,103 @@ ========================================= += CHANGES BETWEEN COQ V8.4 AND CQQ 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 = ========================================= @@ -516,14 +615,14 @@ 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) + (les parties noms et signatures ont été séparées) - Avm,Mavm,Fmavm,Mhm -> utiliser plutôt Map (et freeze alors gratuit) + Avm,Mavm,Fmavm,Mhm -> utiliser plutôt Map (et freeze alors gratuit) Mhb -> Bij - Generic est intégré à Term (et un petit peu à Closure) + Generic est intégré à Term (et un petit peu à Closure) -Changements dans les types de données : +Changements dans les types de données : --------------------------------------- dans Generic: free_rels : constr -> int Listset.t devient : constr -> Intset.t @@ -543,7 +642,7 @@ ATTENTION: try . .. with UserError _ -> ... - mais écrire à la place + mais écrire à la place try ... with e when Logic.catchable_exception e -> ... @@ -675,7 +774,7 @@ 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. +à traduire un constr en inductive sont les find_rectype and co. Changements dans les grammaires ------------------------------- @@ -683,9 +782,9 @@ 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) + casse particulière dans Coq) - . Le mot "command" est remplacé par "constr" dans les noms de + . 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* @@ -693,22 +792,22 @@ Changements dans les grammaires . Les constructeurs d'arguments de tactiques IDENTIFIER, CONSTR, ...n passent en minuscule Identifier, Constr, ... - . Plusieurs parsers ont changé de format (ex: sortarg) + . Plusieurs parsers ont changé de format (ex: sortarg) Changements dans le pretty-printing ----------------------------------- - . Découplage de la traduction de constr -> rawconstr (dans detyping) + . 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 + . 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 + directement le résultat du link du code => debuggage et profiling directs . il n'y a plus d'installation locale dans bin/$ARCH |