diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/logic.ml | 15 | ||||
| -rw-r--r-- | proofs/pfedit.ml | 5 | ||||
| -rw-r--r-- | proofs/pfedit.mli | 3 | ||||
| -rw-r--r-- | proofs/proof_global.ml | 9 |
4 files changed, 22 insertions, 10 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml index 47645d2957..8b48655940 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -340,6 +340,15 @@ let check_conv_leq_goal env sigma arg ty conclty = else raise (RefinerError (BadType (arg,ty,conclty))) else sigma +exception Stop of constr list +let meta_free_prefix a = + try + let _ = Array.fold_left (fun acc a -> + if occur_meta a then raise (Stop acc) + else a :: acc) [] a + in a + with Stop acc -> Array.rev_of_list acc + let goal_type_of env sigma c = if !check then type_of env sigma c else Retyping.get_type_of env sigma c @@ -442,10 +451,10 @@ and mk_hdgoals sigma goal goalacc trm = | App (f,l) -> let (acc',hdty,sigma,applicand) = - if isInd f || isConst f - && not (Array.exists occur_meta l) (* we could be finer *) + if is_template_polymorphic env f then - (goalacc,type_of_global_reference_knowing_parameters env sigma f l,sigma,f) + let l' = meta_free_prefix l in + (goalacc,type_of_global_reference_knowing_parameters env sigma f l',sigma,f) else mk_hdgoals sigma goal goalacc f in let ((acc'',conclty',sigma), args) = mk_arggoals sigma goal acc' hdty l in diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 22262036e7..eeb5770253 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -160,7 +160,8 @@ let solve_by_implicit_tactic env sigma evk = (Environ.named_context env) -> let tac = Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (Errors.UserError ("",Pp.str"Proof is not complete."))) []) in (try - let (ans, _, _) = build_by_tactic env (evi.evar_concl, Evd.get_universe_context_set sigma) tac in - ans + let (ans, _, _) = + build_by_tactic env (evi.evar_concl, Evd.universe_context_set sigma) tac in + fst ans with e when Logic.catchable_exception e -> raise Exit) | _ -> raise Exit diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 3efc644e02..e3df619f82 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -152,7 +152,7 @@ val build_constant_by_tactic : types Univ.in_universe_context_set -> unit Proofview.tactic -> Entries.definition_entry * bool * Universes.universe_opt_subst val build_by_tactic : env -> ?poly:polymorphic -> types Univ.in_universe_context_set -> unit Proofview.tactic -> - constr * bool * Universes.universe_opt_subst + constr Univ.in_universe_context_set * bool * Universes.universe_opt_subst (** Declare the default tactic to fill implicit arguments *) @@ -162,4 +162,5 @@ val declare_implicit_tactic : unit Proofview.tactic -> unit val clear_implicit_tactic : unit -> unit (* Raise Exit if cannot solve *) +(* FIXME: interface: it may incur some new universes etc... *) val solve_by_implicit_tactic : env -> Evd.evar_map -> Evd.evar -> constr diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 9be159640b..12700851aa 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -265,7 +265,7 @@ let get_open_goals () = List.length shelf let nf_body nf b = - let aux (c, t) = (nf c, t) in + let aux ((c, ctx), t) = ((nf c, ctx), t) in Future.chain ~pure:true b aux let close_proof ?feedback_id ~now fpl = @@ -333,12 +333,13 @@ let return_proof () = let eff = Evd.eval_side_effects evd in let evd = Evd.nf_constraints evd in let subst = Evd.universe_subst evd in - let ctx = Evd.universe_context evd in + let ctx = Evd.universe_context_set evd in (** ppedrot: FIXME, this is surely wrong. There is no reason to duplicate side-effects... This may explain why one need to uniquize side-effects thereafter... *) - let proofs = List.map (fun (c, _) -> (Evarutil.nf_evars_universes evd c, eff)) initial_goals in - proofs, (subst, ctx) + let proofs = + List.map (fun (c, _) -> ((Evarutil.nf_evars_universes evd c, ctx), eff)) initial_goals in + proofs, (subst, Univ.ContextSet.to_context ctx) let close_future_proof ~feedback_id proof = close_proof ~feedback_id ~now:false proof |