diff options
Diffstat (limited to 'plugins/funind/indfun.ml')
| -rw-r--r-- | plugins/funind/indfun.ml | 25 |
1 files changed, 12 insertions, 13 deletions
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 74c0eb4cc7..f1a9758e80 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -11,7 +11,6 @@ open Glob_term open Declarations open Misctypes open Decl_kinds -open Sigma.Notations module RelDecl = Context.Rel.Declaration @@ -93,7 +92,7 @@ let functional_induction with_clean c princl pat = in let encoded_pat_as_patlist = List.make (List.length args + List.length c_list - 1) None @ [pat] in - List.map2 (fun c pat -> ((None,Tacexpr.ElimOnConstr ({ Tacexpr.delayed = fun env sigma -> Sigma ((c,NoBindings), sigma, Sigma.refl) })),(None,pat),None)) + List.map2 (fun c pat -> ((None,Tacexpr.ElimOnConstr (fun env sigma -> (sigma,(c,NoBindings)) )),(None,pat),None)) (args@c_list) encoded_pat_as_patlist in let princ' = Some (princ,bindings) in @@ -142,7 +141,7 @@ let rec abstract_glob_constr c = function let interp_casted_constr_with_implicits env sigma impls c = Constrintern.intern_gen Pretyping.WithoutTypeConstraint env ~impls - ~allow_patvar:false c + c (* Construct a fixpoint as a Glob_term @@ -200,13 +199,13 @@ let is_rec names = | GIf(b,_,lhs,rhs) -> (lookup names b) || (lookup names lhs) || (lookup names rhs) | GProd(na,_,t,b) | GLambda(na,_,t,b) -> - lookup names t || lookup (Nameops.name_fold Id.Set.remove na names) b + lookup names t || lookup (Nameops.Name.fold_right Id.Set.remove na names) b | GLetIn(na,b,t,c) -> - lookup names b || Option.cata (lookup names) true t || lookup (Nameops.name_fold Id.Set.remove na names) c + lookup names b || Option.cata (lookup names) true t || lookup (Nameops.Name.fold_right Id.Set.remove na names) c | GLetTuple(nal,_,t,b) -> lookup names t || lookup (List.fold_left - (fun acc na -> Nameops.name_fold Id.Set.remove na acc) + (fun acc na -> Nameops.Name.fold_right Id.Set.remove na acc) names nal ) @@ -734,7 +733,7 @@ let rec add_args id new_args = CAst.map (function CAppExpl((None,r,None),new_args) | _ -> b end - | CFix _ | CCoFix _ -> anomaly ~label:"add_args " (Pp.str "todo") + | CFix _ | CCoFix _ -> anomaly ~label:"add_args " (Pp.str "todo.") | CProdN(nal,b1) -> CProdN(List.map (fun (nal,k,b2) -> (nal,k,add_args id new_args b2)) nal, add_args id new_args b1) @@ -782,9 +781,9 @@ let rec add_args id new_args = CAst.map (function Miscops.map_cast_type (add_args id new_args) b2) | CRecord pars -> CRecord (List.map (fun (e,o) -> e, add_args id new_args o) pars) - | CNotation _ -> anomaly ~label:"add_args " (Pp.str "CNotation") - | CGeneralization _ -> anomaly ~label:"add_args " (Pp.str "CGeneralization") - | CDelimiters _ -> anomaly ~label:"add_args " (Pp.str "CDelimiters") + | CNotation _ -> anomaly ~label:"add_args " (Pp.str "CNotation.") + | CGeneralization _ -> anomaly ~label:"add_args " (Pp.str "CGeneralization.") + | CDelimiters _ -> anomaly ~label:"add_args " (Pp.str "CDelimiters.") ) exception Stop of Constrexpr.constr_expr @@ -826,7 +825,7 @@ let rec chop_n_arrow n t = chop_n_arrow new_n t' with Stop t -> t end - | _ -> anomaly (Pp.str "Not enough products") + | _ -> anomaly (Pp.str "Not enough products.") let rec get_args b t : Constrexpr.local_binder_expr list * @@ -856,7 +855,7 @@ let make_graph (f_ref:global_reference) = | _ -> raise (UserError (None, str "Not a function reference") ) in (match Global.body_of_constant_body c_body with - | None -> error "Cannot build a graph over an axiom !" + | None -> error "Cannot build a graph over an axiom!" | Some body -> let env = Global.env () in let sigma = Evd.from_env env in @@ -885,7 +884,7 @@ let make_graph (f_ref:global_reference) = | Constrexpr.CLocalAssum (nal,_,_) -> List.map (fun (loc,n) -> CAst.make ?loc @@ - CRef(Libnames.Ident(loc, Nameops.out_name n),None)) + CRef(Libnames.Ident(loc, Nameops.Name.get_id n),None)) nal | Constrexpr.CLocalPattern _ -> assert false ) |