diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-06-20 20:53:30 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-06-20 20:53:30 +0000 |
| commit | 0e0769892a42d5790efa9e33023c3f4332417add (patch) | |
| tree | 2604265dd5d0c85b343f5fcd5c3bf5744d57f543 | |
| parent | 2efdb17f8104227187f21edefa2d72ad61e676b6 (diff) | |
Wellfounded recursion using subtac working again.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8966 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | contrib/subtac/subtac_command.ml | 31 | ||||
| -rw-r--r-- | contrib/subtac/subtac_utils.ml | 3 | ||||
| -rw-r--r-- | contrib/subtac/subtac_utils.mli | 2 |
3 files changed, 20 insertions, 16 deletions
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml index 247336386..816f03ce4 100644 --- a/contrib/subtac/subtac_command.ml +++ b/contrib/subtac/subtac_command.ml @@ -301,25 +301,24 @@ let build_wellfounded (recname, n, bl,arityc,body) r notation boxed = match evars_sum with | Some (sum_tac, sumg) -> let proofid = id_of_string (string_of_id recname ^ "_evars_proof") in - Command.start_proof proofid goal_kind sumg - (fun _ gr -> - let constant = match gr with Libnames.ConstRef c -> c - | _ -> assert(false) - in - let def = mkConst constant in + Command.start_proof proofid goal_proof_kind sumg + (fun strength gr -> + debug 2 (str "Proof finished"); + let def = constr_of_global gr in let args = Subtac_utils.destruct_ex def sumg in - let args = - List.map (fun c -> - try Reductionops.whd_betadeltaiota (Global.env ()) Evd.empty c - with Not_found -> - trace (str "Not_found while reducing " ++ - my_print_constr (Global.env ()) c); - c - ) args - in let _, newdef = decompose_lam_n (List.length args) evars_def in let constr = Term.substl (List.rev args) newdef in - debug 1 (str "Applied existentials : " ++ my_print_constr env constr)); + debug 2 (str "Applied existentials : " ++ my_print_constr env constr); + let ce = + { const_entry_body = constr; + const_entry_type = Some fullctyp; + const_entry_opaque = false; + const_entry_boxed = boxed} + in + let constant = Declare.declare_constant + recname (DefinitionEntry ce,IsDefinition Definition) + in + definition_message recname); trace (str "Started existentials proof"); Pfedit.by sum_tac; trace (str "Applied sum tac") diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml index 0d3ebe186..6089f3a64 100644 --- a/contrib/subtac/subtac_utils.ml +++ b/contrib/subtac/subtac_utils.ml @@ -156,6 +156,9 @@ let non_instanciated_map env evd = let global_kind = Decl_kinds.IsDefinition Decl_kinds.Definition let goal_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Definition +let global_proof_kind = Decl_kinds.IsProof Decl_kinds.Lemma +let goal_proof_kind = Decl_kinds.Global, Decl_kinds.Proof Decl_kinds.Lemma + let global_fix_kind = Decl_kinds.IsDefinition Decl_kinds.Fixpoint let goal_fix_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Fixpoint diff --git a/contrib/subtac/subtac_utils.mli b/contrib/subtac/subtac_utils.mli index 4b25ff679..a26793b67 100644 --- a/contrib/subtac/subtac_utils.mli +++ b/contrib/subtac/subtac_utils.mli @@ -68,6 +68,8 @@ val string_of_hole_kind : hole_kind -> string val non_instanciated_map : env -> evar_defs ref -> evar_map val global_kind : logical_kind val goal_kind : locality_flag * goal_object_kind +val global_proof_kind : logical_kind +val goal_proof_kind : locality_flag * goal_object_kind val global_fix_kind : logical_kind val goal_fix_kind : locality_flag * goal_object_kind |