diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenv.ml | 3 | ||||
| -rw-r--r-- | proofs/clenv.mli | 4 | ||||
| -rw-r--r-- | proofs/clenvtac.mli | 2 | ||||
| -rw-r--r-- | proofs/goal.mli | 4 | ||||
| -rw-r--r-- | proofs/logic.mli | 2 | ||||
| -rw-r--r-- | proofs/pfedit.mli | 2 | ||||
| -rw-r--r-- | proofs/proof_type.mli | 27 | ||||
| -rw-r--r-- | proofs/proof_using.mli | 2 | ||||
| -rw-r--r-- | proofs/proofs.mllib | 1 | ||||
| -rw-r--r-- | proofs/redexpr.mli | 2 | ||||
| -rw-r--r-- | proofs/refine.mli | 5 | ||||
| -rw-r--r-- | proofs/refiner.mli | 2 |
12 files changed, 28 insertions, 28 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 1ef0b087ba..78dce0d64c 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -491,7 +491,8 @@ let clenv_unify_binding_type clenv c t u = let evd,c = w_coerce_to_type (cl_env clenv) clenv.evd c t u in TypeProcessed, { clenv with evd = evd }, c with - | PretypeError (_,_,ActualTypeNotCoercible (_,_,NotClean _)) as e -> + | PretypeError (_,_,ActualTypeNotCoercible (_,_, + (NotClean _ | ConversionFailed _))) as e -> raise e | e when precatchable_exception e -> TypeNotProcessed, clenv, c diff --git a/proofs/clenv.mli b/proofs/clenv.mli index 59b166ea01..e9236b1da3 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -6,6 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(** This file defines clausenv, which is a deprecated way to handle open terms + in the proof engine. Most of the API here is legacy except for the + evar-based clauses. *) + open Names open Term open Environ diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli index 00e74a2478..aa091aecda 100644 --- a/proofs/clenvtac.mli +++ b/proofs/clenvtac.mli @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(** Legacy components of the previous proof engine. *) + open Term open Clenv open Tacexpr diff --git a/proofs/goal.mli b/proofs/goal.mli index 8a3d6e815a..6a79c1f451 100644 --- a/proofs/goal.mli +++ b/proofs/goal.mli @@ -6,7 +6,9 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* This module implements the abstract interface to goals *) +(** This module implements the abstract interface to goals. Most of the code + here is useless and should be eventually removed. Consider using + {!Proofview.Goal} instead. *) type goal = Evar.t diff --git a/proofs/logic.mli b/proofs/logic.mli index 9aa4ac2074..2764d28c02 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(** Legacy proof engine. Do not use in newly written code. *) + open Names open Term open Evd diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index cfab8bd630..666730e1af 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(** Global proof state. A quite redundant wrapper on {!Proof_global}. *) + open Loc open Names open Term diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index ef0d52b62d..f7798a0edb 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(** Legacy proof engine. Do not use in newly written code. *) + open Evd open Names open Term @@ -26,31 +28,6 @@ type prim_rule = type rule = prim_rule -(** The type [goal sigma] is the type of subgoal. It has the following form -{v it = \{ evar_concl = [the conclusion of the subgoal] - evar_hyps = [the hypotheses of the subgoal] - evar_body = Evar_Empty; - evar_info = \{ pgm : [The Realizer pgm if any] - lc : [Set of evar num occurring in subgoal] \}\} - sigma = \{ stamp = [an int chardacterizing the ed field, for quick compare] - ed : [A set of existential variables depending in the subgoal] - number of first evar, - it = \{ evar_concl = [the type of first evar] - evar_hyps = [the context of the evar] - evar_body = [the body of the Evar if any] - evar_info = \{ pgm : [Useless ??] - lc : [Set of evars occurring - in the type of evar] \} \}; - ... - number of last evar, - it = \{ evar_concl = [the type of evar] - evar_hyps = [the context of the evar] - evar_body = [the body of the Evar if any] - evar_info = \{ pgm : [Useless ??] - lc : [Set of evars occurring - in the type of evar] \} \} \} v} -*) - type goal = Goal.goal type tactic = goal sigma -> goal list sigma diff --git a/proofs/proof_using.mli b/proofs/proof_using.mli index 1bf38b6908..b2c65412f8 100644 --- a/proofs/proof_using.mli +++ b/proofs/proof_using.mli @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(** Utility code for section variables handling in Proof using... *) + val process_expr : Environ.env -> Vernacexpr.section_subset_expr -> Constr.types list -> Names.Id.t list diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib index 9130a186ba..804a543605 100644 --- a/proofs/proofs.mllib +++ b/proofs/proofs.mllib @@ -2,7 +2,6 @@ Miscprint Goal Evar_refiner Proof_using -Proof_errors Logic Refine Proof diff --git a/proofs/redexpr.mli b/proofs/redexpr.mli index b91911087d..d4c2c4a6c9 100644 --- a/proofs/redexpr.mli +++ b/proofs/redexpr.mli @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(** Interpretation layer of redexprs such as hnf, cbv, etc. *) + open Names open Term open Pattern diff --git a/proofs/refine.mli b/proofs/refine.mli index 17c7e28ca9..a9798b7040 100644 --- a/proofs/refine.mli +++ b/proofs/refine.mli @@ -6,6 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(** The primitive refine tactic used to fill the holes in partial proofs. This + is the recommanded way to write tactics when the proof term is easy to + write down. Note that this is not the user-level refine tactic defined + in Ltac which is actually based on the one below. *) + open Proofview (** {6 The refine tactic} *) diff --git a/proofs/refiner.mli b/proofs/refiner.mli index dd9153a023..6dcafb77a4 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(** Legacy proof engine. Do not use in newly written code. *) + open Evd open Proof_type |