diff -Nru coq-8.4pl3dfsg/CHANGES coq-8.4pl4dfsg/CHANGES --- coq-8.4pl3dfsg/CHANGES 2013-12-21 08:03:14.000000000 +0000 +++ coq-8.4pl4dfsg/CHANGES 2014-04-24 15:13:03.000000000 +0000 @@ -1,3 +1,43 @@ +Changes from V8.4pl3 to V8.4pl4 +=============================== + +WARNING: +The current logic of Coq is now known to be inconsistent with + Axiom prop_extensionality : forall A B:Prop, (A <-> B) -> A = B. +For more details, see: + https://gforge.inria.fr/plugins/scmgit/cgi-bin/gitweb.cgi?p=coq/coq.git;a=blob_plain;f=test-suite/failure/subterm2.v;hb=HEAD +or + https://gforge.inria.fr/plugins/scmgit/cgi-bin/gitweb.cgi?p=coq/coq.git;a=blob_plain;f=test-suite/failure/subterm3.v;hb=HEAD + +Kernel + +- Bug #3211: unsound check of elimination sort. +- Fix guard condition for nested cofixpoints. +- Bug #3243: Univ constraints of module subtyping were not propagated. + +Tactics + +- A new option "Set Stable Omega" ensures that repeated identical calls + to omega will produce identical proof terms. This option is off by default + for maximal compatibility, but should be pretty safe to activate. +- The interpretation of the open_constr tactic argument was erroneously + firing type classes resolution in some corner cases. This has been + fixed. The tactic argument type open_constr_wTC is provided for retro + compatibility purposes. +- Fixing bug #3228 (fixing precedence of ltac variables over variables in + env) introduces rare and justified tactic failure. + +Bug fixes + +- Solved bugs: + #3260, #2697, #3037, #3262, #2900, #3131, #3238, #3204, #1758, #1039, + #3144 +- micromega: solved an ambiguous symbol resolution. +- Coq always uses / as separator between directories on all platforms. +- remove trailing '\r' from file names returned by coqtop. +- bug correction in proving inversion principles for Function. +- ocamlbuild: minor fixes related to camlp4 and cross-compilation. + Changes from V8.4pl2 to V8.4pl3 =============================== diff -Nru coq-8.4pl3dfsg/checker/checker.ml coq-8.4pl4dfsg/checker/checker.ml --- coq-8.4pl3dfsg/checker/checker.ml 2013-12-21 08:03:14.000000000 +0000 +++ coq-8.4pl4dfsg/checker/checker.ml 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* raise (LocalArity None)); srec (push_rel (na1,None,a1) env) t ar' - | Prod (_,a1,a2), [] -> (* whnf of t was not needed here! *) - let ksort = match (whd_betadeltaiota env a2) with - | Sort s -> family_of_sort s + | Prod (na1,a1,a2), [] -> (* whnf of t was not needed here! *) + let env' = push_rel (na1,None,a1) env in + let ksort = match (whd_betadeltaiota env' a2) with + | Sort s -> family_of_sort s | _ -> raise (LocalArity None) in let dep_ind = build_dependent_inductive ind specif params in (try conv env a1 dep_ind @@ -289,6 +290,8 @@ | Sort s', [] -> check_allowed_sort (family_of_sort s') specif; false + | _, (_,Some _,_ as d)::ar' -> + srec (push_rel d env) (lift 1 pt') ar' | _ -> raise (LocalArity None) in @@ -895,12 +898,12 @@ raise (CoFixGuardError (env,RecCallInTypeOfAbstraction a)) | CoFix (j,(_,varit,vdefs as recdef)) -> - if (List.for_all (noccur_with_meta n nbfix) args) + if List.for_all (noccur_with_meta n nbfix) args then - let nbfix = Array.length vdefs in - if (array_for_all (noccur_with_meta n nbfix) varit) then + if array_for_all (noccur_with_meta n nbfix) varit then + let nbfix = Array.length vdefs in let env' = push_rec_types recdef env in - (Array.iter (check_rec_call env' alreadygrd (n+1) vlra) vdefs; + (Array.iter (check_rec_call env' alreadygrd (n+nbfix) vlra) vdefs; List.iter (check_rec_call env alreadygrd n vlra) args) else raise (CoFixGuardError (env,RecCallInTypeOfDef c)) diff -Nru coq-8.4pl3dfsg/checker/inductive.mli coq-8.4pl4dfsg/checker/inductive.mli --- coq-8.4pl3dfsg/checker/inductive.mli 2013-12-21 08:03:14.000000000 +0000 +++ coq-8.4pl4dfsg/checker/inductive.mli 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* Sun, 27 Jul 2014 15:25:03 +0200 + coq (8.4pl3dfsg-1) unstable; urgency=medium * New upstream release diff -Nru coq-8.4pl3dfsg/debian/compat coq-8.4pl4dfsg/debian/compat --- coq-8.4pl3dfsg/debian/compat 2014-01-19 14:09:58.000000000 +0000 +++ coq-8.4pl4dfsg/debian/compat 2014-07-27 11:38:22.000000000 +0000 @@ -1 +1 @@ -7 +9 diff -Nru coq-8.4pl3dfsg/debian/control coq-8.4pl4dfsg/debian/control --- coq-8.4pl3dfsg/debian/control 2014-01-19 14:09:58.000000000 +0000 +++ coq-8.4pl4dfsg/debian/control 2014-07-27 11:38:22.000000000 +0000 @@ -6,9 +6,9 @@ Ralf Treinen , Samuel Mimram , Stéphane Glondu -Standards-Version: 3.9.2 +Standards-Version: 3.9.5 Build-Depends: - debhelper (>= 7.2.11~), + debhelper (>= 9), dh-ocaml (>= 0.9.5~), ocaml-nox (>= 4), ocaml-best-compilers, diff -Nru coq-8.4pl3dfsg/debian/copyright coq-8.4pl4dfsg/debian/copyright --- coq-8.4pl3dfsg/debian/copyright 2014-01-19 14:09:58.000000000 +0000 +++ coq-8.4pl4dfsg/debian/copyright 2014-07-27 08:36:23.000000000 +0000 @@ -1,29 +1,20 @@ +Format: http://www.debian.org/doc/packaging-manuals/copyright-format/1.0/ Packaged-By: Fernando Sanchez Packaged-Date: Fri, 03 Dec 1999 22:06:04 +0100 -Original-Source-Location: http://coq.inria.fr/ +Source: http://coq.inria.fr/ Files: * -Copyright: © 1999-2010 The Coq development team, - INRIA, CNRS, University Paris Sud, - University Paris 7, Ecole Polytechnique. +Copyright: 1999-2014 The Coq development team, INRIA, CNRS, University Paris Sud, University Paris 7, Ecole Polytechnique License: LGPL-2.1 - This product includes also software developed by - Pierre Crégut, France Telecom R & D (plugins/omega and plugins/romega) - Pierre Courtieu and Julien Forest, CNAM (plugins/funind) - Claudio Sacerdoti Coen, HELM, University of Bologna, (plugins/xml) - Pierre Corbineau, Radbout University, Nijmegen (declarative mode) - John Harrison, University of Cambridge (csdp wrapper) - - The file /usr/share/doc/coq/CREDITS.gz contains a list of contributors. - - The Coq Proof Assistant is distributed under the terms of the GNU - Lesser General Public Licence, version 2.1, see - /usr/share/common-licenses/LGPL-2.1. - Files: debian/* -Copyright: © 1999-2000 Fernando Sanchez - © 2001-2002 Judicael Courant - © 2004-2009 Samuel Mimram - © 2008-2010 Stéphane Glondu +Copyright: 1999-2000 Fernando Sanchez + 2001-2002 Judicael Courant + 2004-2009 Samuel Mimram + 2008-2014 Stéphane Glondu +License: LGPL-2.1 + License: LGPL-2.1 + The Coq Proof Assistant is distributed under the terms of the GNU + Lesser General Public Licence, version 2.1, see + `/usr/share/common-licenses/LGPL-2.1'. diff -Nru coq-8.4pl3dfsg/debian/rules coq-8.4pl4dfsg/debian/rules --- coq-8.4pl3dfsg/debian/rules 2014-01-19 15:15:52.000000000 +0000 +++ coq-8.4pl4dfsg/debian/rules 2014-07-27 13:23:48.000000000 +0000 @@ -22,7 +22,7 @@ PACKAGES := $(shell dh_listpackages) -COQ_VERSION := 8.4pl3 +COQ_VERSION := 8.4pl4 COQ_ABI := $(COQ_VERSION)+$(OCAML_ABI) CONFIGUREOPTS := --arch Linux --prefix /usr --mandir /usr/share/man \ @@ -36,13 +36,13 @@ -e 's%@CoqABI@%$(COQ_ABI)%' %: - +dh --with ocaml $@ + +dh $@ --with ocaml # There is already a file named "build" in upstream sources, so the # above rule is never called. We make it explicitly a phony rule here. .PHONY: build build: - +dh --with ocaml $@ + +dh $@ --with ocaml .PHONY: override_dh_auto_configure override_dh_auto_configure: diff -Nru coq-8.4pl3dfsg/dev/db_printers.ml coq-8.4pl4dfsg/dev/db_printers.ml --- coq-8.4pl3dfsg/dev/db_printers.ml 2013-12-21 08:03:14.000000000 +0000 +++ coq-8.4pl4dfsg/dev/db_printers.ml 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* [] diff -Nru coq-8.4pl3dfsg/ide/coq.mli coq-8.4pl4dfsg/ide/coq.mli --- coq-8.4pl3dfsg/ide/coq.mli 2013-12-21 08:03:14.000000000 +0000 +++ coq-8.4pl4dfsg/ide/coq.mli 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* n then - user_err_loc (loc,"",str "Projection has not the right number of explicit parameters."); + user_err_loc (loc,"",str "Projection does not have the right number of explicit parameters."); with Not_found -> user_err_loc (loc,"",pr_global_env Idset.empty ref ++ str " is not a registered projection.")) diff -Nru coq-8.4pl3dfsg/interp/constrintern.mli coq-8.4pl4dfsg/interp/constrintern.mli --- coq-8.4pl3dfsg/interp/constrintern.mli 2013-12-21 08:03:14.000000000 +0000 +++ coq-8.4pl4dfsg/interp/constrintern.mli 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* (open_constr_expr,rlevel) abstract_argument_type -val globwit_open_constr_gen : bool -> (open_glob_constr,glevel) abstract_argument_type -val wit_open_constr_gen : bool -> (open_constr,tlevel) abstract_argument_type +val rawwit_open_constr_gen : bool * bool -> (open_constr_expr,rlevel) abstract_argument_type +val globwit_open_constr_gen : bool * bool -> (open_glob_constr,glevel) abstract_argument_type +val wit_open_constr_gen : bool * bool -> (open_constr,tlevel) abstract_argument_type val rawwit_open_constr : (open_constr_expr,rlevel) abstract_argument_type val globwit_open_constr : (open_glob_constr,glevel) abstract_argument_type @@ -195,6 +195,10 @@ val globwit_casted_open_constr : (open_glob_constr,glevel) abstract_argument_type val wit_casted_open_constr : (open_constr,tlevel) abstract_argument_type +val rawwit_open_constr_wTC : (open_constr_expr,rlevel) abstract_argument_type +val globwit_open_constr_wTC : (open_glob_constr,glevel) abstract_argument_type +val wit_open_constr_wTC : (open_constr,tlevel) abstract_argument_type + val rawwit_constr_with_bindings : (constr_expr with_bindings,rlevel) abstract_argument_type val globwit_constr_with_bindings : (glob_constr_and_expr with_bindings,glevel) abstract_argument_type val wit_constr_with_bindings : (constr with_bindings sigma,tlevel) abstract_argument_type @@ -280,7 +284,7 @@ | ConstrArgType | ConstrMayEvalArgType | QuantHypArgType - | OpenConstrArgType of bool + | OpenConstrArgType of bool * bool | ConstrWithBindingsArgType | BindingsArgType | RedExprArgType diff -Nru coq-8.4pl3dfsg/interp/implicit_quantifiers.ml coq-8.4pl4dfsg/interp/implicit_quantifiers.ml --- coq-8.4pl3dfsg/interp/implicit_quantifiers.ml 2013-12-21 08:03:14.000000000 +0000 +++ coq-8.4pl4dfsg/interp/implicit_quantifiers.ml 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* raise (LocalArity None) in srec (push_rel (na1,None,a1) env) t ar' (union_constraints u univ) - | Prod (_,a1,a2), [] -> (* whnf of t was not needed here! *) - let ksort = match kind_of_term (whd_betadeltaiota env a2) with - | Sort s -> family_of_sort s - | _ -> raise (LocalArity None) in - let dep_ind = build_dependent_inductive ind specif params in - let univ = - try conv env a1 dep_ind - with NotConvertible -> raise (LocalArity None) in - check_allowed_sort ksort specif; - union_constraints u univ + (* The last Prod domain is the type of the scrutinee *) + | Prod (na1,a1,a2), [] -> (* whnf of t was not needed here! *) + let env' = push_rel (na1,None,a1) env in + let ksort = match kind_of_term (whd_betadeltaiota env' a2) with + | Sort s -> family_of_sort s + | _ -> raise (LocalArity None) in + let dep_ind = build_dependent_inductive ind specif params in + let univ = + try conv env a1 dep_ind + with NotConvertible -> raise (LocalArity None) in + check_allowed_sort ksort specif; + union_constraints u univ | _, (_,Some _,_ as d)::ar' -> - srec (push_rel d env) (lift 1 pt') ar' u + srec (push_rel d env) (lift 1 pt') ar' u | _ -> raise (LocalArity None) in @@ -895,12 +897,12 @@ raise (CoFixGuardError (env,RecCallInTypeOfAbstraction a)) | CoFix (j,(_,varit,vdefs as recdef)) -> - if (List.for_all (noccur_with_meta n nbfix) args) + if List.for_all (noccur_with_meta n nbfix) args then - let nbfix = Array.length vdefs in - if (array_for_all (noccur_with_meta n nbfix) varit) then + if array_for_all (noccur_with_meta n nbfix) varit then + let nbfix = Array.length vdefs in let env' = push_rec_types recdef env in - (Array.iter (check_rec_call env' alreadygrd (n+1) vlra) vdefs; + (Array.iter (check_rec_call env' alreadygrd (n+nbfix) vlra) vdefs; List.iter (check_rec_call env alreadygrd n vlra) args) else raise (CoFixGuardError (env,RecCallInTypeOfDef c)) diff -Nru coq-8.4pl3dfsg/kernel/inductive.mli coq-8.4pl4dfsg/kernel/inductive.mli --- coq-8.4pl3dfsg/kernel/inductive.mli 2013-12-21 08:03:14.000000000 +0000 +++ coq-8.4pl4dfsg/kernel/inductive.mli 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* full_add_module mb env) diff -Nru coq-8.4pl3dfsg/kernel/safe_typing.mli coq-8.4pl4dfsg/kernel/safe_typing.mli --- coq-8.4pl3dfsg/kernel/safe_typing.mli 2013-12-21 08:03:14.000000000 +0000 +++ coq-8.4pl4dfsg/kernel/safe_typing.mli 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* coqlib | None -> coqroot in - if Sys.file_exists (Filename.concat coqlib file) + if Sys.file_exists (coqlib//file) then coqlib else Util.error "cannot guess a path for Coq libraries; please use -coqlib option") @@ -54,18 +56,14 @@ Util.split_string_at sep p let xdg_data_home = - Filename.concat - (System.getenv_else "XDG_DATA_HOME" (Filename.concat System.home ".local/share")) - "coq" + (System.getenv_else "XDG_DATA_HOME" (System.home//".local/share"))//"coq" let xdg_config_home = - Filename.concat - (System.getenv_else "XDG_CONFIG_HOME" (Filename.concat System.home ".config")) - "coq" + (System.getenv_else "XDG_CONFIG_HOME" (System.home//".config"))//"coq" let xdg_data_dirs = (try - List.map (fun dir -> Filename.concat dir "coq") (path_to_list (Sys.getenv "XDG_DATA_DIRS")) + List.map (fun dir -> dir//"coq") (path_to_list (Sys.getenv "XDG_DATA_DIRS")) with Not_found -> ["/usr/local/share/coq";"/usr/share/coq"]) @ (match Coq_config.datadir with |None -> [] |Some datadir -> [datadir]) @@ -84,7 +82,7 @@ match l with | [] -> raise Not_found | p :: tl -> - if Sys.file_exists (Filename.concat p f) + if Sys.file_exists (p//f) then p else which tl f @@ -108,7 +106,7 @@ then Coq_config.camllib else let camlbin = camlbin () in - let com = (Filename.concat camlbin "ocamlc") ^ " -where" in + let com = (camlbin//"ocamlc") ^ " -where" in let _,res = System.run_command (fun x -> x) (fun _ -> ()) com in Util.strip res @@ -117,7 +115,7 @@ if !Flags.boot then Coq_config.camlp4bin else try guess_camlp4bin () with e when e <> Sys.Break -> let cb = camlbin () in - if Sys.file_exists (Filename.concat cb (exe Coq_config.camlp4)) then cb + if Sys.file_exists (cb//(exe Coq_config.camlp4)) then cb else Coq_config.camlp4bin let camlp4lib () = @@ -125,7 +123,7 @@ then Coq_config.camlp4lib else let camlp4bin = camlp4bin () in - let com = (Filename.concat camlp4bin Coq_config.camlp4) ^ " -where" in + let com = (camlp4bin//Coq_config.camlp4) ^ " -where" in let ex,res = System.run_command (fun x -> x) (fun _ -> ()) com in match ex with |Unix.WEXITED 0 -> Util.strip res diff -Nru coq-8.4pl3dfsg/lib/envars.mli coq-8.4pl4dfsg/lib/envars.mli --- coq-8.4pl3dfsg/lib/envars.mli 2013-12-21 08:03:14.000000000 +0000 +++ coq-8.4pl4dfsg/lib/envars.mli 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <:expr< Genarg.rawwit_constr_may_eval >> | QuantHypArgType -> <:expr< Genarg.rawwit_quant_hyp >> | RedExprArgType -> <:expr< Genarg.rawwit_red_expr >> - | OpenConstrArgType b -> <:expr< Genarg.rawwit_open_constr_gen $mlexpr_of_bool b$ >> + | OpenConstrArgType (b1,b2) -> <:expr< Genarg.rawwit_open_constr_gen ($mlexpr_of_bool b1$,$mlexpr_of_bool b2$) >> | ConstrWithBindingsArgType -> <:expr< Genarg.rawwit_constr_with_bindings >> | BindingsArgType -> <:expr< Genarg.rawwit_bindings >> | List0ArgType t -> <:expr< Genarg.wit_list0 $make_rawwit loc t$ >> @@ -62,7 +62,7 @@ | ConstrArgType -> <:expr< Genarg.globwit_constr >> | ConstrMayEvalArgType -> <:expr< Genarg.globwit_constr_may_eval >> | RedExprArgType -> <:expr< Genarg.globwit_red_expr >> - | OpenConstrArgType b -> <:expr< Genarg.globwit_open_constr_gen $mlexpr_of_bool b$ >> + | OpenConstrArgType (b1,b2) -> <:expr< Genarg.globwit_open_constr_gen ($mlexpr_of_bool b1$,$mlexpr_of_bool b2$) >> | ConstrWithBindingsArgType -> <:expr< Genarg.globwit_constr_with_bindings >> | BindingsArgType -> <:expr< Genarg.globwit_bindings >> | List0ArgType t -> <:expr< Genarg.wit_list0 $make_globwit loc t$ >> @@ -92,7 +92,7 @@ | ConstrArgType -> <:expr< Genarg.wit_constr >> | ConstrMayEvalArgType -> <:expr< Genarg.wit_constr_may_eval >> | RedExprArgType -> <:expr< Genarg.wit_red_expr >> - | OpenConstrArgType b -> <:expr< Genarg.wit_open_constr_gen $mlexpr_of_bool b$ >> + | OpenConstrArgType (b1,b2) -> <:expr< Genarg.wit_open_constr_gen ($mlexpr_of_bool b1$,$mlexpr_of_bool b2$) >> | ConstrWithBindingsArgType -> <:expr< Genarg.wit_constr_with_bindings >> | BindingsArgType -> <:expr< Genarg.wit_bindings >> | List0ArgType t -> <:expr< Genarg.wit_list0 $make_wit loc t$ >> diff -Nru coq-8.4pl3dfsg/parsing/egrammar.ml coq-8.4pl4dfsg/parsing/egrammar.ml --- coq-8.4pl3dfsg/parsing/egrammar.ml 2013-12-21 08:03:14.000000000 +0000 +++ coq-8.4pl4dfsg/parsing/egrammar.ml 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* ((),c) ] ] ; + open_constr_wTC: + [ [ c = constr -> ((),c) ] ] + ; casted_open_constr: [ [ c = constr -> ((),c) ] ] ; diff -Nru coq-8.4pl3dfsg/parsing/g_vernac.ml4 coq-8.4pl4dfsg/parsing/g_vernac.ml4 --- coq-8.4pl3dfsg/parsing/g_vernac.ml4 2013-12-21 08:03:14.000000000 +0000 +++ coq-8.4pl4dfsg/parsing/g_vernac.ml4 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* VernacImport (false,qidl) | IDENT "Export"; qidl = LIST1 global -> VernacImport (true,qidl) - | IDENT "Include"; e = module_expr_inl; l = LIST0 ext_module_expr -> + | IDENT "Include"; e = module_type_inl; l = LIST0 ext_module_expr -> VernacInclude(e::l) | IDENT "Include"; "Type"; e = module_type_inl; l = LIST0 ext_module_type -> Flags.if_verbose @@ -842,6 +842,7 @@ -> PrintCoercionPaths (s,t) | IDENT "Canonical"; IDENT "Projections" -> PrintCanonicalConversions | IDENT "Tables" -> PrintTables + | IDENT "Options" -> PrintTables (* A Synonymous to Tables *) | IDENT "Hint" -> PrintHintGoal | IDENT "Hint"; qid = smart_global -> PrintHint qid | IDENT "Hint"; "*" -> PrintHintDb diff -Nru coq-8.4pl3dfsg/parsing/g_xml.ml4 coq-8.4pl4dfsg/parsing/g_xml.ml4 --- coq-8.4pl3dfsg/parsing/g_xml.ml4 2013-12-21 08:03:14.000000000 +0000 +++ coq-8.4pl4dfsg/parsing/g_xml.ml4 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* Gram.entry table *) (* Typically for tactic user extensions *) let open_constr = - make_gen_entry utactic (rawwit_open_constr_gen false) "open_constr" + make_gen_entry utactic (rawwit_open_constr_gen (false,false)) "open_constr" let casted_open_constr = - make_gen_entry utactic (rawwit_open_constr_gen true) "casted_open_constr" + make_gen_entry utactic (rawwit_open_constr_gen (true,false)) "casted_open_constr" + let open_constr_wTC = + make_gen_entry utactic (rawwit_open_constr_gen (false,true)) "open_constr_wTC" let constr_with_bindings = make_gen_entry utactic rawwit_constr_with_bindings "constr_with_bindings" let bindings = diff -Nru coq-8.4pl3dfsg/parsing/pcoq.mli coq-8.4pl4dfsg/parsing/pcoq.mli --- coq-8.4pl3dfsg/parsing/pcoq.mli 2013-12-21 08:03:14.000000000 +0000 +++ coq-8.4pl4dfsg/parsing/pcoq.mli 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* pr_red_expr (prc,prlc,pr_or_by_notation prref,prpat) (out_gen rawwit_red_expr x) - | OpenConstrArgType b -> prc (snd (out_gen (rawwit_open_constr_gen b) x)) + | OpenConstrArgType (b1,b2) -> prc (snd (out_gen (rawwit_open_constr_gen (b1,b2)) x)) | ConstrWithBindingsArgType -> pr_with_bindings prc prlc (out_gen rawwit_constr_with_bindings x) | BindingsArgType -> @@ -195,7 +195,7 @@ pr_red_expr (prc,prlc,pr_or_var (pr_and_short_name pr_evaluable_reference),prpat) (out_gen globwit_red_expr x) - | OpenConstrArgType b -> prc (snd (out_gen (globwit_open_constr_gen b) x)) + | OpenConstrArgType (b1,b2) -> prc (snd (out_gen (globwit_open_constr_gen (b1,b2)) x)) | ConstrWithBindingsArgType -> pr_with_bindings prc prlc (out_gen globwit_constr_with_bindings x) | BindingsArgType -> @@ -236,7 +236,7 @@ | RedExprArgType -> pr_red_expr (prc,prlc,pr_evaluable_reference,prpat) (out_gen wit_red_expr x) - | OpenConstrArgType b -> prc (snd (out_gen (wit_open_constr_gen b) x)) + | OpenConstrArgType (b1,b2) -> prc (snd (out_gen (wit_open_constr_gen (b1,b2)) x)) | ConstrWithBindingsArgType -> let (c,b) = (out_gen wit_constr_with_bindings x).Evd.it in pr_with_bindings prc prlc (c,b) diff -Nru coq-8.4pl3dfsg/parsing/pptactic.mli coq-8.4pl4dfsg/parsing/pptactic.mli --- coq-8.4pl3dfsg/parsing/pptactic.mli 2013-12-21 08:03:14.000000000 +0000 +++ coq-8.4pl4dfsg/parsing/pptactic.mli 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* (mt ()) | Some c -> (* Force evaluation *) - let pb = pr_lconstr_env env c in + let pb = pr_lconstr_core true env c in let pb = if isCast c then surround pb else pb in (str" := " ++ pb ++ cut () ) in - let pt = pr_ltype_env env typ in + let pt = pr_ltype_core true env typ in let ptyp = (str" : " ++ pt) in (pr_id id ++ hov 0 (pbody ++ ptyp)) @@ -217,10 +217,10 @@ | None -> mt () | Some c -> (* Force evaluation *) - let pb = pr_lconstr_env env c in + let pb = pr_lconstr_core true env c in let pb = if isCast c then surround pb else pb in (str":=" ++ spc () ++ pb ++ spc ()) in - let ptyp = pr_ltype_env env typ in + let ptyp = pr_ltype_core true env typ in match na with | Anonymous -> hov 0 (str"<>" ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp) | Name id -> hov 0 (pr_id id ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp) diff -Nru coq-8.4pl3dfsg/parsing/printer.mli coq-8.4pl4dfsg/parsing/printer.mli --- coq-8.4pl3dfsg/parsing/printer.mli 2013-12-21 08:03:14.000000000 +0000 +++ coq-8.4pl4dfsg/parsing/printer.mli 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <:expr< Genarg.VarArgType >> | Genarg.StringArgType -> <:expr< Genarg.StringArgType >> | Genarg.QuantHypArgType -> <:expr< Genarg.QuantHypArgType >> - | Genarg.OpenConstrArgType b -> <:expr< Genarg.OpenConstrArgType $mlexpr_of_bool b$ >> + | Genarg.OpenConstrArgType (b1,b2) -> <:expr< Genarg.OpenConstrArgType ($mlexpr_of_bool b1$, $mlexpr_of_bool b2$) >> | Genarg.ConstrWithBindingsArgType -> <:expr< Genarg.ConstrWithBindingsArgType >> | Genarg.BindingsArgType -> <:expr< Genarg.BindingsArgType >> | Genarg.RedExprArgType -> <:expr< Genarg.RedExprArgType >> diff -Nru coq-8.4pl3dfsg/parsing/q_util.ml4 coq-8.4pl4dfsg/parsing/q_util.ml4 --- coq-8.4pl3dfsg/parsing/q_util.ml4 2013-12-21 08:03:14.000000000 +0000 +++ coq-8.4pl4dfsg/parsing/q_util.ml4 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* (t, l) | Construct _ -> (t,l) @@ -576,7 +576,7 @@ onLastHypId (fun heq_id -> tclTHENLIST [ (* Then the new hypothesis *) tclMAP introduction_no_check dyn_infos.rec_hyps; - (* observe_tac "after_introduction" *)(fun g' -> + observe_tac "after_introduction" (fun g' -> (* We get infos on the equations introduced*) let new_term_value_eq = pf_type_of g' (mkVar heq_id) in (* compute the new value of the body *) @@ -603,7 +603,7 @@ } in clean_goal_with_heq ptes_infos continue_tac new_infos g' - )]) + )]) ] g diff -Nru coq-8.4pl3dfsg/plugins/funind/g_indfun.ml4 coq-8.4pl4dfsg/plugins/funind/g_indfun.ml4 --- coq-8.4pl3dfsg/plugins/funind/g_indfun.ml4 2013-12-21 08:03:14.000000000 +0000 +++ coq-8.4pl4dfsg/plugins/funind/g_indfun.ml4 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* + match pat with + | Genarg.IntroIdentifier id -> add id acc + | _ -> anomaly "Not an identifier" + ) + (List.nth intro_pats (pred i)) + empty + in let prove_branche i g = (* We get the identifiers of this branch *) - let this_branche_ids = - List.fold_right - (fun (_,pat) acc -> - match pat with - | Genarg.IntroIdentifier id -> Idset.add id acc - | _ -> anomaly "Not an identifier" - ) - (List.nth intro_pats (pred i)) - Idset.empty - in (* and get the real args of the branch by unfolding the defined constant *) let pre_args,pre_tac = List.fold_right (fun (id,b,t) (pre_args,pre_tac) -> - if Idset.mem id this_branche_ids + if Idset.mem id (this_branche_ids Idset.empty Idset.add i) then match b with - | None -> (id::pre_args,pre_tac) + | None -> + (id::pre_args,pre_tac) | Some b -> (pre_args, tclTHEN (h_reduce (Glob_term.Unfold([Glob_term.all_occurrences_expr,EvalVarRef id])) allHyps) pre_tac @@ -347,8 +351,8 @@ when (eq_constr eq eq_ind) && array_exists (eq_constr graph') graphs_constr -> - ((mkApp(mkVar hid,[|args.(2);(mkApp(eq_construct,[|args.(0);args.(2)|]))|])) - ::args.(2)::acc) + ((mkApp(mkVar hid,[|args.(2);(mkApp(eq_construct,[|args.(0);args.(2)|]))|])) + ::args.(2)::acc) | _ -> mkVar hid :: acc end | _ -> mkVar hid :: acc @@ -390,7 +394,7 @@ | [res;hres] -> res,hres | _ -> assert false in - observe (str "constructor := " ++ Printer.pr_lconstr_env (pf_env g) app_constructor); + observe_tac_msg (str "constructor := " ++ Printer.pr_lconstr_env (pf_env g) app_constructor) ( tclTHENSEQ [ @@ -455,11 +459,10 @@ fun g -> observe (pr_constr_with_binding (Printer.pr_lconstr_env (pf_env g)) (mkVar principle_id,bindings)); - functional_induction false (applist(funs_constr.(i),List.map mkVar args_names)) - (Some (mkVar principle_id,bindings)) - pat g + h_apply false false [dummy_loc,(mkVar principle_id,bindings)] g )) - (fun i g -> observe_tac ("proving branche "^string_of_int i) (prove_branche i) g ) + (fun i g -> observe_tac ("proving branche "^string_of_int i) + (tclTHEN (tclMAP h_intro (this_branche_ids [] (fun a b -> a::b) i)) (prove_branche i)) g ) ] g diff -Nru coq-8.4pl3dfsg/plugins/funind/merge.ml coq-8.4pl4dfsg/plugins/funind/merge.ml --- coq-8.4pl3dfsg/plugins/funind/merge.ml 2013-12-21 08:03:14.000000000 +0000 +++ coq-8.4pl4dfsg/plugins/funind/merge.ml 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* let (f,_) = decompose_app t in eq_constr f (well_founded ()) - | _ -> assert false + | _ -> false in let compare t1 t2 = let b1,b2= is_well_founded t1,is_well_founded t2 in diff -Nru coq-8.4pl3dfsg/plugins/funind/Recdef.v coq-8.4pl4dfsg/plugins/funind/Recdef.v --- coq-8.4pl3dfsg/plugins/funind/Recdef.v 2013-12-21 08:03:14.000000000 +0000 +++ coq-8.4pl4dfsg/plugins/funind/Recdef.v 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* = 8.5, this option is set by default. +*) + let read f () = !f let write f x = f:=x @@ -81,6 +98,14 @@ optread = read old_style_flag; optwrite = write old_style_flag } +let _ = + declare_bool_option + { optsync = true; + optdepr = false; + optname = "Omega automatic reset of generated names"; + optkey = ["Stable";"Omega"]; + optread = read reset_flag; + optwrite = write reset_flag } let all_time = timing "Omega " let solver_time = timing "Solver " @@ -89,30 +114,35 @@ let simpl_time = timing "Simpl " let generalize_time = timing "Generalize" +let intref, reset_all_references = + let refs = ref [] in + (fun n -> let r = ref n in refs := (r,n) :: !refs; r), + (fun () -> List.iter (fun (r,n) -> r:=n) !refs) + let new_identifier = - let cpt = ref 0 in + let cpt = intref 0 in (fun () -> let s = "Omega" ^ string_of_int !cpt in incr cpt; id_of_string s) let new_identifier_state = - let cpt = ref 0 in + let cpt = intref 0 in (fun () -> let s = make_ident "State" (Some !cpt) in incr cpt; s) let new_identifier_var = - let cpt = ref 0 in + let cpt = intref 0 in (fun () -> let s = "Zvar" ^ string_of_int !cpt in incr cpt; id_of_string s) let new_id = - let cpt = ref 0 in fun () -> incr cpt; !cpt + let cpt = intref 0 in fun () -> incr cpt; !cpt let new_var_num = - let cpt = ref 1000 in (fun () -> incr cpt; !cpt) + let cpt = intref 1000 in (fun () -> incr cpt; !cpt) let new_var = - let cpt = ref 0 in fun () -> incr cpt; Nameops.make_ident "WW" (Some !cpt) + let cpt = intref 0 in fun () -> incr cpt; Nameops.make_ident "WW" (Some !cpt) let display_var i = Printf.sprintf "X%d" i -let intern_id,unintern_id = +let intern_id,unintern_id,reset_intern_tables = let cpt = ref 0 in let table = Hashtbl.create 7 and co_table = Hashtbl.create 7 in (fun (name : identifier) -> @@ -124,7 +154,8 @@ (fun idx -> try Hashtbl.find co_table idx with Not_found -> let v = new_var () in - Hashtbl.add table v idx; Hashtbl.add co_table idx v; v) + Hashtbl.add table v idx; Hashtbl.add co_table idx v; v), + (fun () -> cpt := 0; Hashtbl.clear table) let mk_then = tclTHENLIST @@ -141,19 +172,28 @@ in loop -let tag_hypothesis,tag_of_hyp, hyp_of_tag = +let tag_hypothesis,tag_of_hyp, hyp_of_tag, clear_tags = let l = ref ([]:(identifier * int) list) in (fun h id -> l := (h,id):: !l), (fun h -> try List.assoc h !l with Not_found -> failwith "tag_hypothesis"), - (fun h -> try rev_assoc h !l with Not_found -> failwith "tag_hypothesis") + (fun h -> try rev_assoc h !l with Not_found -> failwith "tag_hypothesis"), + (fun () -> l := []) -let hide_constr,find_constr,clear_tables,dump_tables = +let hide_constr,find_constr,clear_constr_tables,dump_tables = let l = ref ([]:(constr * (identifier * identifier * bool)) list) in (fun h id eg b -> l := (h,(id,eg,b)):: !l), (fun h -> try list_assoc_f eq_constr h !l with Not_found -> failwith "find_contr"), (fun () -> l := []), (fun () -> !l) +let reset_all () = + if !reset_flag then begin + reset_all_references (); + reset_intern_tables (); + clear_tags (); + clear_constr_tables () + end + (* Lazy evaluation is used for Coq constants, because this code is evaluated before the compiled modules are loaded. To use the constant Zplus, one must type "Lazy.force coq_Zplus" @@ -1388,7 +1428,7 @@ tclTHEN (tclTRY (clear [id])) (intro_using id) let coq_omega gl = - clear_tables (); + clear_constr_tables (); let tactic_normalisation, system = List.fold_left (destructure_omega gl) ([],[]) (pf_hyps_types gl) in let prelude,sys = @@ -1814,6 +1854,7 @@ let omega_solver gl = Coqlib.check_required_library ["Coq";"omega";"Omega"]; + reset_all (); let result = destructure_goal gl in (* if !display_time_flag then begin text_time (); flush Pervasives.stdout end; *) diff -Nru coq-8.4pl3dfsg/plugins/omega/g_omega.ml4 coq-8.4pl4dfsg/plugins/omega/g_omega.ml4 --- coq-8.4pl3dfsg/plugins/omega/g_omega.ml4 2013-12-21 08:03:14.000000000 +0000 +++ coq-8.4pl4dfsg/plugins/omega/g_omega.ml4 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* - let (evd',j) = Coercion.inh_conv_coerce_to loc env !isevars j p in + let (evd',j) = Coercion.inh_conv_coerce_to true loc env !isevars j p in isevars := evd'; j | None -> j diff -Nru coq-8.4pl3dfsg/plugins/subtac/subtac_cases.mli coq-8.4pl4dfsg/plugins/subtac/subtac_cases.mli --- coq-8.4pl3dfsg/plugins/subtac/subtac_cases.mli 2013-12-21 08:03:14.000000000 +0000 +++ coq-8.4pl4dfsg/plugins/subtac/subtac_cases.mli 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* anomaly "apply_coercion" - let inh_app_fun env isevars j = + let inh_app_fun _ env isevars j = let isevars = ref isevars in let t = hnf env !isevars j.uj_type in match kind_of_term t with @@ -481,8 +481,8 @@ | Some (init, cur) -> (evd, cj) - let inh_conv_coerce_to = inh_conv_coerce_to_gen false - let inh_conv_coerce_rigid_to = inh_conv_coerce_to_gen true + let inh_conv_coerce_to _ = inh_conv_coerce_to_gen false + let inh_conv_coerce_rigid_to _ = inh_conv_coerce_to_gen true let inh_conv_coerces_to loc env isevars t ((abs, t') as _tycon) = let nabsinit, nabs = diff -Nru coq-8.4pl3dfsg/plugins/subtac/subtac.ml coq-8.4pl4dfsg/plugins/subtac/subtac.ml --- coq-8.4pl3dfsg/plugins/subtac/subtac.ml 2013-12-21 08:03:14.000000000 +0000 +++ coq-8.4pl4dfsg/plugins/subtac/subtac.ml 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* j - | Some t -> evd_comb2 (Coercion.inh_conv_coerce_to loc env) evdref j t + | Some t -> evd_comb2 (Coercion.inh_conv_coerce_to resolve_tc loc env) evdref j t let push_rels vars env = List.fold_right push_rel vars env @@ -188,11 +188,14 @@ (* [pretype tycon env evdref lvar lmeta cstr] attempts to type [cstr] *) (* in environment [env], with existential variables [( evdref)] and *) (* the type constraint tycon *) - let rec pretype (tycon : type_constraint) env evdref lvar c = + let rec pretype resolve_tc (tycon : type_constraint) env evdref lvar c = (* let _ = try Subtac_utils.trace (str "pretype " ++ Subtac_utils.my_print_glob_constr env c ++ *) (* str " with tycon " ++ Evarutil.pr_tycon env tycon) *) (* with _ -> () *) (* in *) + let pretype = pretype resolve_tc in + let pretype_type = pretype_type resolve_tc in + let inh_conv_coerce_to_tycon = inh_conv_coerce_to_tycon resolve_tc in match c with | GRef (loc,ref) -> inh_conv_coerce_to_tycon loc env evdref @@ -335,7 +338,7 @@ | [] -> resj | c::rest -> let argloc = loc_of_glob_constr c in - let resj = evd_comb1 (Coercion.inh_app_fun env) evdref resj in + let resj = evd_comb1 (Coercion.inh_app_fun resolve_tc env) evdref resj in let resty = whd_betadeltaiota env !evdref resj.uj_type in match kind_of_term resty with | Prod (na,c1,c2) -> @@ -557,7 +560,7 @@ inh_conv_coerce_to_tycon loc env evdref cj tycon (* [pretype_type valcon env evdref lvar c] coerces [c] into a type *) - and pretype_type valcon env evdref lvar = function + and pretype_type resolve_tc valcon env evdref lvar = function | GHole loc -> (match valcon with | Some v -> @@ -577,7 +580,7 @@ { utj_val = e_new_evar evdref env ~src:loc (mkSort s); utj_type = s}) | c -> - let j = pretype empty_tycon env evdref lvar c in + let j = pretype resolve_tc empty_tycon env evdref lvar c in let loc = loc_of_glob_constr c in let tj = evd_comb1 (Coercion.inh_coerce_to_sort loc env) evdref j in match valcon with @@ -592,9 +595,9 @@ let c' = match kind with | OfType exptyp -> let tycon = match exptyp with None -> empty_tycon | Some t -> mk_tycon t in - (pretype tycon env evdref lvar c).uj_val + (pretype resolve_classes tycon env evdref lvar c).uj_val | IsType -> - (pretype_type empty_valcon env evdref lvar c).utj_val + (pretype_type resolve_classes empty_valcon env evdref lvar c).utj_val in if resolve_classes then (try @@ -616,14 +619,14 @@ let understand_judgment sigma env c = let evdref = ref (create_evar_defs sigma) in - let j = pretype empty_tycon env evdref ([],[]) c in + let j = pretype true empty_tycon env evdref ([],[]) c in let evd = consider_remaining_unif_problems env !evdref in let j = j_nf_evar evd j in check_evars env sigma evd (mkCast(j.uj_val,DEFAULTcast, j.uj_type)); j let understand_judgment_tcc evdref env c = - let j = pretype empty_tycon env evdref ([],[]) c in + let j = pretype true empty_tycon env evdref ([],[]) c in j_nf_evar !evdref j (* Raw calls to the unsafe inference machine: boolean says if we must diff -Nru coq-8.4pl3dfsg/plugins/subtac/subtac_pretyping.ml coq-8.4pl4dfsg/plugins/subtac/subtac_pretyping.ml --- coq-8.4pl3dfsg/plugins/subtac/subtac_pretyping.ml 2013-12-21 08:03:14.000000000 +0000 +++ coq-8.4pl4dfsg/plugins/subtac/subtac_pretyping.ml 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* - let (evd',j) = Coercion.inh_conv_coerce_to loc env !evdref j p in + let (evd',j) = Coercion.inh_conv_coerce_to true loc env !evdref j p in evdref := evd'; j | None -> j diff -Nru coq-8.4pl3dfsg/pretyping/cases.mli coq-8.4pl4dfsg/pretyping/cases.mli --- coq-8.4pl3dfsg/pretyping/cases.mli 2013-12-21 08:03:14.000000000 +0000 +++ coq-8.4pl4dfsg/pretyping/cases.mli 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* evar_map -> unsafe_judgment -> evar_map * unsafe_judgment + bool -> env -> evar_map -> unsafe_judgment -> evar_map * unsafe_judgment (* [inh_coerce_to_sort env evd j] coerces [j] to a type; i.e. it inserts a coercion into [j], if needed, in such a way it gets as @@ -57,10 +57,10 @@ (* [inh_conv_coerce_to loc env evd j t] coerces [j] to an object of type [t]; i.e. it inserts a coercion into [j], if needed, in such a way [t] and [j.uj_type] are convertible; it fails if no coercion is applicable *) - val inh_conv_coerce_to : loc -> + val inh_conv_coerce_to : bool -> loc -> env -> evar_map -> unsafe_judgment -> type_constraint_type -> evar_map * unsafe_judgment - val inh_conv_coerce_rigid_to : loc -> + val inh_conv_coerce_rigid_to : bool -> loc -> env -> evar_map -> unsafe_judgment -> type_constraint_type -> evar_map * unsafe_judgment (* [inh_conv_coerces_to loc env evd t t'] checks if an object of type [t] @@ -140,9 +140,11 @@ lookup_path_to_fun_from env evd j.uj_type in (evd,apply_coercion env evd p j t) - let inh_app_fun env evd j = + let inh_app_fun resolve_tc env evd j = try inh_app_fun env evd j - with Not_found -> + with + | Not_found when not resolve_tc -> (evd, j) + | Not_found -> try inh_app_fun env (saturate_evd env evd) j with Not_found -> (evd, j) @@ -221,13 +223,15 @@ | _ -> raise NoCoercion (* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *) - let inh_conv_coerce_to_gen rigidonly loc env evd cj (n, t) = + let inh_conv_coerce_to_gen resolve_tc rigidonly loc env evd cj (n, t) = match n with None -> let (evd', val') = try inh_conv_coerce_to_fail loc env evd rigidonly (Some cj.uj_val) cj.uj_type t - with NoCoercion -> + with + | NoCoercion when not resolve_tc -> error_actual_type_loc loc env evd cj t + | NoCoercion -> let evd = saturate_evd env evd in try inh_conv_coerce_to_fail loc env evd rigidonly (Some cj.uj_val) cj.uj_type t @@ -238,8 +242,8 @@ (evd',{ uj_val = val'; uj_type = t }) | Some (init, cur) -> (evd, cj) - let inh_conv_coerce_to = inh_conv_coerce_to_gen false - let inh_conv_coerce_rigid_to = inh_conv_coerce_to_gen true + let inh_conv_coerce_to resolve_tc = inh_conv_coerce_to_gen resolve_tc false + let inh_conv_coerce_rigid_to resolve_tc = inh_conv_coerce_to_gen resolve_tc true let inh_conv_coerces_to loc env (evd : evar_map) t (abs, t') = diff -Nru coq-8.4pl3dfsg/pretyping/coercion.mli coq-8.4pl4dfsg/pretyping/coercion.mli --- coq-8.4pl3dfsg/pretyping/coercion.mli 2013-12-21 08:03:14.000000000 +0000 +++ coq-8.4pl4dfsg/pretyping/coercion.mli 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* evar_map -> unsafe_judgment -> evar_map * unsafe_judgment + bool -> env -> evar_map -> unsafe_judgment -> evar_map * unsafe_judgment (** [inh_coerce_to_sort env isevars j] coerces [j] to a type; i.e. it inserts a coercion into [j], if needed, in such a way it gets as @@ -40,13 +42,15 @@ val inh_coerce_to_prod : loc -> env -> evar_map -> type_constraint_type -> evar_map * type_constraint_type - (** [inh_conv_coerce_to loc env isevars j t] coerces [j] to an object of type + (** [inh_conv_coerce_to resolve_tc loc env isevars j t] coerces [j] to an object of type [t]; i.e. it inserts a coercion into [j], if needed, in such a way [t] and - [j.uj_type] are convertible; it fails if no coercion is applicable *) - val inh_conv_coerce_to : loc -> + [j.uj_type] are convertible; it fails if no coercion is applicable. + resolve_tc=false disables resolving type classes (as the last + resort before failing) *) + val inh_conv_coerce_to : bool -> loc -> env -> evar_map -> unsafe_judgment -> type_constraint_type -> evar_map * unsafe_judgment - val inh_conv_coerce_rigid_to : loc -> + val inh_conv_coerce_rigid_to : bool -> loc -> env -> evar_map -> unsafe_judgment -> type_constraint_type -> evar_map * unsafe_judgment (** [inh_conv_coerces_to loc env isevars t t'] checks if an object of type [t] diff -Nru coq-8.4pl3dfsg/pretyping/detyping.ml coq-8.4pl4dfsg/pretyping/detyping.ml --- coq-8.4pl3dfsg/pretyping/detyping.ml 2013-12-21 08:03:14.000000000 +0000 +++ coq-8.4pl4dfsg/pretyping/detyping.ml 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* !debug_unification); + Goptions.optwrite = (fun a -> debug_unification:=a); +} + + type flex_kind_of_term = | Rigid of constr | PseudoRigid of constr (* approximated as rigid but not necessarily so *) @@ -210,6 +221,13 @@ in (* Evar must be undefined since we have flushed evars *) + let () = if !debug_unification then + let open Pp in + let pr_state (tm,l) = + h 0 (Termops.print_constr tm ++ str "|" ++ cut () + ++ prlist_with_sep pr_semicolon + (fun x -> hov 1 (Termops.print_constr x)) l) in + pp (v 0 (pr_state appr1 ++ cut () ++ pr_state appr2 ++ cut ()) ++ fnl ()) in match (flex_kind_of_term term1 l1, flex_kind_of_term term2 l2) with | Flexible (sp1,al1 as ev1), Flexible (sp2,al2 as ev2) -> let f1 i = diff -Nru coq-8.4pl3dfsg/pretyping/evarconv.mli coq-8.4pl4dfsg/pretyping/evarconv.mli --- coq-8.4pl3dfsg/pretyping/evarconv.mli 2013-12-21 08:03:14.000000000 +0000 +++ coq-8.4pl4dfsg/pretyping/evarconv.mli 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* candidates + | Some filter -> + let ids = List.map pi1 (list_filter_with filter (evar_context evi)) in + List.filter (fun a -> list_subset (Idset.elements (collect_vars a)) ids) + candidates + +let filter_candidates evd evk filter candidates_update = let evi = Evd.find_undefined evd evk in - let candidates = match candidates with + let candidates = match candidates_update with | None -> evi.evar_candidates - | Some _ -> candidates in - match candidates,filter with - | None,_ | _, None -> candidates - | Some l, Some filter -> - let ids = List.map pi1 (list_filter_with filter (evar_context evi)) in - Some (List.filter (fun a -> - list_subset (Idset.elements (collect_vars a)) ids) l) + | Some _ -> candidates_update + in + match candidates with + | None -> None + | Some l -> + let l' = filter_effective_candidates evi filter l in + if List.length l = List.length l' && candidates_update = None then + None + else + Some l' let closure_of_filter evd evk filter = let evi = Evd.find_undefined evd evk in @@ -1530,6 +1541,7 @@ exception NotInvertibleUsingOurAlgorithm of constr exception NotEnoughInformationToProgress of (identifier * evar_projection) list +exception NotEnoughInformationEvarEvar of constr exception OccurCheckIn of evar_map * constr let rec invert_definition conv_algo choose env evd (evk,argsv as ev) rhs = @@ -1608,7 +1620,8 @@ with | EvarSolvedOnTheFly (evd,t) -> evdref:=evd; imitate envk t | CannotProject filter' -> - assert !progress; + if not !progress then + raise (NotEnoughInformationEvarEvar t); (* Make the virtual left evar real *) let ty = get_type_of env' !evdref t in let (evd,evar'',ev'') = @@ -1714,6 +1727,8 @@ with | NotEnoughInformationToProgress sols -> postpone_non_unique_projection env evd ev sols rhs + | NotEnoughInformationEvarEvar t -> + add_conv_pb (Reduction.CONV,env,mkEvar ev,t) evd | NotInvertibleUsingOurAlgorithm t -> error_not_clean env evd evk t (evar_source evk evd) | OccurCheckIn (evd,rhs) -> diff -Nru coq-8.4pl3dfsg/pretyping/evarutil.mli coq-8.4pl4dfsg/pretyping/evarutil.mli --- coq-8.4pl3dfsg/pretyping/evarutil.mli 2013-12-21 08:03:14.000000000 +0000 +++ coq-8.4pl4dfsg/pretyping/evarutil.mli 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* Anonymous -> - (* Unable to manage the presence of both an alias and a variable *) - raise Not_found - | GVar (loc,id) -> PatVar (loc,Name id) - | GHole (loc,_) -> PatVar (loc,na) - | GRef (loc,ConstructRef cstr) -> - PatCstr (loc,cstr,[],na) - | GApp (loc,GRef (_,ConstructRef (ind,_ as cstr)),args) -> - let mib,_ = Global.lookup_inductive ind in - let nparams = mib.Declarations.mind_nparams in - if nparams > List.length args then - user_err_loc (loc,"",Pp.str "Invalid notation for pattern."); - let params,args = list_chop nparams args in - List.iter (function GHole _ -> () - | _ -> user_err_loc (loc,"",Pp.str"Invalid notation for pattern.")) - params; - let args = List.map (cases_pattern_of_glob_constr Anonymous) args in - PatCstr (loc,cstr,args,na) - | _ -> raise Not_found - -let rec cases_pattern_of_glob_constr na = function - | GVar (loc,id) when na<>Anonymous -> (* Unable to manage the presence of both an alias and a variable *) raise Not_found | GVar (loc,id) -> PatVar (loc,Name id) diff -Nru coq-8.4pl3dfsg/pretyping/glob_term.mli coq-8.4pl4dfsg/pretyping/glob_term.mli --- coq-8.4pl3dfsg/pretyping/glob_term.mli 2013-12-21 08:03:14.000000000 +0000 +++ coq-8.4pl4dfsg/pretyping/glob_term.mli 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* env -> evar_map ref -> + bool -> type_constraint -> env -> evar_map ref -> ltac_var_map -> glob_constr -> unsafe_judgment val pretype_type : - val_constraint -> env -> evar_map ref -> + bool -> val_constraint -> env -> evar_map ref -> ltac_var_map -> glob_constr -> unsafe_type_judgment val pretype_gen : @@ -259,9 +259,9 @@ done (* coerce to tycon if any *) - let inh_conv_coerce_to_tycon loc env evdref j = function + let inh_conv_coerce_to_tycon resolve_tc loc env evdref j = function | None -> j - | Some t -> evd_comb2 (Coercion.inh_conv_coerce_to loc env) evdref j t + | Some t -> evd_comb2 (Coercion.inh_conv_coerce_to resolve_tc loc env) evdref j t let push_rels vars env = List.fold_right push_rel vars env @@ -297,18 +297,19 @@ let c = substl subst c in { uj_val = c; uj_type = protected_get_type_of env sigma c } with Not_found -> - (* Check if [id] is a section or goal variable *) - try - let (_,_,typ) = lookup_named id env in - { uj_val = mkVar id; uj_type = typ } - with Not_found -> - (* [id] not found, build nice error message if [id] yet known from ltac *) + (* if [id] an ltac variable not bound to a term *) + (* build a nice error message *) try match List.assoc id unbndltacvars with | None -> user_err_loc (loc,"", str "Variable " ++ pr_id id ++ str " should be bound to a term.") | Some id0 -> Pretype_errors.error_var_not_found_loc loc id0 with Not_found -> + (* Check if [id] is a section or goal variable *) + try + let (_,_,typ) = lookup_named id env in + { uj_val = mkVar id; uj_type = typ } + with Not_found -> (* [id] not found, standard error message *) error_var_not_found_loc loc id @@ -346,7 +347,11 @@ (* [pretype tycon env evdref lvar lmeta cstr] attempts to type [cstr] *) (* in environment [env], with existential variables [evdref] and *) (* the type constraint tycon *) - let rec pretype (tycon : type_constraint) env evdref lvar = function + let rec pretype resolve_tc (tycon : type_constraint) env evdref lvar t = + let pretype = pretype resolve_tc in + let pretype_type = pretype_type resolve_tc in + let inh_conv_coerce_to_tycon = inh_conv_coerce_to_tycon resolve_tc in + match t with | GRef (loc,ref) -> inh_conv_coerce_to_tycon loc env evdref (pretype_ref loc evdref env ref) @@ -459,7 +464,7 @@ | [] -> resj | c::rest -> let argloc = loc_of_glob_constr c in - let resj = evd_comb1 (Coercion.inh_app_fun env) evdref resj in + let resj = evd_comb1 (Coercion.inh_app_fun resolve_tc env) evdref resj in let resty = whd_betadeltaiota env !evdref resj.uj_type in match kind_of_term resty with | Prod (na,c1,c2) -> @@ -696,7 +701,7 @@ in inh_conv_coerce_to_tycon loc env evdref cj tycon (* [pretype_type valcon env evdref lvar c] coerces [c] into a type *) - and pretype_type valcon env evdref lvar = function + and pretype_type resolve_tc valcon env evdref lvar = function | GHole loc -> (match valcon with | Some v -> @@ -716,7 +721,7 @@ { utj_val = e_new_evar evdref env ~src:loc (mkSort s); utj_type = s}) | c -> - let j = pretype empty_tycon env evdref lvar c in + let j = pretype resolve_tc empty_tycon env evdref lvar c in let loc = loc_of_glob_constr c in let tj = evd_comb1 (Coercion.inh_coerce_to_sort loc env) evdref j in match valcon with @@ -731,9 +736,9 @@ let c' = match kind with | OfType exptyp -> let tycon = match exptyp with None -> empty_tycon | Some t -> mk_tycon t in - (pretype tycon env evdref lvar c).uj_val + (pretype resolve_classes tycon env evdref lvar c).uj_val | IsType -> - (pretype_type empty_valcon env evdref lvar c).utj_val + (pretype_type resolve_classes empty_valcon env evdref lvar c).utj_val in resolve_evars env evdref fail_evar resolve_classes; let c = if expand_evar then nf_evar !evdref c' else c' in @@ -747,14 +752,14 @@ let understand_judgment sigma env c = let evdref = ref sigma in - let j = pretype empty_tycon env evdref ([],[]) c in + let j = pretype true empty_tycon env evdref ([],[]) c in resolve_evars env evdref true true; let j = j_nf_evar !evdref j in check_evars env sigma !evdref (mkCast(j.uj_val,DEFAULTcast, j.uj_type)); j let understand_judgment_tcc evdref env c = - let j = pretype empty_tycon env evdref ([],[]) c in + let j = pretype true empty_tycon env evdref ([],[]) c in resolve_evars env evdref false true; j_nf_evar !evdref j diff -Nru coq-8.4pl3dfsg/pretyping/pretyping.mli coq-8.4pl4dfsg/pretyping/pretyping.mli --- coq-8.4pl3dfsg/pretyping/pretyping.mli 2013-12-21 08:03:14.000000000 +0000 +++ coq-8.4pl4dfsg/pretyping/pretyping.mli 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* env -> evar_map ref -> + bool -> type_constraint -> env -> evar_map ref -> ltac_var_map -> glob_constr -> unsafe_judgment val pretype_type : - val_constraint -> env -> evar_map ref -> + bool -> val_constraint -> env -> evar_map ref -> ltac_var_map -> glob_constr -> unsafe_type_judgment val pretype_gen : diff -Nru coq-8.4pl3dfsg/pretyping/recordops.ml coq-8.4pl4dfsg/pretyping/recordops.ml --- coq-8.4pl3dfsg/pretyping/recordops.ml 2013-12-21 08:03:14.000000000 +0000 +++ coq-8.4pl4dfsg/pretyping/recordops.ml 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* [] | file :: fl -> - let dirname = Filename.dirname file in - let basename = Filename.basename file in - let modulename = - if Filename.check_suffix basename ".v" then - Filename.chop_suffix basename ".v" + let name_no_suffix = + if Filename.check_suffix file ".v" then + Filename.chop_suffix file ".v" else - basename + file in + let modulename = Filename.basename name_no_suffix in check_module_name modulename; - let file = Filename.concat dirname modulename in (if !verbose then "-compile-verbose" else "-compile") - :: file :: (make_compilation_args fl) + :: name_no_suffix :: (make_compilation_args fl) (* compilation of files [files] with command [command] and args [args] *) diff -Nru coq-8.4pl3dfsg/scripts/coqmktop.ml coq-8.4pl4dfsg/scripts/coqmktop.ml --- coq-8.4pl3dfsg/scripts/coqmktop.ml 2013-12-21 08:03:14.000000000 +0000 +++ coq-8.4pl4dfsg/scripts/coqmktop.ml 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* (str"unfold " ++ pr_evaluable_reference c) | Extern tac -> - (str "(*external*) " ++ Pptactic.pr_glob_tactic (Global.env()) tac) + let env = + try + let (_, env) = Pfedit.get_current_goal_context () in + env + with e when Errors.noncritical e -> Global.env () + in + (str "(*external*) " ++ Pptactic.pr_glob_tactic env tac) let pr_hint (id, v) = (pr_autotactic v.code ++ str"(level " ++ int v.pri ++ str", id " ++ int id ++ str ")" ++ spc ()) diff -Nru coq-8.4pl3dfsg/tactics/auto.mli coq-8.4pl4dfsg/tactics/auto.mli --- coq-8.4pl3dfsg/tactics/auto.mli 2013-12-21 08:03:14.000000000 +0000 +++ coq-8.4pl4dfsg/tactics/auto.mli 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* [ admit_as_an_axiom ] END -let replace_in_clause_maybe_by (sigma1,c1) c2 in_hyp tac = + + +let classes_dirpath = + make_dirpath (List.map id_of_string ["Classes";"Coq"]) + +let init_setoid () = + if Libnames.is_dirpath_prefix_of classes_dirpath (Lib.cwd ()) then () + else Coqlib.check_required_library ["Coq";"Setoids";"Setoid"] + + +let occurrences_of occs = + let loccs = match occs with + | n::_ as nl when n < 0 -> (false,List.map (fun n -> ArgArg (abs n)) nl) + | nl -> + if List.exists (fun n -> n < 0) nl then + error "Illegal negative occurrence number."; + (true, List.map (fun n -> (ArgArg n)) nl) + in + init_setoid (); + {onhyps = Some []; concl_occs =loccs} + +let replace_in_clause_maybe_by (sigma1,c1) c2 cl tac = Refiner.tclWITHHOLES false - (replace_in_clause_maybe_by c1 c2 (glob_in_arg_hyp_to_clause in_hyp)) + (replace_in_clause_maybe_by c1 c2 cl) sigma1 (Option.map Tacinterp.eval_tactic tac) @@ -44,9 +65,15 @@ TACTIC EXTEND replace ["replace" open_constr(c1) "with" constr(c2) in_arg_hyp(in_hyp) by_arg_tac(tac) ] --> [ replace_in_clause_maybe_by c1 c2 in_hyp tac ] +-> [ replace_in_clause_maybe_by c1 c2 (glob_in_arg_hyp_to_clause in_hyp) tac ] END +TACTIC EXTEND replace_at + ["replace" open_constr(c1) "with" constr(c2) "at" occurrences(occs) by_arg_tac(tac) ] +-> [ replace_in_clause_maybe_by c1 c2 (occurrences_of occs) tac ] +END + + TACTIC EXTEND replace_term_left [ "replace" "->" open_constr(c) in_arg_hyp(in_hyp) ] -> [ replace_multi_term (Some true) c in_hyp] diff -Nru coq-8.4pl3dfsg/tactics/extratactics.mli coq-8.4pl4dfsg/tactics/extratactics.mli --- coq-8.4pl3dfsg/tactics/extratactics.mli 2013-12-21 08:03:14.000000000 +0000 +++ coq-8.4pl4dfsg/tactics/extratactics.mli 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* in_gen globwit_red_expr (intern_red_expr ist (out_gen rawwit_red_expr x)) - | OpenConstrArgType b -> - in_gen (globwit_open_constr_gen b) - ((),intern_constr ist (snd (out_gen (rawwit_open_constr_gen b) x))) + | OpenConstrArgType (b1,b2) -> + in_gen (globwit_open_constr_gen (b1,b2)) + ((),intern_constr ist (snd (out_gen (rawwit_open_constr_gen (b1,b2)) x))) | ConstrWithBindingsArgType -> in_gen globwit_constr_with_bindings (intern_constr_with_bindings ist (out_gen rawwit_constr_with_bindings x)) @@ -1290,8 +1290,11 @@ let interp_open_constr_gen kind ist = interp_gen kind ist false true false false -let interp_open_constr ccl ist = - interp_gen (OfType ccl) ist false true false (ccl<>None) +(* wTC is for retrocompatibility: TC resolution started only if needed *) +let interp_open_constr ccl wTC ist e s t = + try interp_gen (OfType ccl) ist false true false (ccl<>None) e s t + with ex when Pretype_errors.precatchable_exception ex && ccl = None && wTC -> + interp_gen (OfType ccl) ist false true false true e s t let interp_pure_open_constr ist = interp_gen (OfType None) ist false false false false @@ -1333,7 +1336,7 @@ let interp_open_constr_list = interp_constr_in_compound_list (fun x -> x) (fun x -> x) - (interp_open_constr None) + (interp_open_constr None false) let interp_auto_lemmas ist env sigma lems = let local_sigma, lems = interp_open_constr_list ist env sigma lems in @@ -1526,7 +1529,7 @@ with Not_found -> NamedHyp id let interp_binding ist env sigma (loc,b,c) = - let sigma, c = interp_open_constr None ist env sigma c in + let sigma, c = interp_open_constr None false ist env sigma c in sigma, (loc,interp_binding_name ist b,c) let interp_bindings ist env sigma = function @@ -1541,12 +1544,12 @@ let interp_constr_with_bindings ist env sigma (c,bl) = let sigma, bl = interp_bindings ist env sigma bl in - let sigma, c = interp_open_constr None ist env sigma c in + let sigma, c = interp_open_constr None false ist env sigma c in sigma, (c,bl) -let interp_open_constr_with_bindings ist env sigma (c,bl) = +let interp_open_constr_with_bindings wTC ist env sigma (c,bl) = let sigma, bl = interp_bindings ist env sigma bl in - let sigma, c = interp_open_constr None ist env sigma c in + let sigma, c = interp_open_constr None wTC ist env sigma c in sigma, (c, bl) let loc_of_bindings = function @@ -1554,11 +1557,11 @@ | ImplicitBindings l -> loc_of_glob_constr (fst (list_last l)) | ExplicitBindings l -> pi1 (list_last l) -let interp_open_constr_with_bindings_loc ist env sigma ((c,_),bl as cb) = +let interp_open_constr_with_bindings_loc wTC ist env sigma ((c,_),bl as cb) = let loc1 = loc_of_glob_constr c in let loc2 = loc_of_bindings bl in let loc = if loc2 = dummy_loc then loc1 else join_loc loc1 loc2 in - let sigma, cb = interp_open_constr_with_bindings ist env sigma cb in + let sigma, cb = interp_open_constr_with_bindings wTC ist env sigma cb in sigma, (loc,cb) let interp_induction_arg ist gl arg = @@ -1754,8 +1757,8 @@ let mk_constr_value ist gl c = let (sigma,c_interp) = pf_interp_constr ist gl c in sigma,VConstr ([],c_interp) -let mk_open_constr_value ist gl c = - let (sigma,c_interp) = pf_apply (interp_open_constr None ist) gl c in +let mk_open_constr_value wTC ist gl c = + let (sigma,c_interp) = pf_apply (interp_open_constr None wTC ist) gl c in sigma,VConstr ([],c_interp) let mk_hyp_value ist gl c = VConstr ([],mkVar (interp_hyp ist gl c)) let mk_int_or_var_value ist c = VInteger (interp_int_or_var ist c) @@ -2132,11 +2135,11 @@ let (sigma,r_interp) = pf_interp_red_expr ist gl (out_gen globwit_red_expr x) in evdref := sigma; in_gen wit_red_expr r_interp - | OpenConstrArgType casted -> - in_gen (wit_open_constr_gen casted) - (interp_open_constr (if casted then Some (pf_concl gl) else None) + | OpenConstrArgType (casted,wTC) -> + in_gen (wit_open_constr_gen (casted,wTC)) + (interp_open_constr (if casted then Some (pf_concl gl) else None) wTC ist (pf_env gl) (project gl) - (snd (out_gen (globwit_open_constr_gen casted) x))) + (snd (out_gen (globwit_open_constr_gen (casted,wTC)) x))) | ConstrWithBindingsArgType -> in_gen wit_constr_with_bindings (pack_sigma (interp_constr_with_bindings ist (pf_env gl) (project gl) @@ -2332,7 +2335,7 @@ (h_vm_cast_no_check c_interp) | TacApply (a,ev,cb,cl) -> let sigma, l = - list_fold_map (interp_open_constr_with_bindings_loc ist env) sigma cb + list_fold_map (interp_open_constr_with_bindings_loc true ist env) sigma cb in let tac = match cl with | None -> h_apply a ev @@ -2547,7 +2550,7 @@ (* Equality and inversion *) | TacRewrite (ev,l,cl,by) -> let l = List.map (fun (b,m,c) -> - let f env sigma = interp_open_constr_with_bindings ist env sigma c in + let f env sigma = interp_open_constr_with_bindings false ist env sigma c in (b,m,f)) l in let cl = interp_clause ist gl cl in Equality.general_multi_multi_rewrite ev l cl @@ -2610,8 +2613,12 @@ let (sigma,v) = mk_constr_value ist gl (out_gen globwit_constr x) in evdref := sigma; v - | OpenConstrArgType false -> - let (sigma,v) = mk_open_constr_value ist gl (snd (out_gen globwit_open_constr x)) in + | OpenConstrArgType (false,true) -> + let (sigma,v) = mk_open_constr_value true ist gl (snd (out_gen globwit_open_constr_wTC x)) in + evdref := sigma; + v + | OpenConstrArgType (false,false) -> + let (sigma,v) = mk_open_constr_value false ist gl (snd (out_gen globwit_open_constr x)) in evdref := sigma; v | ConstrMayEvalArgType -> @@ -3013,9 +3020,9 @@ (out_gen globwit_quant_hyp x)) | RedExprArgType -> in_gen globwit_red_expr (subst_redexp subst (out_gen globwit_red_expr x)) - | OpenConstrArgType b -> - in_gen (globwit_open_constr_gen b) - ((),subst_glob_constr subst (snd (out_gen (globwit_open_constr_gen b) x))) + | OpenConstrArgType (b1,b2) -> + in_gen (globwit_open_constr_gen (b1,b2)) + ((),subst_glob_constr subst (snd (out_gen (globwit_open_constr_gen (b1,b2)) x))) | ConstrWithBindingsArgType -> in_gen globwit_constr_with_bindings (subst_glob_with_bindings subst (out_gen globwit_constr_with_bindings x)) diff -Nru coq-8.4pl3dfsg/tactics/tacinterp.mli coq-8.4pl4dfsg/tactics/tacinterp.mli --- coq-8.4pl3dfsg/tactics/tacinterp.mli 2013-12-21 08:03:14.000000000 +0000 +++ coq-8.4pl4dfsg/tactics/tacinterp.mli 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* Environ.env -> Evd.evar_map -> glob_constr_and_expr Glob_term.bindings -> Evd.evar_map * constr Glob_term.bindings -val interp_open_constr_with_bindings : interp_sign -> Environ.env -> Evd.evar_map -> +(* first arguments mean wTC (with type classes resolution) *) +val interp_open_constr_with_bindings : bool -> interp_sign -> Environ.env -> Evd.evar_map -> glob_constr_and_expr Glob_term.with_bindings -> Evd.evar_map * constr Glob_term.with_bindings (** Initial call for interpretation *) diff -Nru coq-8.4pl3dfsg/tactics/tacticals.ml coq-8.4pl4dfsg/tactics/tacticals.ml --- coq-8.4pl3dfsg/tactics/tacticals.ml 2013-12-21 08:03:14.000000000 +0000 +++ coq-8.4pl4dfsg/tactics/tacticals.ml 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* - forall x0 x4 x5 S0 : nat, x0 + S0 = x4 + x5 + (S x + x1) + H : forall x5 x6 : nat, + x5 + x1 = x4 + x6 -> + forall x7 x8 x9 S : nat, x7 + S = x8 + x9 + (Datatypes.S x5 + x1) H0 : x + x1 = x4 + x0 ============================ forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x @@ -64,9 +64,9 @@ x1 : nat x4 : nat x0 : nat - H : forall x x3 : nat, - x + x1 = x4 + x3 -> - forall x0 x4 x5 S0 : nat, x0 + S0 = x4 + x5 + (S x + x1) + H : forall x5 x6 : nat, + x5 + x1 = x4 + x6 -> + forall x7 x8 x9 S : nat, x7 + S = x8 + x9 + (Datatypes.S x5 + x1) H0 : x + x1 = x4 + x0 x5 : nat x6 : nat @@ -78,6 +78,6 @@ x3 : nat a : nat - H : a = 0 -> forall a : nat, a = 0 + H : a = 0 -> forall a0 : nat, a0 = 0 ============================ a = 0 diff -Nru coq-8.4pl3dfsg/test-suite/success/Check.v coq-8.4pl4dfsg/test-suite/success/Check.v --- coq-8.4pl3dfsg/test-suite/success/Check.v 2013-12-21 08:03:14.000000000 +0000 +++ coq-8.4pl4dfsg/test-suite/success/Check.v 2014-04-24 15:13:03.000000000 +0000 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(*