diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-09-04 17:58:12 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-09-04 18:06:16 +0200 |
commit | 6828b31acdf10cf7987f0e494f6f7505a15b1000 (patch) | |
tree | 98497c88a99aaa7453b605c30957a28b4916937c /proofs/logic.ml | |
parent | 99a70a4e2e19441f29667b243b232f5f9f1059a2 (diff) |
Removing the old implementation of clear_body.
Diffstat (limited to 'proofs/logic.ml')
-rw-r--r-- | proofs/logic.ml | 40 |
1 files changed, 0 insertions, 40 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml index a7538193b..b9cff0527 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -113,35 +113,6 @@ 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 *) @@ -708,17 +679,6 @@ 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 |