diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/base_include | 1 | ||||
| -rw-r--r-- | dev/doc/changes.txt | 2 |
2 files changed, 3 insertions, 0 deletions
diff --git a/dev/base_include b/dev/base_include index 255e28a668..398f60d2b7 100644 --- a/dev/base_include +++ b/dev/base_include @@ -89,6 +89,7 @@ open Indrec open Typing open Inductiveops open Unification +open Matching open Constrextern open Constrintern diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index d8cdf738d9..b50a3d72bc 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -9,6 +9,8 @@ A few differences in Coq ML interfaces between Coq V8.0 and V8.1 Eauto: e_resolve_constr, vernac_e_resolve_constr -> simplest_eapply Tactics: apply_with_bindings -> apply_with_bindings_wo_evars +Tactics: boolean argument of letin_tac changed its meaning (false now + means use Leibniz equality instead of a local definition) Eauto.simplest_apply -> Hiddentac.h_simplest_apply Evarutil.define_evar_as_arrow -> define_evar_as_product |