diff options
author | aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-02 15:35:34 +0000 |
---|---|---|
committer | aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-02 15:35:34 +0000 |
commit | e6404437c1f6ae451f4253cd3450f75513b395c3 (patch) | |
tree | b8fae579662002cd7a921aa6baa5af6d920204a4 /tactics/tactics.ml | |
parent | 15effb7dedbaa407bbe25055da6efded366dd3b1 (diff) |
Replaced monads.ml by an essentially equivalent proofview_gen.ml generated by extraction.
The goal was to use Coq's partial evaluation capabilities to do manually some
inlining that Ocaml couldn't do. It may be critical as we are defining higher
order combinators in term of others and no inlining means a lot of
unnecessary, short-lived closures built.
With this modification we get back some (but not all) of the loss of performance introduced by threading the monadic type all over the place.
I still have an estimated 15% longer compilation time for Coq.
Makes use of Set Extraction Conservative Types and Set Extraction File Comment
to maintain the relationship between the functions and their types.
Uses an intermediate layer Proofview_monad between Proofview_gen and
Proofview in order to use a hand-written mli to catch potential errors in the
generated file (it uses Extract Constant a lot).
A bug in the extraction of signatures forces to remove the generated
proofview_gen.mli which does not have the correct types.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16981 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/tactics.ml')
-rw-r--r-- | tactics/tactics.ml | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index f6983cba3..3e37ea998 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -3758,6 +3758,7 @@ let abstract_subproof id tac gl = with Uninstantiated_evar _ -> error "\"abstract\" cannot handle existentials." in (* spiwack: the [abstract] tacticals loses the "unsafe status" information *) + try let (const,_) = Pfedit.build_constant_by_tactic id secsign concl (Tacticals.New.tclCOMPLETE (Tacticals.New.tclTHEN (Tacticals.New.tclDO (List.length sign) intro) tac)) in let cd = Entries.DefinitionEntry const in @@ -3772,6 +3773,12 @@ let abstract_subproof id tac gl = exact_no_check (applist (lem,List.rev (instance_from_named_context sign))) gl + with Proof_errors.TacticFailure e -> + (* if the tactic [tac] fails, it reports a [TacticFailure e], + which is an error irrelevant to the proof system (in fact it + means that [e] comes from [tac] failing to yield enough + success). Hence it reraises [e]. *) + raise e let tclABSTRACT name_op tac gl = let s = match name_op with |