diff options
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/functional_principles_types.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/g_indfun.ml4 | 2 | ||||
| -rw-r--r-- | plugins/funind/indfun.ml | 1 | ||||
| -rw-r--r-- | plugins/funind/indfun_common.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 4 |
5 files changed, 6 insertions, 5 deletions
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 88693c196..05cdd288c 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -645,7 +645,7 @@ let build_case_scheme fa = (* Constrintern.global_reference id *) (* in *) let funs = (fun (_,f,_) -> - try Universes.constr_of_global (Nametab.global f) + try Universes.unsafe_constr_of_global (Nametab.global f) with Not_found -> Errors.error ("Cannot find "^ Libnames.string_of_reference f)) fa in let first_fun,u = destConst funs in diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 3802aa365..90282fcf7 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -163,7 +163,7 @@ VERNAC COMMAND EXTEND Function (Vernacexpr.VernacFixpoint(None, List.map snd recsl)) with | Vernacexpr.VtSideff ids, _ when hard -> - Vernacexpr.(VtStartProof ("Classic", GuaranteesOpacity, ids), VtLater) + Vernacexpr.(VtStartProof ("Classic", GuaranteesOpacity, ids, false), VtLater) | x -> x ] -> [ do_generate_principle false (List.map snd recsl) ] END diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index d98f824e8..d6ad5575b 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -181,6 +181,7 @@ let is_rec names = let rec lookup names = function | GVar(_,id) -> check_id id names | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ -> false + | GProj (loc, p, c) -> lookup names c | GCast(_,b,_) -> lookup names b | GProj _ -> error "GProj not handled" | GRec _ -> error "GRec not handled" diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 8cccb0bed..5d9c226b7 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -166,7 +166,7 @@ let save with_clean id const (locality,_,kind) hook = let cook_proof _ = - let (id,(entry,strength)) = Pfedit.cook_proof () in + let (id,(entry,_,strength)) = Pfedit.cook_proof () in (id,(entry,strength)) let get_proof_clean do_reduce = diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 96bf4c921..50e7507f4 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -75,7 +75,7 @@ let type_of_const t = Const sp -> Typeops.type_of_constant (Global.env()) sp |_ -> assert false -let constr_of_global = Universes.constr_of_global +let constr_of_global = Universes.unsafe_constr_of_global let constant sl s = constr_of_global (find_reference sl s) @@ -1016,7 +1016,7 @@ let compute_terminate_type nb_args func = delayed_force nat, (mkProd (Name k_id, delayed_force nat, mkArrow cond result))))|])in - let value = mkApp(delayed_force coq_sig, + let value = mkApp(constr_of_global (delayed_force coq_sig_ref), [|b; (mkLambda (Name v_id, b, nb_iter))|]) in compose_prod rev_args value |