diff options
| author | Matthieu Sozeau | 2014-04-28 13:42:46 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-05-06 09:59:01 +0200 |
| commit | 6bcefa6a9f6fb70334b5c68e8d17aedec5ca7b13 (patch) | |
| tree | d7bddd4c3110e0482b7d4ee4c6fb9d29a6cb3f30 | |
| parent | 338be26cee38bb97cfbec7e1fd10b74906be8515 (diff) | |
Fix funind w.r.t. universes
| -rw-r--r-- | plugins/funind/indfun_common.ml | 8 | ||||
| -rw-r--r-- | plugins/funind/invfun.ml | 10 |
2 files changed, 12 insertions, 6 deletions
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 5d9c226b7f..0d1e600ee6 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -229,7 +229,7 @@ type function_info = (* let function_table = ref ([] : function_db) *) -let from_function = Summary.ref Cmap.empty ~name:"functions_db_fn" +let from_function = Summary.ref Cmap_env.empty ~name:"functions_db_fn" let from_graph = Summary.ref Indmap.empty ~name:"functions_db_gr" (* @@ -254,7 +254,7 @@ let cache_Function (_,(finfos)) = *) let cache_Function (_,finfos) = - from_function := Cmap.add finfos.function_constant finfos !from_function; + from_function := Cmap_env.add finfos.function_constant finfos !from_function; from_graph := Indmap.add finfos.graph_ind finfos !from_graph @@ -348,7 +348,7 @@ let pr_info f_info = str "graph_ind := " ++ Printer.pr_lconstr (mkInd f_info.graph_ind) ++ fnl () let pr_table tb = - let l = Cmap.fold (fun k v acc -> v::acc) tb [] in + let l = Cmap_env.fold (fun k v acc -> v::acc) tb [] in Pp.prlist_with_sep fnl pr_info l let in_Function : function_info -> Libobject.obj = @@ -372,7 +372,7 @@ let find_or_none id = let find_Function_infos f = - Cmap.find f !from_function + Cmap_env.find f !from_function let find_Function_of_graph ind = diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 072b1ce005..d5640798e2 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -484,7 +484,10 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem observe_tac "idtac" tclIDTAC; tclTHEN_i (observe_tac "functional_induction" ( - apply (mkApp (mkVar principle_id,Array.of_list bindings)) + (fun gl -> + let term = mkApp (mkVar principle_id,Array.of_list bindings) in + let gl', _ty = pf_eapply Typing.e_type_of gl term in + apply term gl') )) (fun i g -> observe_tac ("proving branche "^string_of_int i) (prove_branche i) g ) ] @@ -1117,7 +1120,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g let schemes = Array.of_list scheme in - let _proving_tac = + let proving_tac = prove_fun_complete funs_constr mib.Declarations.mind_packets schemes lemmas_types_infos in Array.iteri @@ -1131,6 +1134,9 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g (Decl_kinds.Global,false(*FIXME*),(Decl_kinds.Proof Decl_kinds.Theorem)) (fst lemmas_types_infos.(i), (*FIXME*)Univ.ContextSet.empty) (fun _ _ -> ()); + ignore (Pfedit.by + (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")") + (proving_tac i)))); do_save (); let finfo = find_Function_infos f_as_constant in let lem_cst,u = destConst (Constrintern.global_reference lem_id) in |