diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-10-08 10:33:20 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-10-13 18:13:20 +0200 |
| commit | 9d0011125da2b24ccf006154ab205c6987fb03d2 (patch) | |
| tree | fb28bab986b15fb05e9d9ddbf0556f0a62f29b54 /plugins/funind | |
| parent | e62984e17cad223448feddeccac0d40e1f604c31 (diff) | |
library/opaqueTables: enable their use in interactive mode
Before this patch opaque tables were only growing, making them unusable
in interactive mode (leak on Undo).
With this patch the opaque tables are functional and part of the env.
I.e. a constant_body can point to the proof term in 2 ways:
1) directly (before the constant is discharged)
2) indirectly, via an int, that is mapped by the opaque table to
the proof term.
This is now consistent in batch/interactive mode
This is step 0 to make an interactive coqtop able to dump a .vo/.vi
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 5 | ||||
| -rw-r--r-- | plugins/funind/functional_principles_types.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/indfun.ml | 2 |
3 files changed, 4 insertions, 5 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index cd3f1a5d4..b740e192a 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -948,8 +948,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num = (* observe (str "rec_args_num := " ++ str (string_of_int (rec_args_num + 1) )); *) let f_def = Global.lookup_constant (fst (destConst f)) in let eq_lhs = mkApp(f,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i))) in - let f_body = Option.get (body_of_constant f_def) - in + let f_body = Option.get (Global.body_of_constant_body f_def)in let params,f_body_with_params = decompose_lam_n nb_params f_body in let (_,num),(_,_,bodies) = destFix f_body_with_params in let fnames_with_params = @@ -1065,7 +1064,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : } in let get_body const = - match body_of_constant (Global.lookup_constant const) with + match Global.body_of_constant const with | Some body -> Tacred.cbv_norm_flags (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA]) diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index c4a340880..41f3a5a8b 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -384,7 +384,7 @@ let get_funs_constant mp dp = in function const -> let find_constant_body const = - match body_of_constant (Global.lookup_constant const) with + match Global.body_of_constant const with | Some body -> let body = Tacred.cbv_norm_flags (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA]) diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index b613a4b13..71ebf4923 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -763,7 +763,7 @@ let make_graph (f_ref:global_reference) = | _ -> raise (UserError ("", str "Not a function reference") ) in Dumpglob.pause (); - (match body_of_constant c_body with + (match Global.body_of_constant_body c_body with | None -> error "Cannot build a graph over an axiom !" | Some body -> let env = Global.env () in |