diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/logic.ml | 40 | ||||
| -rw-r--r-- | proofs/proof_type.ml | 1 | ||||
| -rw-r--r-- | proofs/proof_type.mli | 1 | ||||
| -rw-r--r-- | proofs/tacmach.ml | 5 | ||||
| -rw-r--r-- | proofs/tacmach.mli | 1 |
5 files changed, 48 insertions, 0 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml index b9cff0527..a7538193b 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -113,6 +113,35 @@ let clear_hyps2 sigma ids sign t cl = (* The ClearBody tactic *) +let recheck_typability (what,id) env sigma t = + try check_typability env sigma t + with e when Errors.noncritical e -> + let s = match what with + | None -> "the conclusion" + | Some id -> "hypothesis "^(Id.to_string id) in + error + ("The correctness of "^s^" relies on the body of "^(Id.to_string id)) + +let remove_hyp_body env sigma id = + let sign = + apply_to_hyp_and_dependent_on (named_context_val env) id + (fun (_,c,t) _ -> + match c with + | None -> error ((Id.to_string id)^" is not a local definition.") + | Some c ->(id,None,t)) + (fun (id',c,t as d) sign -> + (if !check then + begin + let env = reset_with_named_context sign env in + match c with + | None -> recheck_typability (Some id',id) env sigma t + | Some b -> + let b' = mkCast (b,DEFAULTcast, t) in + recheck_typability (Some id',id) env sigma b' + end;d)) + in + reset_with_named_context sign env + (* Reordering of the context *) (* faire le minimum d'echanges pour que l'ordre donne soit un *) @@ -679,6 +708,17 @@ let prim_refiner r sigma goal = let sigma = Goal.V82.partial_solution sigma goal ev in ([gl], sigma) + | ThinBody ids -> + let clear_aux env id = + let env' = remove_hyp_body env sigma id in + if !check then recheck_typability (None,id) env' sigma cl; + env' + in + let sign' = named_context_val (List.fold_left clear_aux env ids) in + let (sg,ev,sigma) = mk_goal sign' cl in + let sigma = Goal.V82.partial_solution sigma goal ev in + ([sg], sigma) + | Move (withdep, hfrom, hto) -> let (left,right,declfrom,toleft) = split_sign hfrom hto (named_context_of_val sign) in diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index 76459a59a..7297706e1 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -35,6 +35,7 @@ type prim_rule = | Convert_concl of types * cast_kind | Convert_hyp of named_declaration | Thin of Id.t list + | ThinBody of Id.t list | Move of bool * Id.t * Id.t move_location | Rename of Id.t * Id.t diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index bbb2c8e09..0aadd862b 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -27,6 +27,7 @@ type prim_rule = | Convert_concl of types * cast_kind | Convert_hyp of named_declaration | Thin of Id.t list + | ThinBody of Id.t list | Move of bool * Id.t * Id.t move_location | Rename of Id.t * Id.t diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 6c72009d4..f87d03183 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -127,6 +127,10 @@ let convert_hyp_no_check d gl = let thin_no_check ids gl = if List.is_empty ids then tclIDTAC gl else refiner (Thin ids) gl +(* This does not check dependencies *) +let thin_body_no_check ids gl = + if List.is_empty ids then tclIDTAC gl else refiner (ThinBody ids) gl + let move_hyp_no_check with_dep id1 id2 gl = refiner (Move (with_dep,id1,id2)) gl @@ -151,6 +155,7 @@ let refine c = with_check (refine_no_check c) let convert_concl d sty = with_check (convert_concl_no_check d sty) let convert_hyp d = with_check (convert_hyp_no_check d) let thin c = with_check (thin_no_check c) +let thin_body c = with_check (thin_body_no_check c) let move_hyp b id id' = with_check (move_hyp_no_check b id id') let rename_hyp l = with_check (rename_hyp_no_check l) diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index cebe78ed0..c7729e416 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -100,6 +100,7 @@ val refine : constr -> tactic val convert_concl : types -> cast_kind -> tactic val convert_hyp : named_declaration -> tactic val thin : Id.t list -> tactic +val thin_body : Id.t list -> tactic val move_hyp : bool -> Id.t -> Id.t move_location -> tactic val rename_hyp : (Id.t*Id.t) list -> tactic |