diff options
| -rw-r--r-- | .gitlab-ci.yml | 4 | ||||
| -rw-r--r-- | Makefile.ci | 1 | ||||
| -rw-r--r-- | dev/base_include | 1 | ||||
| -rwxr-xr-x | dev/ci/ci-basic-overlay.sh | 7 | ||||
| -rwxr-xr-x | dev/ci/ci-fiat_crypto_legacy.sh | 13 | ||||
| -rw-r--r-- | doc/sphinx/practical-tools/utilities.rst | 4 | ||||
| -rw-r--r-- | plugins/ltac/leminv.ml | 2 | ||||
| -rw-r--r-- | proofs/clenv.ml | 129 | ||||
| -rw-r--r-- | proofs/clenv.mli | 21 | ||||
| -rw-r--r-- | proofs/clenvtac.ml | 135 | ||||
| -rw-r--r-- | proofs/clenvtac.mli | 23 | ||||
| -rw-r--r-- | proofs/logic.ml | 29 | ||||
| -rw-r--r-- | proofs/logic.mli | 3 | ||||
| -rw-r--r-- | proofs/proofs.mllib | 1 | ||||
| -rw-r--r-- | stm/stm.ml | 12 | ||||
| -rw-r--r-- | tactics/auto.ml | 3 | ||||
| -rw-r--r-- | tactics/class_tactics.ml | 23 | ||||
| -rw-r--r-- | tactics/class_tactics.mli | 3 | ||||
| -rw-r--r-- | tactics/eauto.ml | 5 | ||||
| -rw-r--r-- | tactics/equality.ml | 8 | ||||
| -rw-r--r-- | tactics/tacticals.ml | 10 | ||||
| -rw-r--r-- | tactics/tacticals.mli | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 11 |
23 files changed, 183 insertions, 267 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index f6c035553c..7915cc34fb 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -742,6 +742,10 @@ library:ci-fiat_crypto: - library:ci-coqprime - plugin:ci-rewriter +library:ci-fiat_crypto_legacy: + extends: .ci-template-flambda + allow_failure: true # See https://github.com/coq/coq/wiki/Coq-Call-2020-06-24#adding-back-fiat-crypto-legacy + # We cannot use flambda due to # https://github.com/ocaml/ocaml/issues/7842, see # https://github.com/coq/coq/pull/11916#issuecomment-609977375 diff --git a/Makefile.ci b/Makefile.ci index 07f06caa3a..77d8bda671 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -29,6 +29,7 @@ CI_TARGETS= \ ci-equations \ ci-fcsl_pcm \ ci-fiat_crypto \ + ci-fiat_crypto_legacy \ ci-fiat_crypto_ocaml \ ci-fiat_parsers \ ci-flocq \ diff --git a/dev/base_include b/dev/base_include index 45e79147c1..efbd156758 100644 --- a/dev/base_include +++ b/dev/base_include @@ -66,7 +66,6 @@ open Pretyping open Cbv open Coercionops open Clenv -open Clenvtac open Constr_matching open Glob_term open Glob_ops diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 88471a92aa..4973cbb478 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -179,6 +179,13 @@ : "${fiat_crypto_CI_ARCHIVEURL:=${fiat_crypto_CI_GITURL}/archive}" ######################################################################## +# fiat_crypto_legacy +######################################################################## +: "${fiat_crypto_legacy_CI_REF:=sp2019latest}" +: "${fiat_crypto_legacy_CI_GITURL:=https://github.com/mit-plv/fiat-crypto}" +: "${fiat_crypto_legacy_CI_ARCHIVEURL:=${fiat_crypto_legacy_CI_GITURL}/archive}" + +######################################################################## # coq_dpdgraph ######################################################################## : "${coq_dpdgraph_CI_REF:=coq-master}" diff --git a/dev/ci/ci-fiat_crypto_legacy.sh b/dev/ci/ci-fiat_crypto_legacy.sh new file mode 100755 index 0000000000..6d0a803401 --- /dev/null +++ b/dev/ci/ci-fiat_crypto_legacy.sh @@ -0,0 +1,13 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +FORCE_GIT=1 +git_download fiat_crypto_legacy + +fiat_crypto_legacy_CI_TARGETS1="print-old-pipeline-lite-hardcoded old-pipeline-lite-hardcoded lite-display-hardcoded" +fiat_crypto_legacy_CI_TARGETS2="print-old-pipeline-nobigmem-hardcoded old-pipeline-nobigmem-hardcoded nonautogenerated-specific nonautogenerated-specific-display selected-specific selected-specific-display" + +( cd "${CI_BUILD_DIR}/fiat_crypto_legacy" && git submodule update --init --recursive && \ + make ${fiat_crypto_legacy_CI_TARGETS1} && make -j 1 ${fiat_crypto_legacy_CI_TARGETS2} ) diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index 33ebbce640..d9992029ba 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -74,8 +74,8 @@ to literally pass an argument ``foo`` to ``coqc``: in the example, this allows to pass the two-word option ``-w all`` (see :ref:`command line options <command-line-options>`). -Currently, both |CoqIDE| and Proof-General (version ≥ ``4.3pre``) -understand ``_CoqProject`` files and invoke |Coq| with the desired options. +|CoqIDE|, Proof-General and VSCoq all +understand ``_CoqProject`` files and can be used to invoke |Coq| with the desired options. The ``coq_makefile`` utility can be used to set up a build infrastructure for the |Coq| project based on makefiles. The recommended way of diff --git a/plugins/ltac/leminv.ml b/plugins/ltac/leminv.ml index 5a8ec404ee..0024d1a4ba 100644 --- a/plugins/ltac/leminv.ml +++ b/plugins/ltac/leminv.ml @@ -261,7 +261,7 @@ let lemInv id c = try let clause = mk_clenv_from_env (pf_env gls) (project gls) None (c, pf_get_type_of gls c) in let clause = clenv_constrain_last_binding (EConstr.mkVar id) clause in - Clenvtac.res_pf clause ~flags:(Unification.elim_flags ()) ~with_evars:false + Clenv.res_pf clause ~flags:(Unification.elim_flags ()) ~with_evars:false with | NoSuchBinding -> user_err diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 87b4255b88..7fb3a21813 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -28,6 +28,7 @@ open Pretype_errors open Evarutil open Unification open Tactypes +open Logic (******************************************************************) (* Clausal environments *) @@ -41,7 +42,6 @@ type clausenv = { let cl_env ce = ce.env let cl_sigma ce = ce.evd -let clenv_nf_meta clenv c = nf_meta clenv.env clenv.evd c let clenv_term clenv c = meta_instance clenv.env clenv.evd c let clenv_meta_type clenv mv = Typing.meta_type clenv.env clenv.evd mv let clenv_value clenv = meta_instance clenv.env clenv.evd clenv.templval @@ -376,21 +376,21 @@ let adjust_meta_source evd mv = function *) let clenv_pose_metas_as_evars clenv dep_mvs = - let rec fold clenv evs = function - | [] -> clenv, evs + let rec fold clenv = function + | [] -> clenv | mv::mvs -> let ty = clenv_meta_type clenv mv in (* Postpone the evar-ization if dependent on another meta *) (* This assumes no cycle in the dependencies - is it correct ? *) - if occur_meta clenv.evd ty then fold clenv evs (mvs@[mv]) + if occur_meta clenv.evd ty then fold clenv (mvs@[mv]) else let src = evar_source_of_meta mv clenv.evd in let src = adjust_meta_source clenv.evd mv src in let evd = clenv.evd in let (evd, evar) = new_evar (cl_env clenv) evd ~src ty in let clenv = clenv_assign mv evar {clenv with evd=evd} in - fold clenv (fst (destEvar evd evar) :: evs) mvs in - fold clenv [] dep_mvs + fold clenv mvs in + fold clenv dep_mvs (******************************************************************) @@ -444,8 +444,6 @@ let clenv_fchain ?with_univs ?(flags=fchain_flags ()) mv clenv nextclenv = (***************************************************************) (* Bindings *) -type arg_bindings = constr explicit_bindings - (* [clenv_independent clenv] * returns a list of metavariables which appear in the term cval, * and which are not dependent. That is, they do not appear in @@ -598,6 +596,121 @@ let clenv_constrain_dep_args hyps_only bl clenv = else error_not_right_number_missing_arguments (List.length occlist) + +(* This function put casts around metavariables whose type could not be + * inferred by the refiner, that is head of applications, predicates and + * subject of Cases. + * Does check that the casted type is closed. Anyway, the refiner would + * fail in this case... *) + +let clenv_cast_meta clenv = + let rec crec u = + match EConstr.kind clenv.evd u with + | App _ | Case _ -> crec_hd u + | Cast (c,_,_) when isMeta clenv.evd c -> u + | Proj (p, c) -> mkProj (p, crec_hd c) + | _ -> EConstr.map clenv.evd crec u + + and crec_hd u = + match EConstr.kind clenv.evd (strip_outer_cast clenv.evd u) with + | Meta mv -> + (try + let b = Typing.meta_type clenv.env clenv.evd mv in + assert (not (occur_meta clenv.evd b)); + if occur_meta clenv.evd b then u + else mkCast (mkMeta mv, DEFAULTcast, b) + with Not_found -> u) + | App(f,args) -> mkApp (crec_hd f, Array.map crec args) + | Case(ci,p,c,br) -> + mkCase (ci, crec_hd p, crec_hd c, Array.map crec br) + | Proj (p, c) -> mkProj (p, crec_hd c) + | _ -> u + in + crec + +let clenv_value_cast_meta clenv = + clenv_cast_meta clenv (clenv_value clenv) + +let clenv_pose_dependent_evars ?(with_evars=false) clenv = + let dep_mvs = clenv_dependent clenv in + let env, sigma = clenv.env, clenv.evd in + if not (List.is_empty dep_mvs) && not with_evars then + raise + (RefinerError (env, sigma, UnresolvedBindings (List.map (meta_name clenv.evd) dep_mvs))); + clenv_pose_metas_as_evars clenv dep_mvs + +let clenv_refine ?(with_evars=false) ?(with_classes=true) clenv = + Proofview.Goal.enter begin fun gl -> + let clenv = clenv_pose_dependent_evars ~with_evars clenv in + let evd' = + if with_classes then + let evd' = + Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars + ~fail:(not with_evars) clenv.env clenv.evd + in + (* After an apply, all the subgoals including those dependent shelved ones are in + the hands of the user and resolution won't be called implicitely on them. *) + Typeclasses.make_unresolvables (fun x -> true) evd' + else clenv.evd + in + let clenv = { clenv with evd = evd' } in + Proofview.tclTHEN + (Proofview.Unsafe.tclEVARS (Evd.clear_metas evd')) + (refiner ~check:false EConstr.Unsafe.(to_constr (clenv_cast_meta clenv (clenv_value clenv)))) + end + +open Unification + +let dft = default_unify_flags + +let res_pf ?with_evars ?(with_classes=true) ?(flags=dft ()) clenv = + Proofview.Goal.enter begin fun gl -> + let clenv = clenv_unique_resolver ~flags clenv gl in + clenv_refine ?with_evars ~with_classes clenv + end + +(* [unifyTerms] et [unify] ne semble pas gérer les Meta, en + particulier ne semblent pas vérifier que des instances différentes + d'une même Meta sont compatibles. D'ailleurs le "fst" jette les metas + provenant de w_Unify. (Utilisé seulement dans prolog.ml) *) + +let fail_quick_core_unif_flags = { + modulo_conv_on_closed_terms = Some TransparentState.full; + use_metas_eagerly_in_conv_on_closed_terms = false; + use_evars_eagerly_in_conv_on_closed_terms = false; + modulo_delta = TransparentState.empty; + modulo_delta_types = TransparentState.full; + check_applied_meta_types = false; + use_pattern_unification = false; + use_meta_bound_pattern_unification = true; (* ? *) + allowed_evars = AllowAll; + restrict_conv_on_strict_subterms = false; (* ? *) + modulo_betaiota = false; + modulo_eta = true; +} + +let fail_quick_unif_flags = { + core_unify_flags = fail_quick_core_unif_flags; + merge_unify_flags = fail_quick_core_unif_flags; + subterm_unify_flags = fail_quick_core_unif_flags; + allow_K_in_toplevel_higher_order_unification = false; + resolve_evars = false +} + +(* let unifyTerms m n = walking (fun wc -> fst (w_Unify CONV m n [] wc)) *) +let unify ?(flags=fail_quick_unif_flags) m = + Proofview.Goal.enter begin fun gl -> + let env = Tacmach.New.pf_env gl in + let n = Tacmach.New.pf_concl gl in + let evd = clear_metas (Tacmach.New.project gl) in + try + let evd' = w_unify env evd CONV ~flags m n in + Proofview.Unsafe.tclEVARSADVANCE evd' + with e when CErrors.noncritical e -> + let info = Exninfo.reify () in + Proofview.tclZERO ~info e + end + (****************************************************************) (* Clausal environment for an application *) diff --git a/proofs/clenv.mli b/proofs/clenv.mli index 4279ab4768..fd1e2fe593 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -37,9 +37,6 @@ val clenv_value : clausenv -> constr (** type of clenv (instantiated) *) val clenv_type : clausenv -> types -(** substitute resolved metas *) -val clenv_nf_meta : clausenv -> EConstr.constr -> EConstr.constr - (** type of a meta in clenv context *) val clenv_meta_type : clausenv -> metavariable -> types @@ -62,18 +59,8 @@ val clenv_fchain : val clenv_unify : ?flags:unify_flags -> conv_pb -> constr -> constr -> clausenv -> clausenv -(** unifies the concl of the goal with the type of the clenv *) -val clenv_unique_resolver : - ?flags:unify_flags -> clausenv -> Proofview.Goal.t -> clausenv - -val clenv_dependent : clausenv -> metavariable list - -val clenv_pose_metas_as_evars : clausenv -> metavariable list -> clausenv * Evar.t list - (** {6 Bindings } *) -type arg_bindings = constr explicit_bindings - (** bindings where the key is the position in the template of the clenv (dependent or not). Positions can be negative meaning to start from the rightmost argument of the template. *) @@ -109,6 +96,14 @@ val make_clenv_binding : exception NotExtensibleClause val clenv_push_prod : clausenv -> clausenv +(** {6 Clenv tactics} *) + +val unify : ?flags:unify_flags -> constr -> unit Proofview.tactic +val res_pf : ?with_evars:bool -> ?with_classes:bool -> ?flags:unify_flags -> clausenv -> unit Proofview.tactic + +val clenv_pose_dependent_evars : ?with_evars:bool -> clausenv -> clausenv +val clenv_value_cast_meta : clausenv -> constr + (** {6 Pretty-print (debug only) } *) val pr_clenv : clausenv -> Pp.t diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml deleted file mode 100644 index 007d53f911..0000000000 --- a/proofs/clenvtac.ml +++ /dev/null @@ -1,135 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* <O___,, * (see version control and CREDITS file for authors & dates) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Util -open Constr -open Termops -open Evd -open EConstr -open Logic -open Reduction -open Clenv - -(* This function put casts around metavariables whose type could not be - * inferred by the refiner, that is head of applications, predicates and - * subject of Cases. - * Does check that the casted type is closed. Anyway, the refiner would - * fail in this case... *) - -let clenv_cast_meta clenv = - let rec crec u = - match EConstr.kind clenv.evd u with - | App _ | Case _ -> crec_hd u - | Cast (c,_,_) when isMeta clenv.evd c -> u - | Proj (p, c) -> mkProj (p, crec_hd c) - | _ -> EConstr.map clenv.evd crec u - - and crec_hd u = - match EConstr.kind clenv.evd (strip_outer_cast clenv.evd u) with - | Meta mv -> - (try - let b = Typing.meta_type clenv.env clenv.evd mv in - assert (not (occur_meta clenv.evd b)); - if occur_meta clenv.evd b then u - else mkCast (mkMeta mv, DEFAULTcast, b) - with Not_found -> u) - | App(f,args) -> mkApp (crec_hd f, Array.map crec args) - | Case(ci,p,c,br) -> - mkCase (ci, crec_hd p, crec_hd c, Array.map crec br) - | Proj (p, c) -> mkProj (p, crec_hd c) - | _ -> u - in - crec - -let clenv_value_cast_meta clenv = - clenv_cast_meta clenv (clenv_value clenv) - -let clenv_pose_dependent_evars ?(with_evars=false) clenv = - let dep_mvs = clenv_dependent clenv in - let env, sigma = clenv.env, clenv.evd in - if not (List.is_empty dep_mvs) && not with_evars then - raise - (RefinerError (env, sigma, UnresolvedBindings (List.map (meta_name clenv.evd) dep_mvs))); - clenv_pose_metas_as_evars clenv dep_mvs - -let clenv_refine ?(with_evars=false) ?(with_classes=true) clenv = - Proofview.Goal.enter begin fun gl -> - let clenv, evars = clenv_pose_dependent_evars ~with_evars clenv in - let evd' = - if with_classes then - let evd' = - Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars - ~fail:(not with_evars) clenv.env clenv.evd - in - (* After an apply, all the subgoals including those dependent shelved ones are in - the hands of the user and resolution won't be called implicitely on them. *) - Typeclasses.make_unresolvables (fun x -> true) evd' - else clenv.evd - in - let clenv = { clenv with evd = evd' } in - Proofview.tclTHEN - (Proofview.Unsafe.tclEVARS (Evd.clear_metas evd')) - (refiner ~check:false EConstr.Unsafe.(to_constr (clenv_cast_meta clenv (clenv_value clenv)))) - end - -let clenv_pose_dependent_evars ?(with_evars=false) clenv = - fst (clenv_pose_dependent_evars ~with_evars clenv) - -open Unification - -let dft = default_unify_flags - -let res_pf ?with_evars ?(with_classes=true) ?(flags=dft ()) clenv = - Proofview.Goal.enter begin fun gl -> - let clenv = clenv_unique_resolver ~flags clenv gl in - clenv_refine ?with_evars ~with_classes clenv - end - -(* [unifyTerms] et [unify] ne semble pas gérer les Meta, en - particulier ne semblent pas vérifier que des instances différentes - d'une même Meta sont compatibles. D'ailleurs le "fst" jette les metas - provenant de w_Unify. (Utilisé seulement dans prolog.ml) *) - -let fail_quick_core_unif_flags = { - modulo_conv_on_closed_terms = Some TransparentState.full; - use_metas_eagerly_in_conv_on_closed_terms = false; - use_evars_eagerly_in_conv_on_closed_terms = false; - modulo_delta = TransparentState.empty; - modulo_delta_types = TransparentState.full; - check_applied_meta_types = false; - use_pattern_unification = false; - use_meta_bound_pattern_unification = true; (* ? *) - allowed_evars = AllowAll; - restrict_conv_on_strict_subterms = false; (* ? *) - modulo_betaiota = false; - modulo_eta = true; -} - -let fail_quick_unif_flags = { - core_unify_flags = fail_quick_core_unif_flags; - merge_unify_flags = fail_quick_core_unif_flags; - subterm_unify_flags = fail_quick_core_unif_flags; - allow_K_in_toplevel_higher_order_unification = false; - resolve_evars = false -} - -(* let unifyTerms m n = walking (fun wc -> fst (w_Unify CONV m n [] wc)) *) -let unify ?(flags=fail_quick_unif_flags) m = - Proofview.Goal.enter begin fun gl -> - let env = Tacmach.New.pf_env gl in - let n = Tacmach.New.pf_concl gl in - let evd = clear_metas (Tacmach.New.project gl) in - try - let evd' = w_unify env evd CONV ~flags m n in - Proofview.Unsafe.tclEVARSADVANCE evd' - with e when CErrors.noncritical e -> - let info = Exninfo.reify () in - Proofview.tclZERO ~info e - end diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli deleted file mode 100644 index 6eafca359b..0000000000 --- a/proofs/clenvtac.mli +++ /dev/null @@ -1,23 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* <O___,, * (see version control and CREDITS file for authors & dates) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -(** Legacy components of the previous proof engine. *) - -open Clenv -open EConstr -open Unification - -(** Tactics *) -val unify : ?flags:unify_flags -> constr -> unit Proofview.tactic -val clenv_refine : ?with_evars:bool -> ?with_classes:bool -> clausenv -> unit Proofview.tactic -val res_pf : ?with_evars:bool -> ?with_classes:bool -> ?flags:unify_flags -> clausenv -> unit Proofview.tactic - -val clenv_pose_dependent_evars : ?with_evars:bool -> clausenv -> clausenv -val clenv_value_cast_meta : clausenv -> constr diff --git a/proofs/logic.ml b/proofs/logic.ml index c7a1c32e7c..07ea2ea572 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -20,7 +20,6 @@ open Environ open Reductionops open Inductiveops open Typing -open Type_errors open Retyping module NamedDecl = Context.Named.Declaration @@ -40,34 +39,6 @@ type refiner_error = exception RefinerError of Environ.env * Evd.evar_map * refiner_error -open Pretype_errors - -(** FIXME: this is quite brittle. Why not accept any PretypeError? *) -let is_typing_error = function -| UnexpectedType (_, _) | NotProduct _ -| VarNotFound _ | TypingError _ -> true -| _ -> false - -let is_unification_error = function -| CannotUnify _ | CannotUnifyLocal _| CannotGeneralize _ -| NoOccurrenceFound _ | CannotUnifyBindingType _ -| ActualTypeNotCoercible _ | UnifOccurCheck _ -| CannotFindWellTypedAbstraction _ | WrongAbstractionType _ -| UnsolvableImplicit _| AbstractionOverMeta _ -| UnsatisfiableConstraints _ -> true -| _ -> false - -let catchable_exception = function - | CErrors.UserError _ | TypeError _ - | Proof.OpenProof _ - (* abstract will call close_proof inside a tactic *) - | RefinerError _ | Indrec.RecursionSchemeError _ - | Nametab.GlobalizationError _ - (* reduction errors *) - | Tacred.ReductionTacticError _ -> true - (* unification and typing errors *) - | PretypeError(_,_, e) -> is_unification_error e || is_typing_error e - | _ -> false let error_no_such_hypothesis env sigma id = raise (RefinerError (env, sigma, NoSuchHyp id)) diff --git a/proofs/logic.mli b/proofs/logic.mli index 9dc75000a1..21757e47dc 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -47,9 +47,6 @@ exception RefinerError of Environ.env * evar_map * refiner_error val error_no_such_hypothesis : Environ.env -> evar_map -> Id.t -> 'a -val catchable_exception : exn -> bool -[@@ocaml.deprecated "This function does not scale in the presence of dynamically added exceptions. Use instead CErrors.noncritical, or the exact name of the exception that matters in the corresponding case."] - (** Move destination for hypothesis *) type 'id move_location = diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib index 756fef0511..790a9dd2cc 100644 --- a/proofs/proofs.mllib +++ b/proofs/proofs.mllib @@ -9,4 +9,3 @@ Proof_bullet Refiner Tacmach Clenv -Clenvtac diff --git a/stm/stm.ml b/stm/stm.ml index b72cee7a9d..943c83ecd3 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1932,8 +1932,7 @@ end = struct (* {{{ *) List.for_all (Context.Named.Declaration.for_all is_ground) Evd.(evar_context g)) then - CErrors.user_err ~hdr:"STM" Pp.(strbrk("the par: goal selector supports ground "^ - "goals only")) + CErrors.user_err ~hdr:"STM" Pp.(strbrk("The par: goal selector does not support goals with existential variables")) else begin let (i, ast) = r_ast in PG_compat.map_proof (fun p -> Proof.focus focus_cond () i p); @@ -1950,10 +1949,15 @@ end = struct (* {{{ *) | Evd.Evar_empty -> RespNoProgress | Evd.Evar_defined t -> let t = Evarutil.nf_evar sigma t in - if Evarutil.is_ground_term sigma t then + let evars = Evarutil.undefined_evars_of_term sigma t in + if Evar.Set.is_empty evars then let t = EConstr.Unsafe.to_constr t in RespBuiltSubProof (t, Evd.evar_universe_context sigma) - else CErrors.user_err ~hdr:"STM" Pp.(str"The solution is not ground") + else + CErrors.user_err ~hdr:"STM" + Pp.(str"The par: selector requires a tactic that makes no progress or fully" ++ + str" solves the goal and leaves no unresolved existential variables. The following" ++ + str" existentials remain unsolved: " ++ prlist (Termops.pr_existential_key sigma) (Evar.Set.elements evars)) end) () with e when CErrors.noncritical e -> RespError (CErrors.print e) diff --git a/tactics/auto.ml b/tactics/auto.ml index f041af1db1..3287c1c354 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -99,8 +99,7 @@ let connect_hint_clenv h gl = let unify_resolve flags (h : hint) = Proofview.Goal.enter begin fun gl -> let clenv, c = connect_hint_clenv h gl in - let clenv = clenv_unique_resolver ~flags clenv gl in - Clenvtac.clenv_refine clenv + Clenv.res_pf ~flags clenv end let unify_resolve_nodelta h = unify_resolve auto_unif_flags h diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 484aab2f00..4156d5f0ee 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -14,7 +14,6 @@ *) open Pp -open CErrors open Util open Names open Term @@ -159,27 +158,17 @@ let e_give_exact flags h = in let (sigma, t1) = Typing.type_of (pf_env gl) sigma c in Proofview.Unsafe.tclEVARS sigma <*> - Clenvtac.unify ~flags t1 <*> exact_no_check c - end - -let clenv_unique_resolver_tac with_evars ~flags clenv' = - Proofview.Goal.enter begin fun gls -> - let resolve = - try Proofview.tclUNIT (clenv_unique_resolver ~flags clenv' gls) - with e when noncritical e -> - let _, info = Exninfo.capture e in - Proofview.tclZERO ~info e - in resolve >>= fun clenv' -> - Clenvtac.clenv_refine ~with_evars ~with_classes:false clenv' + Clenv.unify ~flags t1 <*> exact_no_check c end let unify_e_resolve flags = begin fun gls (h, _) -> let clenv', c = connect_hint_clenv h gls in - clenv_unique_resolver_tac true ~flags clenv' end + Clenv.res_pf ~with_evars:true ~with_classes:false ~flags clenv' + end let unify_resolve flags = begin fun gls (h, _) -> let clenv', _ = connect_hint_clenv h gls in - clenv_unique_resolver_tac false ~flags clenv' + Clenv.res_pf ~with_evars:false ~with_classes:false ~flags clenv' end (** Application of a lemma using [refine] instead of the old [w_unify] *) @@ -446,10 +435,6 @@ let e_possible_resolve db_list local_db secvars only_classes env sigma concl = let cut_of_hints h = List.fold_left (fun cut db -> PathOr (Hint_db.cut db, cut)) PathEmpty h -let catchable = function - | Refiner.FailError _ -> true - | e -> Logic.catchable_exception e [@@ocaml.warning "-3"] - let pr_depth l = let rec fmt elts = match elts with diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli index b97b90d777..381f68f14f 100644 --- a/tactics/class_tactics.mli +++ b/tactics/class_tactics.mli @@ -15,9 +15,6 @@ open EConstr val typeclasses_db : string -val catchable : exn -> bool -[@@ocaml.deprecated "Use instead CErrors.noncritical, or the exact name of the exception that matters in the corresponding case."] - val set_typeclasses_debug : bool -> unit val set_typeclasses_depth : int option -> unit diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 90e4aaa167..d275e15255 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -37,7 +37,7 @@ let e_give_exact ?(flags=eauto_unif_flags) c = if occur_existential sigma t1 || occur_existential sigma t2 then Tacticals.New.tclTHENLIST [Proofview.Unsafe.tclEVARS sigma; - Clenvtac.unify ~flags t1; + Clenv.unify ~flags t1; exact_no_check c] else exact_check c end @@ -68,8 +68,7 @@ open Auto let unify_e_resolve flags h = Proofview.Goal.enter begin fun gl -> let clenv', c = connect_hint_clenv h gl in - let clenv' = clenv_unique_resolver ~flags clenv' gl in - Clenvtac.clenv_refine ~with_evars:true ~with_classes:true clenv' + Clenv.res_pf ~with_evars:true ~with_classes:true ~flags clenv' end let hintmap_of sigma secvars concl = diff --git a/tactics/equality.ml b/tactics/equality.ml index 79b6dfe920..39017c946f 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -154,7 +154,7 @@ let instantiate_lemma_all frzevars gl c ty l l2r concl = let c1 = args.(arglen - 2) in let c2 = args.(arglen - 1) in let try_occ (evd', c') = - Clenvtac.clenv_pose_dependent_evars ~with_evars:true {eqclause with evd = evd'} + Clenv.clenv_pose_dependent_evars ~with_evars:true {eqclause with evd = evd'} in let flags = make_flags frzevars (Tacmach.New.project gl) rewrite_unif_flags eqclause in let occs = @@ -1045,7 +1045,7 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn = discrimination_pf e (t,t1,t2) discriminator lbeq false_kind >>= fun pf -> let pf_ty = mkArrow eqn Sorts.Relevant false_0 in let absurd_clause = apply_on_clause (pf,pf_ty) eq_clause in - let pf = Clenvtac.clenv_value_cast_meta absurd_clause in + let pf = Clenv.clenv_value_cast_meta absurd_clause in tclTHENS (assert_after Anonymous false_0) [onLastHypId gen_absurdity; (Refiner.refiner ~check:true EConstr.Unsafe.(to_constr pf))] @@ -1067,7 +1067,7 @@ let onEquality with_evars tac (c,lbindc) = let t = pf_get_type_of gl c in let t' = try snd (reduce_to_quantified_ind t) with UserError _ -> t in let eq_clause = pf_apply make_clenv_binding gl (c,t') lbindc in - let eq_clause' = Clenvtac.clenv_pose_dependent_evars ~with_evars eq_clause in + let eq_clause' = Clenv.clenv_pose_dependent_evars ~with_evars eq_clause in let eqn = clenv_type eq_clause' in (* FIXME evar leak *) let (eq,u,eq_args) = pf_apply find_this_eq_data_decompose gl eqn in @@ -1397,7 +1397,7 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac = let pf = applist(congr,[t;resty;injfun;t1;t2]) in let sigma, pf_typ = Typing.type_of env sigma pf in let inj_clause = apply_on_clause (pf,pf_typ) eq_clause in - let pf = Clenvtac.clenv_value_cast_meta inj_clause in + let pf = Clenv.clenv_value_cast_meta inj_clause in let ty = simplify_args env sigma (clenv_type inj_clause) in evdref := sigma; Some (pf, ty) diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index a4d306c497..22c5bbe73f 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -140,9 +140,7 @@ let ifOnHyp pred tac1 tac2 id gl = type branch_args = { ity : pinductive; (* the type we were eliminating on *) - largs : constr list; (* its arguments *) branchnum : int; (* the branch number *) - pred : constr; (* the predicate we used *) nassums : int; (* number of assumptions/letin to be introduced *) branchsign : bool list; (* the signature of the branch. true=assumption, false=let-in *) @@ -686,22 +684,18 @@ module New = struct | None -> elimclause' | Some p -> clenv_unify ~flags Reduction.CONV (mkMeta pmv) p elimclause' in - let clenv' = clenv_unique_resolver ~flags elimclause' gl in let after_tac i = - let (hd,largs) = decompose_app clenv'.evd clenv'.templtyp.Evd.rebus in let ba = { branchsign = branchsigns.(i); branchnames = brnames.(i); nassums = List.length branchsigns.(i); branchnum = i+1; - ity = ind; - largs = List.map (clenv_nf_meta clenv') largs; - pred = clenv_nf_meta clenv' hd } + ity = ind; } in tac ba in let branchtacs = List.init (Array.length branchsigns) after_tac in Proofview.tclTHEN - (Clenvtac.clenv_refine clenv') + (Clenv.res_pf ~flags elimclause') (Proofview.tclEXTEND [] tclIDTAC branchtacs) end) end diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index eebe702259..88419af836 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -89,9 +89,7 @@ val onClauseLR : (Id.t option -> tactic) -> clause -> tactic type branch_args = private { ity : pinductive; (** the type we were eliminating on *) - largs : constr list; (** its arguments *) branchnum : int; (** the branch number *) - pred : constr; (** the predicate we used *) nassums : int; (** number of assumptions/letin to be introduced *) branchsign : bool list; (** the signature of the branch. true=assumption, false=let-in *) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 65f79b6a51..3133f9be1e 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1373,7 +1373,7 @@ let do_replace id = function [id] is replaced by P using the proof given by [tac] *) let clenv_refine_in ?err with_evars targetid id sigma0 clenv tac = - let clenv = Clenvtac.clenv_pose_dependent_evars ~with_evars clenv in + let clenv = Clenv.clenv_pose_dependent_evars ~with_evars clenv in let clenv = { clenv with evd = Typeclasses.resolve_typeclasses ~fail:(not with_evars) clenv.env clenv.evd } @@ -1475,7 +1475,7 @@ let general_elim_clause with_evars flags where indclause elim = match where with | None -> let elimclause = clenv_fchain ~flags indmv elimclause indclause in - Clenvtac.res_pf elimclause ~with_evars ~with_classes:true ~flags + Clenv.res_pf elimclause ~with_evars ~with_classes:true ~flags | Some id -> let hypmv = match List.remove Int.equal indmv (clenv_independent elimclause) with @@ -1737,7 +1737,7 @@ let general_apply ?(respect_opaque=false) with_delta with_destruct with_evars let n = nb_prod_modulo_zeta sigma thm_ty - nprod in if n<0 then error "Applied theorem does not have enough premises."; let clause = make_clenv_binding_apply env sigma (Some n) (c,thm_ty) lbind in - Clenvtac.res_pf clause ~with_evars ~flags + Clenv.res_pf clause ~with_evars ~flags with exn when noncritical exn -> let exn, info = Exninfo.capture exn in Proofview.tclZERO ~info exn @@ -4371,8 +4371,7 @@ let induction_tac with_evars params indvars elim = (* elimclause' is built from elimclause by instantiating all args and params. *) let elimclause' = recolle_clenv i params indvars elimclause gl in (* one last resolution (useless?) *) - let resolved = clenv_unique_resolver ~flags:(elim_flags ()) elimclause' gl in - Clenvtac.clenv_refine ~with_evars resolved + Clenv.res_pf ~with_evars ~flags:(elim_flags ()) elimclause' end (* Apply induction "in place" taking into account dependent @@ -4813,7 +4812,7 @@ let elim_scheme_type elim t = (* t is inductive, then CUMUL or CONV is irrelevant *) clenv_unify ~flags:(elim_flags ()) Reduction.CUMUL t (clenv_meta_type clause mv) clause in - Clenvtac.res_pf clause' ~flags:(elim_flags ()) ~with_evars:false + Clenv.res_pf clause' ~flags:(elim_flags ()) ~with_evars:false | _ -> anomaly (Pp.str "elim_scheme_type.") end |