diff options
| -rw-r--r-- | proofs/logic.ml | 29 | ||||
| -rw-r--r-- | proofs/logic.mli | 3 | ||||
| -rw-r--r-- | stm/stm.ml | 12 | ||||
| -rw-r--r-- | tactics/class_tactics.ml | 4 | ||||
| -rw-r--r-- | tactics/class_tactics.mli | 3 |
5 files changed, 8 insertions, 43 deletions
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/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/class_tactics.ml b/tactics/class_tactics.ml index 5ad21c2a5b..4156d5f0ee 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -435,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 |