diff options
69 files changed, 787 insertions, 518 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 9ba39abdb..a6a27194a 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -100,13 +100,15 @@ before_script: .test-suite-template: &test-suite-template stage: test script: - - set -e - cd test-suite - make clean # careful with the ending / - make -j ${NJOBS} BIN=$(readlink -f ../install/bin)/ LIB=$(readlink -f ../install/lib/coq)/ all - - cat summary.log - - set +e + artifacts: + name: "$CI_JOB_NAME.logs" + when: on_failure + paths: + - test-suite/logs .validate-template: &validate-template stage: test @@ -6,6 +6,9 @@ Tactics - New tactic "extensionality in H" which applies (possibly dependent) functional extensionality in H supposed to be a quantified equality until giving a bare equality. +- Tactic "specialize with ..." now accepts any partial bindings. + Missing bindings are either solved by unification or left quantified + in the hypothesis. - New representation of terms that statically ensure stability by evar-expansion. This has several consequences. * In terms of performance, this adds a cost to every term destructuration, diff --git a/Makefile.build b/Makefile.build index c8aa6d6c1..da736345c 100644 --- a/Makefile.build +++ b/Makefile.build @@ -479,7 +479,6 @@ check: validate test-suite test-suite: world $(ALLSTDLIB).v $(MAKE) $(MAKE_TSOPTS) clean $(MAKE) $(MAKE_TSOPTS) all - $(MAKE) $(MAKE_TSOPTS) report ########################################################################### # Default rules for compiling ML code diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index 7fad65bf0..bcda4ff50 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -51,6 +51,12 @@ In Constrexpr_ops: interpreting "(x y z:_)" as "(x:_) (y:_) (z:_)" while the second ones were preserving the original sharing of the type. +In Nameops: + + The API has been made more uniform. New combinators added in the + "Name" space name. Function "out_name" now fails with IsAnonymous + rather than with Failure "Nameops.out_name". + Location handling and AST attributes: Location handling has been reworked. First, Loc.ghost has been @@ -113,13 +119,17 @@ In Coqlib / reference location: We have removed from Coqlib functions returning `constr` from names. Now it is only possible to obtain references, that must be processed wrt the particular needs of the client. + We have changed in constrintern the functions returnin `constr` as + well to return global references instead. Users of `coq_constant/gen_constant` can do `Universes.constr_of_global (find_reference dir r)` _however_ note the warnings in the `Universes.constr_of_global` in the documentation. It is very likely that you were previously suffering from problems with polymorphic universes due to using - `Coqlib.coq_constant` that used to do this. + `Coqlib.coq_constant` that used to do this. You must rather use + `pf_constr_of_global` in tactics and `Evarutil.new_global` variants + when constructing terms in ML (see univpoly.txt for more information). ** Tactic API ** @@ -127,6 +137,10 @@ In Coqlib / reference location: Thus it only generates one instance of the global reference, and it is the caller's responsibility to perform a focus on the goal. +- pf_global, construct_reference, global_reference, + global_reference_in_absolute_module now return a global_reference + instead of a constr. + - The tclWEAK_PROGRESS and tclNOTSAMEGOAL tacticals were removed. Their usecase was very specific. Use tclPROGRESS instead. diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index def42955f..253eb7f01 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -1384,12 +1384,16 @@ in the list of subgoals remaining to prove. quantifications or non-dependent implications) are instantiated by concrete terms coming either from arguments \term$_1$ $\ldots$ \term$_n$ or from a bindings list (see - Section~\ref{Binding-list} for more about bindings lists). In the - second form, all instantiation elements must be given, whereas - in the first form the application to \term$_1$ {\ldots} + Section~\ref{Binding-list} for more about bindings lists). + In the first form the application to \term$_1$ {\ldots} \term$_n$ can be partial. The first form is equivalent to {\tt assert ({\ident} := {\ident} {\term$_1$} \dots\ \term$_n$)}. + In the second form, instantiation elements can also be partial. + In this case the uninstantiated arguments are inferred by + unification if possible or left quantified in the hypothesis + otherwise. + With the {\tt as} clause, the local hypothesis {\ident} is left unchanged and instead, the modified hypothesis is introduced as specified by the {\intropattern}. diff --git a/engine/eConstr.ml b/engine/eConstr.ml index c0485e4e7..5a05150d4 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -782,6 +782,9 @@ let fresh_global ?loc ?rigid ?names env sigma reference = Sigma.fresh_global ?loc ?rigid ?names env sigma reference in Sigma.Sigma (of_constr t,sigma,p) +let is_global sigma gr c = + Globnames.is_global gr (to_constr sigma c) + module Unsafe = struct let to_sorts = ESorts.unsafe_to_sorts diff --git a/engine/eConstr.mli b/engine/eConstr.mli index 9d705b4d5..9f45187cf 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -261,6 +261,8 @@ val fresh_global : ?loc:Loc.t -> ?rigid:Evd.rigid -> ?names:Univ.Instance.t -> Environ.env -> 'r Sigma.t -> Globnames.global_reference -> (t, 'r) Sigma.sigma +val is_global : Evd.evar_map -> Globnames.global_reference -> t -> bool + (** {5 Extra} *) val of_named_decl : (Constr.t, Constr.types) Context.Named.Declaration.pt -> (t, types) Context.Named.Declaration.pt diff --git a/engine/termops.ml b/engine/termops.ml index 1ec2b8103..cbb0f0779 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -31,10 +31,6 @@ let pr_sort_family = function | InProp -> (str "Prop") | InType -> (str "Type") -let pr_name = function - | Name id -> pr_id id - | Anonymous -> str "_" - let pr_con sp = str(string_of_con sp) let pr_fix pr_constr ((t,i),(lna,tl,bl)) = @@ -42,7 +38,7 @@ let pr_fix pr_constr ((t,i),(lna,tl,bl)) = hov 1 (str"fix " ++ int i ++ spc() ++ str"{" ++ v 0 (prlist_with_sep spc (fun (na,i,ty,bd) -> - pr_name na ++ str"/" ++ int i ++ str":" ++ pr_constr ty ++ + Name.print na ++ str"/" ++ int i ++ str":" ++ pr_constr ty ++ cut() ++ str":=" ++ pr_constr bd) (Array.to_list fixl)) ++ str"}") @@ -65,10 +61,10 @@ let rec pr_constr c = match kind_of_term c with (str"(" ++ pr_constr t ++ str " ->" ++ spc() ++ pr_constr c ++ str")") | Lambda (na,t,c) -> hov 1 - (str"fun " ++ pr_name na ++ str":" ++ + (str"fun " ++ Name.print na ++ str":" ++ pr_constr t ++ str" =>" ++ spc() ++ pr_constr c) | LetIn (na,b,t,c) -> hov 0 - (str"let " ++ pr_name na ++ str":=" ++ pr_constr b ++ + (str"let " ++ Name.print na ++ str":=" ++ pr_constr b ++ str":" ++ brk(1,2) ++ pr_constr t ++ cut() ++ pr_constr c) | App (c,l) -> hov 1 @@ -93,7 +89,7 @@ let rec pr_constr c = match kind_of_term c with hov 1 (str"cofix " ++ int i ++ spc() ++ str"{" ++ v 0 (prlist_with_sep spc (fun (na,ty,bd) -> - pr_name na ++ str":" ++ pr_constr ty ++ + Name.print na ++ str":" ++ pr_constr ty ++ cut() ++ str":=" ++ pr_constr bd) (Array.to_list fixl)) ++ str"}") @@ -309,8 +305,8 @@ let pr_evar_universe_context ctx = let print_env_short env = let print_constr = print_kconstr in let pr_rel_decl = function - | RelDecl.LocalAssum (n,_) -> pr_name n - | RelDecl.LocalDef (n,b,_) -> str "(" ++ pr_name n ++ str " := " ++ print_constr b ++ str ")" + | RelDecl.LocalAssum (n,_) -> Name.print n + | RelDecl.LocalDef (n,b,_) -> str "(" ++ Name.print n ++ str " := " ++ print_constr b ++ str ")" in let pr_named_decl = NamedDecl.to_rel_decl %> pr_rel_decl in let nc = List.rev (named_context env) in diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 4c29fc809..f6da10c96 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -740,7 +740,7 @@ let rec extern inctx scopes vars r = | GCases (sty,rtntypopt,tml,eqns) -> let vars' = - List.fold_right (name_fold Id.Set.add) + List.fold_right (Name.fold_right Id.Set.add) (cases_predicate_names tml) vars in let rtntypopt' = Option.map (extern_typ scopes vars') rtntypopt in let tml = List.map (fun (tm,(na,x)) -> @@ -790,12 +790,12 @@ let rec extern inctx scopes vars r = let (bl,ty,def) = blv.(i), tyv.(i), bv.(i) in let bl = List.map (extended_glob_local_binder_of_decl ?loc) bl in let (assums,ids,bl) = extern_local_binder scopes vars bl in - let vars0 = List.fold_right (name_fold Id.Set.add) ids vars in - let vars1 = List.fold_right (name_fold Id.Set.add) ids vars' in + let vars0 = List.fold_right (Name.fold_right Id.Set.add) ids vars in + let vars1 = List.fold_right (Name.fold_right Id.Set.add) ids vars' in let n = match fst nv.(i) with | None -> None - | Some x -> Some (Loc.tag @@ out_name (List.nth assums x)) + | Some x -> Some (Loc.tag @@ Name.get_id (List.nth assums x)) in let ro = extern_recursion_order scopes vars (snd nv.(i)) in ((Loc.tag fi), (n, ro), bl, extern_typ scopes vars0 ty, @@ -807,8 +807,8 @@ let rec extern inctx scopes vars r = Array.mapi (fun i fi -> let bl = List.map (extended_glob_local_binder_of_decl ?loc) blv.(i) in let (_,ids,bl) = extern_local_binder scopes vars bl in - let vars0 = List.fold_right (name_fold Id.Set.add) ids vars in - let vars1 = List.fold_right (name_fold Id.Set.add) ids vars' in + let vars0 = List.fold_right (Name.fold_right Id.Set.add) ids vars in + let vars1 = List.fold_right (Name.fold_right Id.Set.add) ids vars' in ((Loc.tag fi),bl,extern_typ scopes vars0 tyv.(i), sub_extern false scopes vars1 bv.(i))) idv in @@ -852,14 +852,14 @@ and extern_local_binder scopes vars = function [] -> ([],[],[]) | { v = GLocalDef (na,bk,bd,ty)}::l -> let (assums,ids,l) = - extern_local_binder scopes (name_fold Id.Set.add na vars) l in + extern_local_binder scopes (Name.fold_right Id.Set.add na vars) l in (assums,na::ids, CLocalDef((Loc.tag na), extern false scopes vars bd, Option.map (extern false scopes vars) ty) :: l) | { v = GLocalAssum (na,bk,ty)}::l -> let ty = extern_typ scopes vars ty in - (match extern_local_binder scopes (name_fold Id.Set.add na vars) l with + (match extern_local_binder scopes (Name.fold_right Id.Set.add na vars) l with (assums,ids,CLocalAssum(nal,k,ty')::l) when constr_expr_eq ty ty' && match na with Name id -> not (occur_var_constr_expr id ty') diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 6514ad8be..190369e8f 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -98,16 +98,16 @@ let global_reference_of_reference ref = locate_reference (snd (qualid_of_reference ref)) let global_reference id = - Universes.constr_of_global (locate_reference (qualid_of_ident id)) + locate_reference (qualid_of_ident id) let construct_reference ctx id = try - Term.mkVar (let _ = Context.Named.lookup id ctx in id) + VarRef (let _ = Context.Named.lookup id ctx in id) with Not_found -> global_reference id let global_reference_in_absolute_module dir id = - Universes.constr_of_global (Nametab.global_of_path (Libnames.make_path dir id)) + Nametab.global_of_path (Libnames.make_path dir id) (**********************************************************************) (* Internalization errors *) @@ -536,7 +536,7 @@ let traverse_binder (terms,_,_ as subst) avoid (renaming,env) = function try (* Binders bound in the notation are considered first-order objects *) let _,na = coerce_to_name (fst (Id.Map.find id terms)) in - (renaming,{env with ids = name_fold Id.Set.add na env.ids}), na + (renaming,{env with ids = Name.fold_right Id.Set.add na env.ids}), na with Not_found -> (* Binders not bound in the notation do not capture variables *) (* outside the notation (i.e. in the substitution) *) @@ -1660,7 +1660,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = | CCases (sty, rtnpo, tms, eqns) -> let as_in_vars = List.fold_left (fun acc (_,na,inb) -> Option.fold_left (fun acc tt -> Id.Set.union (ids_of_cases_indtype tt) acc) - (Option.fold_left (fun acc (_,y) -> name_fold Id.Set.add y acc) acc na) + (Option.fold_left (fun acc (_,y) -> Name.fold_right Id.Set.add y acc) acc na) inb) Id.Set.empty tms in (* as, in & return vars *) let forbidden_vars = Option.cata free_vars_of_constr_expr as_in_vars rtnpo in @@ -2071,7 +2071,7 @@ let intern_context global_level env impl_env binders = with InternalizationError (loc,e) -> user_err ?loc ~hdr:"internalize" (explain_internalization_error e) -let interp_rawcontext_evars env evdref k bl = +let interp_glob_context_evars env evdref k bl = let open EConstr in let (env, par, _, impls) = List.fold_left @@ -2100,6 +2100,6 @@ let interp_rawcontext_evars env evdref k bl = let interp_context_evars ?(global_level=false) ?(impl_env=empty_internalization_env) ?(shift=0) env evdref params = let int_env,bl = intern_context global_level env impl_env params in - let x = interp_rawcontext_evars env evdref shift bl in + let x = interp_glob_context_evars env evdref shift bl in int_env, x diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 644cafe57..644f60d85 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -176,9 +176,9 @@ val interp_context_evars : val locate_reference : Libnames.qualid -> Globnames.global_reference val is_global : Id.t -> bool -val construct_reference : ('c, 't) Context.Named.pt -> Id.t -> constr -val global_reference : Id.t -> constr -val global_reference_in_absolute_module : DirPath.t -> Id.t -> constr +val construct_reference : ('c, 't) Context.Named.pt -> Id.t -> Globnames.global_reference +val global_reference : Id.t -> Globnames.global_reference +val global_reference_in_absolute_module : DirPath.t -> Id.t -> Globnames.global_reference (** Interprets a term as the left-hand side of a notation. The returned map is guaranteed to have the same domain as the input one. *) diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index cfc6e6c2a..ade524141 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -264,7 +264,7 @@ let implicits_of_glob_constr ?(with_products=true) l = let () = match bk with | Implicit -> Feedback.msg_warning (strbrk "Ignoring implicit status of product binder " ++ - pr_name na ++ strbrk " and following binders") + Name.print na ++ strbrk " and following binders") | _ -> () in [] | GLambda (na, bk, t, b) -> abs na bk b diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 6f9100911..8e876ec16 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -22,31 +22,6 @@ open Notation_term (**********************************************************************) (* Utilities *) -let on_true_do b f c = if b then (f c; b) else b - -let compare_glob_constr f add t1 t2 = match CAst.(t1.v,t2.v) with - | GRef (r1,_), GRef (r2,_) -> eq_gr r1 r2 - | GVar v1, GVar v2 -> on_true_do (Id.equal v1 v2) add (Name v1) - | GApp (f1,l1), GApp (f2,l2) -> f f1 f2 && List.for_all2eq f l1 l2 - | GLambda (na1,bk1,ty1,c1), GLambda (na2,bk2,ty2,c2) - when Name.equal na1 na2 && Constrexpr_ops.binding_kind_eq bk1 bk2 -> - on_true_do (f ty1 ty2 && f c1 c2) add na1 - | GProd (na1,bk1,ty1,c1), GProd (na2,bk2,ty2,c2) - when Name.equal na1 na2 && Constrexpr_ops.binding_kind_eq bk1 bk2 -> - on_true_do (f ty1 ty2 && f c1 c2) add na1 - | GHole _, GHole _ -> true - | GSort s1, GSort s2 -> Miscops.glob_sort_eq s1 s2 - | GLetIn (na1,b1,t1,c1), GLetIn (na2,b2,t2,c2) when Name.equal na1 na2 -> - on_true_do (f b1 b2 && f c1 c2) add na1 - | (GCases _ | GRec _ - | GPatVar _ | GEvar _ | GLetTuple _ | GIf _ | GCast _),_ - | _,(GCases _ | GRec _ - | GPatVar _ | GEvar _ | GLetTuple _ | GIf _ | GCast _) - -> user_err Pp.(str "Unsupported construction in recursive notations.") - | (GRef _ | GVar _ | GApp _ | GLambda _ | GProd _ - | GHole _ | GSort _ | GLetIn _), _ - -> false - let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with | NRef gr1, NRef gr2 -> eq_gr gr1 gr2 | NVar id1, NVar id2 -> Int.equal (List.index Id.equal id1 vars1) (List.index Id.equal id2 vars2) @@ -184,7 +159,7 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc = e',Some (Loc.tag ?loc (ind,nal')) in let e',na' = g e' na in (e',(f e tm,(na',t'))::tml')) tml (e,[]) in - let fold (idl,e) na = let (e,na) = g e na in ((name_cons na idl,e),na) in + let fold (idl,e) na = let (e,na) = g e na in ((Name.cons na idl,e),na) in let eqnl' = List.map (fun (patl,rhs) -> let ((idl,e),patl) = List.fold_map (cases_pattern_fold_map ?loc fold) ([],e) patl in @@ -287,7 +262,7 @@ let compare_recursive_parts found f f' (iterator,subc) = | Some _ -> false end | GLambda (Name x,_,t_x,c), GLambda (Name y,_,t_y,term) - | GProd (Name x,_,t_x,c), GProd (Name y,_,t_y,term) -> + | GProd (Name x,_,t_x,c), GProd (Name y,_,t_y,term) when not (Id.equal x y) -> (* We found a binding position where it differs *) begin match !diff with | None -> @@ -296,7 +271,7 @@ let compare_recursive_parts found f f' (iterator,subc) = | Some _ -> false end | _ -> - compare_glob_constr aux (add_name found) c1 c2 in + mk_glob_constr_eq aux c1 c2 in if aux iterator subc then match !diff with | None -> diff --git a/interp/topconstr.ml b/interp/topconstr.ml index a79f10df6..94bbc60ea 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -83,13 +83,13 @@ let ids_of_cases_tomatch tms = (fun (_, ona, indnal) l -> Option.fold_right (fun t ids -> cases_pattern_fold_names Id.Set.add ids t) indnal - (Option.fold_right (down_located (name_fold Id.Set.add)) ona l)) + (Option.fold_right (down_located (Name.fold_right Id.Set.add)) ona l)) tms Id.Set.empty let rec fold_constr_expr_binders g f n acc b = function | (nal,bk,t)::l -> let nal = snd (List.split nal) in - let n' = List.fold_right (name_fold g) nal n in + let n' = List.fold_right (Name.fold_right g) nal n in f n (fold_constr_expr_binders g f n' acc b l) t | [] -> f n acc b @@ -97,10 +97,10 @@ let rec fold_constr_expr_binders g f n acc b = function let rec fold_local_binders g f n acc b = function | CLocalAssum (nal,bk,t)::l -> let nal = snd (List.split nal) in - let n' = List.fold_right (name_fold g) nal n in + let n' = List.fold_right (Name.fold_right g) nal n in f n (fold_local_binders g f n' acc b l) t | CLocalDef ((_,na),c,t)::l -> - Option.fold_left (f n) (f n (fold_local_binders g f (name_fold g na n) acc b l) c) t + Option.fold_left (f n) (f n (fold_local_binders g f (Name.fold_right g na n) acc b l) c) t | CLocalPattern (_,(pat,t))::l -> let acc = fold_local_binders g f (cases_pattern_fold_names g n pat) acc b l in Option.fold_left (f n) acc t @@ -112,7 +112,7 @@ let fold_constr_expr_with_binders g f n acc = CAst.with_val (function | CApp ((_,t),l) -> List.fold_left (f n) (f n acc t) (List.map fst l) | CProdN (l,b) | CLambdaN (l,b) -> fold_constr_expr_binders g f n acc b l | CLetIn (na,a,t,b) -> - f (name_fold g (snd na) n) (Option.fold_left (f n) (f n acc a) t) b + f (Name.fold_right g (snd na) n) (Option.fold_left (f n) (f n acc a) t) b | CCast (a,(CastConv b|CastVM b|CastNative b)) -> f n (f n acc a) b | CCast (a,CastCoerce) -> f n acc a | CNotation (_,(l,ll,bll)) -> @@ -133,12 +133,12 @@ let fold_constr_expr_with_binders g f n acc = CAst.with_val (function let ids = ids_of_pattern_list patl in f (Id.Set.fold g ids n) acc rhs) bl acc | CLetTuple (nal,(ona,po),b,c) -> - let n' = List.fold_right (down_located (name_fold g)) nal n in - f (Option.fold_right (down_located (name_fold g)) ona n') (f n acc b) c + let n' = List.fold_right (down_located (Name.fold_right g)) nal n in + f (Option.fold_right (down_located (Name.fold_right g)) ona n') (f n acc b) c | CIf (c,(ona,po),b1,b2) -> let acc = f n (f n (f n acc b1) b2) c in Option.fold_left - (f (Option.fold_right (down_located (name_fold g)) ona n)) acc po + (f (Option.fold_right (down_located (Name.fold_right g)) ona n)) acc po | CFix (_,l) -> let n' = List.fold_right (fun ((_,id),_,_,_,_) -> g id) l n in List.fold_right (fun (_,(_,o),lb,t,c) acc -> @@ -198,7 +198,7 @@ let split_at_annot bl na = (* Used in correctness and interface *) -let map_binder g e nal = List.fold_right (down_located (name_fold g)) nal e +let map_binder g e nal = List.fold_right (down_located (Name.fold_right g)) nal e let map_binders f g e bl = (* TODO: avoid variable capture in [t] by some [na] in [List.tl nal] *) @@ -212,7 +212,7 @@ let map_local_binders f g e bl = CLocalAssum(nal,k,ty) -> (map_binder g e nal, CLocalAssum(nal,k,f e ty)::bl) | CLocalDef((loc,na),c,ty) -> - (name_fold g na e, CLocalDef((loc,na),f e c,Option.map (f e) ty)::bl) + (Name.fold_right g na e, CLocalDef((loc,na),f e c,Option.map (f e) ty)::bl) | CLocalPattern (loc,(pat,t)) -> let ids = ids_of_pattern pat in (Id.Set.fold g ids e, CLocalPattern (loc,(pat,Option.map (f e) t))::bl) in @@ -228,7 +228,7 @@ let map_constr_expr_with_binders g f e = CAst.map (function | CLambdaN (bl,b) -> let (e,bl) = map_binders f g e bl in CLambdaN (bl,f e b) | CLetIn (na,a,t,b) -> - CLetIn (na,f e a,Option.map (f e) t,f (name_fold g (snd na) e) b) + CLetIn (na,f e a,Option.map (f e) t,f (Name.fold_right g (snd na) e) b) | CCast (a,c) -> CCast (f e a, Miscops.map_cast_type (f e) c) | CNotation (n,(l,ll,bll)) -> (* This is an approximation because we don't know what binds what *) @@ -247,11 +247,11 @@ let map_constr_expr_with_binders g f e = CAst.map (function let po = Option.map (f (Id.Set.fold g ids e)) rtnpo in CCases (sty, po, List.map (fun (tm,x,y) -> f e tm,x,y) a,bl) | CLetTuple (nal,(ona,po),b,c) -> - let e' = List.fold_right (down_located (name_fold g)) nal e in - let e'' = Option.fold_right (down_located (name_fold g)) ona e in + let e' = List.fold_right (down_located (Name.fold_right g)) nal e in + let e'' = Option.fold_right (down_located (Name.fold_right g)) ona e in CLetTuple (nal,(ona,Option.map (f e'') po),f e b,f e' c) | CIf (c,(ona,po),b1,b2) -> - let e' = Option.fold_right (down_located (name_fold g)) ona e in + let e' = Option.fold_right (down_located (Name.fold_right g)) ona e in CIf (f e c,(ona,Option.map (f e') po),f e b1,f e b2) | CFix (id,dl) -> CFix (id,List.map (fun (id,n,bl,t,d) -> diff --git a/kernel/names.ml b/kernel/names.ml index afdbe0c0d..ae3403335 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -104,8 +104,12 @@ struct | _ -> false let hash = function - | Anonymous -> 0 - | Name id -> Id.hash id + | Anonymous -> 0 + | Name id -> Id.hash id + + let print = function + | Anonymous -> str "_" + | Name id -> Id.print id module Self_Hashcons = struct diff --git a/kernel/names.mli b/kernel/names.mli index 5b0163aa5..c73eb197b 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -105,6 +105,9 @@ sig val hcons : t -> t (** Hashconsing over names. *) + val print : t -> Pp.std_ppcmds + (** Pretty-printer (print "_" for [Anonymous]. *) + end (** {6 Type aliases} *) diff --git a/library/nameops.ml b/library/nameops.ml index 098f5112f..0b5dfd8d0 100644 --- a/library/nameops.ml +++ b/library/nameops.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp open Util open Names @@ -14,10 +13,6 @@ open Names let pr_id id = Id.print id -let pr_name = function - | Anonymous -> str "_" - | Name id -> pr_id id - (* Utilities *) let code_of_0 = Char.code '0' @@ -124,34 +119,82 @@ let atompart_of_id id = fst (repr_ident id) (* Names *) -let out_name = function - | Name id -> id - | Anonymous -> failwith "Nameops.out_name" +module type ExtName = +sig + + include module type of struct include Names.Name end + + exception IsAnonymous + + val fold_left : ('a -> Id.t -> 'a) -> 'a -> t -> 'a + val fold_right : (Id.t -> 'a -> 'a) -> t -> 'a -> 'a + val iter : (Id.t -> unit) -> t -> unit + val map : (Id.t -> Id.t) -> t -> t + val fold_map : ('a -> Id.t -> 'a * Id.t) -> 'a -> t -> 'a * t + val get_id : t -> Id.t + val pick : t -> t -> t + val cons : t -> Id.t list -> Id.t list + val to_option : Name.t -> Id.t option + +end + +module Name : ExtName = +struct + + include Names.Name + + exception IsAnonymous + + let fold_left f a = function + | Name id -> f a id + | Anonymous -> a + + let fold_right f na a = + match na with + | Name id -> f id a + | Anonymous -> a + + let iter f na = fold_right (fun x () -> f x) na () + + let map f = function + | Name id -> Name (f id) + | Anonymous -> Anonymous + + let fold_map f a = function + | Name id -> let (a, id) = f a id in (a, Name id) + | Anonymous -> a, Anonymous + + let get_id = function + | Name id -> id + | Anonymous -> raise IsAnonymous -let name_fold f na a = - match na with - | Name id -> f id a - | Anonymous -> a + let pick na1 na2 = + match na1 with + | Name _ -> na1 + | Anonymous -> na2 -let name_iter f na = name_fold (fun x () -> f x) na () + let cons na l = + match na with + | Anonymous -> l + | Name id -> id::l -let name_cons na l = - match na with - | Anonymous -> l - | Name id -> id::l + let to_option = function + | Anonymous -> None + | Name id -> Some id -let name_app f = function - | Name id -> Name (f id) - | Anonymous -> Anonymous +end -let name_fold_map f e = function - | Name id -> let (e,id) = f e id in (e,Name id) - | Anonymous -> e,Anonymous +open Name -let name_max na1 na2 = - match na1 with - | Name _ -> na1 - | Anonymous -> na2 +(* Compatibility *) +let out_name = get_id +let name_fold = fold_right +let name_iter = iter +let name_app = map +let name_fold_map = fold_map +let name_cons = cons +let name_max = pick +let pr_name = print let pr_lab l = Label.print l diff --git a/library/nameops.mli b/library/nameops.mli index 3a67b61a1..abfc09db8 100644 --- a/library/nameops.mli +++ b/library/nameops.mli @@ -9,8 +9,6 @@ open Names (** Identifiers and names *) -val pr_id : Id.t -> Pp.std_ppcmds -val pr_name : Name.t -> Pp.std_ppcmds val make_ident : string -> int option -> Id.t val repr_ident : Id.t -> string * int option @@ -50,16 +48,69 @@ val increment_subscript : Id.t -> Id.t val forget_subscript : Id.t -> Id.t +module Name : sig + + include module type of struct include Names.Name end + + exception IsAnonymous + + val fold_left : ('a -> Id.t -> 'a) -> 'a -> Name.t -> 'a + (** [fold_left f na a] is [f id a] if [na] is [Name id], and [a] otherwise. *) + + val fold_right : (Id.t -> 'a -> 'a) -> Name.t -> 'a -> 'a + (** [fold_right f a na] is [f a id] if [na] is [Name id], and [a] otherwise. *) + + val iter : (Id.t -> unit) -> Name.t -> unit + (** [iter f na] does [f id] if [na] equals [Name id], nothing otherwise. *) + + val map : (Id.t -> Id.t) -> Name.t -> t + (** [map f na] is [Anonymous] if [na] is [Anonymous] and [Name (f id)] if [na] is [Name id]. *) + + val fold_map : ('a -> Id.t -> 'a * Id.t) -> 'a -> Name.t -> 'a * Name.t + (** [fold_map f na a] is [a',Name id'] when [na] is [Name id] and [f a id] is [(a',id')]. + It is [a,Anonymous] otherwise. *) + + val get_id : Name.t -> Id.t + (** [get_id] associates [id] to [Name id]. @raise IsAnonymous otherwise. *) + + val pick : Name.t -> Name.t -> Name.t + (** [pick na na'] returns [Anonymous] if both names are [Anonymous]. + Pick one of [na] or [na'] otherwise. *) + + val cons : Name.t -> Id.t list -> Id.t list + (** [cons na l] returns [id::l] if [na] is [Name id] and [l] otherwise. *) + + val to_option : Name.t -> Id.t option + (** [to_option Anonymous] is [None] and [to_option (Name id)] is [Some id] *) + +end + val out_name : Name.t -> Id.t -(** [out_name] associates [id] to [Name id]. Raises [Failure "Nameops.out_name"] - otherwise. *) +(** @deprecated Same as [Name.get_id] *) val name_fold : (Id.t -> 'a -> 'a) -> Name.t -> 'a -> 'a +(** @deprecated Same as [Name.fold_right] *) + val name_iter : (Id.t -> unit) -> Name.t -> unit -val name_cons : Name.t -> Id.t list -> Id.t list +(** @deprecated Same as [Name.iter] *) + val name_app : (Id.t -> Id.t) -> Name.t -> Name.t +(** @deprecated Same as [Name.map] *) + val name_fold_map : ('a -> Id.t -> 'a * Id.t) -> 'a -> Name.t -> 'a * Name.t +(** @deprecated Same as [Name.fold_map] *) + val name_max : Name.t -> Name.t -> Name.t +(** @deprecated Same as [Name.pick] *) + +val name_cons : Name.t -> Id.t list -> Id.t list +(** @deprecated Same as [Name.cons] *) + +val pr_name : Name.t -> Pp.std_ppcmds +(** @deprecated Same as [Name.print] *) + +val pr_id : Id.t -> Pp.std_ppcmds +(** @deprecated Same as [Names.Id.print] *) val pr_lab : Label.t -> Pp.std_ppcmds diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index b3017f359..43c06a54d 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -231,9 +231,9 @@ let make_prb gls depth additionnal_terms = let build_projection intype (cstr:pconstructor) special default gls= let open Tacmach.New in let ci= (snd(fst cstr)) in - let body=Equality.build_selector (pf_env gls) (project gls) ci (mkRel 1) intype special default in + let sigma, body=Equality.build_selector (pf_env gls) (project gls) ci (mkRel 1) intype special default in let id=pf_get_new_id (Id.of_string "t") gls in - mkLambda(Name id,intype,body) + sigma, mkLambda(Name id,intype,body) (* generate an adhoc tactic following the proof tree *) @@ -346,12 +346,13 @@ let rec proof_tac p : unit Proofview.tactic = let special=mkRel (1+nargs-argind) in refresh_universes (type_of ti) (fun intype -> refresh_universes (type_of default) (fun outtype -> - let proj = + let sigma, proj = build_projection intype cstr special default gl in let injt= app_global_with_holes _f_equal [|intype;outtype;proj;ti;tj|] 1 in - Tacticals.New.tclTHEN injt (proof_tac prf))) + Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma) + (Tacticals.New.tclTHEN injt (proof_tac prf)))) with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e end } diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 434fb14a6..0041797de 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -944,7 +944,7 @@ let generalize_non_dep hyp g = ((* observe_tac "thin" *) (thin to_revert)) g -let id_of_decl = RelDecl.get_name %> Nameops.out_name +let id_of_decl = RelDecl.get_name %> Nameops.Name.get_id let var_of_decl = id_of_decl %> mkVar let revert idl = tclTHEN @@ -1127,11 +1127,11 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam ) in observe (str "full_params := " ++ - prlist_with_sep spc (RelDecl.get_name %> Nameops.out_name %> Ppconstr.pr_id) + prlist_with_sep spc (RelDecl.get_name %> Nameops.Name.get_id %> Ppconstr.pr_id) full_params ); observe (str "princ_params := " ++ - prlist_with_sep spc (RelDecl.get_name %> Nameops.out_name %> Ppconstr.pr_id) + prlist_with_sep spc (RelDecl.get_name %> Nameops.Name.get_id %> Ppconstr.pr_id) princ_params ); observe (str "fbody_with_full_params := " ++ @@ -1158,7 +1158,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam (fun i types -> let types = prod_applist (project g) types (List.rev_map var_of_decl princ_params) in { idx = idxs.(i) - fix_offset; - name = Nameops.out_name (fresh_id names.(i)); + name = Nameops.Name.get_id (fresh_id names.(i)); types = types; offset = fix_offset; nb_realargs = @@ -1181,7 +1181,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam let first_args = Array.init nargs (fun i -> mkRel (nargs -i)) in let app_f = mkApp(f,first_args) in let pte_args = (Array.to_list first_args)@[app_f] in - let app_pte = applist(mkVar (Nameops.out_name pte),pte_args) in + let app_pte = applist(mkVar (Nameops.Name.get_id pte),pte_args) in let body_with_param,num = let body = get_body fnames.(i) in let body_with_full_params = @@ -1208,9 +1208,9 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam num_in_block = num } in -(* observe (str "binding " ++ Ppconstr.pr_id (Nameops.out_name pte) ++ *) +(* observe (str "binding " ++ Ppconstr.pr_id (Nameops.Name.get_id pte) ++ *) (* str " to " ++ Ppconstr.pr_id info.name); *) - (Id.Map.add (Nameops.out_name pte) info acc_map,info::acc_info) + (Id.Map.add (Nameops.Name.get_id pte) info acc_map,info::acc_info) ) 0 (Id.Map.empty,[]) @@ -1284,7 +1284,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam (do_replace evd full_params (fix_info.idx + List.length princ_params) - (args_id@(List.map (RelDecl.get_name %> Nameops.out_name) princ_params)) + (args_id@(List.map (RelDecl.get_name %> Nameops.Name.get_id) princ_params)) (all_funs.(fix_info.num_in_block)) fix_info.num_in_block all_funs @@ -1563,17 +1563,17 @@ let prove_principle_for_gen | _ -> assert false in (* observe (str "rec_arg_id := " ++ pr_lconstr (mkVar rec_arg_id)); *) - let subst_constrs = List.map (get_name %> Nameops.out_name %> mkVar) (pre_rec_arg@princ_info.params) in + let subst_constrs = List.map (get_name %> Nameops.Name.get_id %> mkVar) (pre_rec_arg@princ_info.params) in let relation = substl subst_constrs relation in let input_type = substl subst_constrs rec_arg_type in - let wf_thm_id = Nameops.out_name (fresh_id (Name (Id.of_string "wf_R"))) in + let wf_thm_id = Nameops.Name.get_id (fresh_id (Name (Id.of_string "wf_R"))) in let acc_rec_arg_id = - Nameops.out_name (fresh_id (Name (Id.of_string ("Acc_"^(Id.to_string rec_arg_id))))) + Nameops.Name.get_id (fresh_id (Name (Id.of_string ("Acc_"^(Id.to_string rec_arg_id))))) in let revert l = tclTHEN (Proofview.V82.of_tactic (Tactics.generalize (List.map mkVar l))) (Proofview.V82.of_tactic (clear l)) in - let fix_id = Nameops.out_name (fresh_id (Name hrec_id)) in + let fix_id = Nameops.Name.get_id (fresh_id (Name hrec_id)) in let prove_rec_arg_acc g = ((* observe_tac "prove_rec_arg_acc" *) (tclCOMPLETE @@ -1591,7 +1591,7 @@ let prove_principle_for_gen ) g in - let args_ids = List.map (get_name %> Nameops.out_name) princ_info.args in + let args_ids = List.map (get_name %> Nameops.Name.get_id) princ_info.args in let lemma = match !tcc_lemma_ref with | Undefined -> user_err Pp.(str "No tcc proof !!") @@ -1639,7 +1639,7 @@ let prove_principle_for_gen [ observe_tac "start_tac" start_tac; h_intros - (List.rev_map (get_name %> Nameops.out_name) + (List.rev_map (get_name %> Nameops.Name.get_id) (princ_info.args@princ_info.branches@princ_info.predicates@princ_info.params) ); (* observe_tac "" *) Proofview.V82.of_tactic (assert_by @@ -1677,14 +1677,14 @@ let prove_principle_for_gen in let acc_inv = lazy (mkApp(Lazy.force acc_inv, [|mkVar acc_rec_arg_id|])) in let predicates_names = - List.map (get_name %> Nameops.out_name) princ_info.predicates + List.map (get_name %> Nameops.Name.get_id) princ_info.predicates in let pte_info = { proving_tac = (fun eqs -> (* msgnl (str "tcc_list := "++ prlist_with_sep spc Ppconstr.pr_id !tcc_list); *) -(* msgnl (str "princ_info.args := "++ prlist_with_sep spc Ppconstr.pr_id (List.map (fun (na,_,_) -> (Nameops.out_name na)) princ_info.args)); *) -(* msgnl (str "princ_info.params := "++ prlist_with_sep spc Ppconstr.pr_id (List.map (fun (na,_,_) -> (Nameops.out_name na)) princ_info.params)); *) +(* msgnl (str "princ_info.args := "++ prlist_with_sep spc Ppconstr.pr_id (List.map (fun (na,_,_) -> (Nameops.Name.get_id na)) princ_info.args)); *) +(* msgnl (str "princ_info.params := "++ prlist_with_sep spc Ppconstr.pr_id (List.map (fun (na,_,_) -> (Nameops.Name.get_id na)) princ_info.params)); *) (* msgnl (str "acc_rec_arg_id := "++ Ppconstr.pr_id acc_rec_arg_id); *) (* msgnl (str "eqs := "++ prlist_with_sep spc Ppconstr.pr_id eqs); *) @@ -1693,7 +1693,7 @@ let prove_principle_for_gen is_mes acc_inv fix_id (!tcc_list@(List.map - (get_name %> Nameops.out_name) + (get_name %> Nameops.Name.get_id) (princ_info.args@princ_info.params) )@ ([acc_rec_arg_id])) eqs ) @@ -1722,7 +1722,7 @@ let prove_principle_for_gen (* observe_tac "instanciate_hyps_with_args" *) (instanciate_hyps_with_args make_proof - (List.map (get_name %> Nameops.out_name) princ_info.branches) + (List.map (get_name %> Nameops.Name.get_id) princ_info.branches) (List.rev args_ids) ) gl' diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 18d63dd94..942527167 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -62,7 +62,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = then List.tl args else args in - Context.Named.Declaration.LocalAssum (Nameops.out_name (Context.Rel.Declaration.get_name decl), + Context.Named.Declaration.LocalAssum (Nameops.Name.get_id (Context.Rel.Declaration.get_name decl), Term.compose_prod real_args (mkSort new_sort)) in let new_predicates = @@ -185,11 +185,11 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = with | Toberemoved -> -(* observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *) +(* observe (str "Decl of "++Ppconstr.Name.print x ++ str " is removed "); *) let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [dummy_var] 1 b) in new_b, List.map pop binders_to_remove_from_b | Toberemoved_with_rel (n,c) -> -(* observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *) +(* observe (str "Decl of "++Ppconstr.Name.print x ++ str " is removed "); *) let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [c] n b) in new_b, list_add_set_eq eq_constr (mkRel n) (List.map pop binders_to_remove_from_b) end @@ -214,11 +214,11 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = with | Toberemoved -> -(* observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *) +(* observe (str "Decl of "++Ppconstr.Name.print x ++ str " is removed "); *) let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [dummy_var] 1 b) in new_b, List.map pop binders_to_remove_from_b | Toberemoved_with_rel (n,c) -> -(* observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *) +(* observe (str "Decl of "++Ppconstr.Name.print x ++ str " is removed "); *) let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [c] n b) in new_b, list_add_set_eq eq_constr (mkRel n) (List.map pop binders_to_remove_from_b) end diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 74c0eb4cc..4946285e1 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -200,13 +200,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 ) @@ -885,7 +885,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 ) diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index d68bdc215..12232dd83 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -421,7 +421,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes let params_bindings,avoid = List.fold_left2 (fun (bindings,avoid) decl p -> - let id = Namegen.next_ident_away (Nameops.out_name (RelDecl.get_name decl)) avoid in + let id = Namegen.next_ident_away (Nameops.Name.get_id (RelDecl.get_name decl)) avoid in p::bindings,id::avoid ) ([],pf_ids_of_hyps g) @@ -431,7 +431,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes let lemmas_bindings = List.rev (fst (List.fold_left2 (fun (bindings,avoid) decl p -> - let id = Namegen.next_ident_away (Nameops.out_name (RelDecl.get_name decl)) avoid in + let id = Namegen.next_ident_away (Nameops.Name.get_id (RelDecl.get_name decl)) avoid in (nf_zeta p)::bindings,id::avoid) ([],avoid) princ_infos.predicates diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index b2c8489ce..763443717 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -133,20 +133,6 @@ let prNamedRLDecl s lc = prstr "\n"; end -let showind (id:Id.t) = - let cstrid = Constrintern.global_reference id in - let (ind1, u),cstrlist = Inductiveops.find_inductive (Global.env()) Evd.empty (EConstr.of_constr cstrid) in - let mib1,ib1 = Inductive.lookup_mind_specif (Global.env()) ind1 in - let u = EConstr.Unsafe.to_instance u in - List.iter (fun decl -> - print_string (string_of_name (Context.Rel.Declaration.get_name decl) ^ ":"); - prconstr (RelDecl.get_type decl); print_string "\n") - ib1.mind_arity_ctxt; - Printf.printf "arity :"; prconstr (Inductiveops.type_of_inductive (Global.env ()) (ind1, u)); - Array.iteri - (fun i x -> Printf.printf"type constr %d :" i ; prconstr x) - ib1.mind_user_lc - (** {2 Misc} *) exception Found of int diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 2f9f70876..62eba9513 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -879,7 +879,7 @@ let rec make_rewrite_list expr_info max = function let k_na,_,t = destProd sigma t_eq in let _,_,t = destProd sigma t in let def_na,_,_ = destProd sigma t in - Nameops.out_name k_na,Nameops.out_name def_na + Nameops.Name.get_id k_na,Nameops.Name.get_id def_na in Proofview.V82.of_tactic (general_rewrite_bindings false Locus.AllOccurrences true (* dep proofs also: *) true @@ -905,7 +905,7 @@ let make_rewrite expr_info l hp max = let k_na,_,t = destProd sigma t_eq in let _,_,t = destProd sigma t in let def_na,_,_ = destProd sigma t in - Nameops.out_name k_na,Nameops.out_name def_na + Nameops.Name.get_id k_na,Nameops.Name.get_id def_na in observe_tac (str "general_rewrite_bindings") (Proofview.V82.of_tactic (general_rewrite_bindings false Locus.AllOccurrences diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index cba9c1364..9726a5b40 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -306,7 +306,8 @@ let project_hint pri l2r r = | _ -> assert false in let p = if l2r then build_coq_iff_left_proj () else build_coq_iff_right_proj () in - let p = EConstr.of_constr @@ Universes.constr_of_global p in + let sigma, p = Evd.fresh_global env sigma p in + let p = EConstr.of_constr p in let c = Reductionops.whd_beta sigma (mkApp (c, Context.Rel.to_extended_vect mkRel 0 sign)) in let c = it_mkLambda_or_LetIn (mkApp (p,[|mkArrow a (lift 1 b);mkArrow b (lift 1 a);c|])) sign in @@ -735,7 +736,6 @@ let rewrite_except h = let refl_equal = let coq_base_constant s = - Universes.constr_of_global @@ Coqlib.gen_reference_in_modules "RecursiveDefinition" (Coqlib.init_modules @ [["Coq";"Arith";"Le"];["Coq";"Arith";"Lt"]]) s in function () -> (coq_base_constant "eq_refl") @@ -747,8 +747,9 @@ let refl_equal = let mkCaseEq a : unit Proofview.tactic = Proofview.Goal.enter { enter = begin fun gl -> let type_of_a = Tacmach.New.pf_unsafe_type_of gl a in - Tacticals.New.tclTHENLIST - [Tactics.generalize [(mkApp(EConstr.of_constr (delayed_force refl_equal), [| type_of_a; a|]))]; + Tacticals.New.pf_constr_of_global (delayed_force refl_equal) >>= fun req -> + Tacticals.New.tclTHENLIST + [Tactics.generalize [(mkApp(req, [| type_of_a; a|]))]; Proofview.Goal.enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 4e254ea76..580c21d40 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -571,7 +571,7 @@ type 'a extra_genarg_printer = str "=>" ++ brk (1,4) ++ pr t)) | All t -> str "_" ++ spc () ++ str "=>" ++ brk (1,4) ++ pr t - let pr_funvar n = spc () ++ pr_name n + let pr_funvar n = spc () ++ Name.print n let pr_let_clause k pr (id,(bl,t)) = hov 0 (keyword k ++ spc () ++ pr_lident id ++ prlist pr_funvar bl ++ diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 966b11d0e..dadcfb9f2 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -751,17 +751,23 @@ let default_flags = { under_lambdas = true; on_morphisms = true; } let get_opt_rew_rel = function RewPrf (rel, prf) -> Some rel | _ -> None -let make_eq () = -(*FIXME*) EConstr.of_constr (Universes.constr_of_global (Coqlib.build_coq_eq ())) -let make_eq_refl () = -(*FIXME*) EConstr.of_constr (Universes.constr_of_global (Coqlib.build_coq_eq_refl ())) +let new_global (evars, cstrs) gr = + let Sigma (c, sigma, _) = Evarutil.new_global (Sigma.Unsafe.of_evar_map evars) gr + in (Sigma.to_evar_map sigma, cstrs), c -let get_rew_prf r = match r.rew_prf with - | RewPrf (rel, prf) -> rel, prf +let make_eq sigma = + new_global sigma (Coqlib.build_coq_eq ()) +let make_eq_refl sigma = + new_global sigma (Coqlib.build_coq_eq_refl ()) + +let get_rew_prf evars r = match r.rew_prf with + | RewPrf (rel, prf) -> evars, (rel, prf) | RewCast c -> - let rel = mkApp (make_eq (), [| r.rew_car |]) in - rel, mkCast (mkApp (make_eq_refl (), [| r.rew_car; r.rew_from |]), - c, mkApp (rel, [| r.rew_from; r.rew_to |])) + let evars, eq = make_eq evars in + let evars, eq_refl = make_eq_refl evars in + let rel = mkApp (eq, [| r.rew_car |]) in + evars, (rel, mkCast (mkApp (eq_refl, [| r.rew_car; r.rew_from |]), + c, mkApp (rel, [| r.rew_from; r.rew_to |]))) let poly_subrelation sort = if sort then PropGlobal.subrelation else TypeGlobal.subrelation @@ -827,7 +833,8 @@ let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' (b,cstr) ev env evars carrier relation x in [ proof ; x ; x ] @ acc, subst, evars, sigargs, x :: typeargs' | Some r -> - [ snd (get_rew_prf r); r.rew_to; x ] @ acc, subst, evars, + let evars, proof = get_rew_prf evars r in + [ snd proof; r.rew_to; x ] @ acc, subst, evars, sigargs, r.rew_to :: typeargs') | None -> if not (Option.is_empty y) then @@ -847,7 +854,8 @@ let apply_constraint env avoid car rel prf cstr res = | Some r -> resolve_subrelation env avoid car rel (fst cstr) prf r res let coerce env avoid cstr res = - let rel, prf = get_rew_prf res in + let evars, (rel, prf) = get_rew_prf res.rew_evars res in + let res = { res with rew_evars = evars } in apply_constraint env avoid res.rew_car rel prf cstr res let apply_rule unify loccs : int pure_strategy = @@ -868,8 +876,7 @@ let apply_rule unify loccs : int pure_strategy = else if Termops.eq_constr (fst rew.rew_evars) t rew.rew_to then (occ, Identity) else let res = { rew with rew_car = ty } in - let rel, prf = get_rew_prf res in - let res = Success (apply_constraint env unfresh rew.rew_car rel prf cstr res) in + let res = Success (coerce env unfresh cstr res) in (occ, res) } @@ -1231,9 +1238,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = in let res = match res with - | Success r -> - let rel, prf = get_rew_prf r in - Success (apply_constraint env unfresh r.rew_car rel prf (prop,cstr) r) + | Success r -> Success (coerce env unfresh (prop,cstr) r) | Fail | Identity -> res in state, res | _ -> state, Fail diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index 75f89a81e..f44ccbd3b 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -502,7 +502,7 @@ let print_ltacs () = | Tacexpr.TacFun (l, t) -> (l, t) | _ -> ([], body) in - let pr_ltac_fun_arg n = spc () ++ pr_name n in + let pr_ltac_fun_arg n = spc () ++ Name.print n in hov 2 (pr_qualid qid ++ prlist pr_ltac_fun_arg l) in Feedback.msg_notice (prlist_with_sep fnl pr_entry entries) diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 2dc3bb378..0096abfa6 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -718,7 +718,7 @@ let split_ltac_fun = function | TacFun (l,t) -> (l,t) | t -> ([],t) -let pr_ltac_fun_arg n = spc () ++ pr_name n +let pr_ltac_fun_arg n = spc () ++ Name.print n let print_ltac id = try diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 6b0914ff9..594c4fa15 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -1113,11 +1113,11 @@ let cons_and_check_name id l = let rec read_match_goal_hyps lfun ist env sigma lidh = function | (Hyp ((loc,na) as locna,mp))::tl -> - let lidh' = name_fold cons_and_check_name na lidh in + let lidh' = Name.fold_right cons_and_check_name na lidh in Hyp (locna,read_pattern lfun ist env sigma mp):: (read_match_goal_hyps lfun ist env sigma lidh' tl) | (Def ((loc,na) as locna,mv,mp))::tl -> - let lidh' = name_fold cons_and_check_name na lidh in + let lidh' = Name.fold_right cons_and_check_name na lidh in Def (locna,read_pattern lfun ist env sigma mv, read_pattern lfun ist env sigma mp):: (read_match_goal_hyps lfun ist env sigma lidh' tl) | [] -> [] @@ -1420,7 +1420,7 @@ and tactic_of_value ist vle = (str "A fully applied tactic is expected:" ++ spc() ++ Pp.str "missing " ++ Pp.str (String.plural numargs "argument") ++ Pp.str " for " ++ Pp.str (String.plural numargs "variable") ++ Pp.str " " ++ - pr_enum pr_name vars ++ Pp.str ".") + pr_enum Name.print vars ++ Pp.str ".") | VRec _ -> Tacticals.New.tclZEROMSG (str "A fully applied tactic is expected.") else if has_type vle (topwit wit_tactic) then let tac = out_gen (topwit wit_tactic) vle in diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml index f5e6f05ce..2858df313 100644 --- a/plugins/ltac/tacsubst.ml +++ b/plugins/ltac/tacsubst.ml @@ -14,7 +14,6 @@ open Stdarg open Tacarg open Misctypes open Globnames -open Term open Genredexpr open Patternops @@ -91,7 +90,7 @@ open Printer let subst_global_reference subst = let subst_global ref = let ref',t' = subst_global subst ref in - if not (eq_constr (Universes.constr_of_global ref') t') then + if not (is_global ref' t') then Feedback.msg_warning (strbrk "The reference " ++ pr_global ref ++ str " is not " ++ str " expanded to \"" ++ pr_lconstr t' ++ str "\", but to " ++ pr_global ref') ; diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml index 4ec111e01..d8e21d81d 100644 --- a/plugins/ltac/tauto.ml +++ b/plugins/ltac/tauto.ml @@ -220,9 +220,7 @@ let apply_nnpp _ ist = Proofview.tclBIND (Proofview.tclUNIT ()) begin fun () -> try - let nnpp = Universes.constr_of_global (Nametab.global_of_path coq_nnpp_path) in - let nnpp = EConstr.of_constr nnpp in - apply nnpp + Tacticals.New.pf_constr_of_global (Nametab.global_of_path coq_nnpp_path) >>= apply with Not_found -> tclFAIL 0 (Pp.mt ()) end diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index ee748567b..d7408e88e 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -39,10 +39,10 @@ open OmegaSolver let elim_id id = Proofview.Goal.enter { enter = begin fun gl -> - simplest_elim (Tacmach.New.pf_global id gl) + simplest_elim (mkVar id) end } let resolve_id id = Proofview.Goal.enter { enter = begin fun gl -> - apply (Tacmach.New.pf_global id gl) + apply (mkVar id) end } let timing timer_name f arg = f arg diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index 7412de1e8..ba8356b52 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -456,39 +456,56 @@ let quote_terms env sigma ivs lc = term. Ring for example needs that, but Ring doesn't use Quote yet. *) +let pf_constrs_of_globals l = + let rec aux l acc = + match l with + [] -> Proofview.tclUNIT (List.rev acc) + | hd :: tl -> + Tacticals.New.pf_constr_of_global hd >>= fun g -> aux tl (g :: acc) + in aux l [] + let quote f lid = - Proofview.Goal.nf_enter { enter = begin fun gl -> - let env = Proofview.Goal.env gl in - let sigma = Tacmach.New.project gl in - let f = Tacmach.New.pf_global f gl in - let cl = List.map (fun id -> EConstr.to_constr sigma (Tacmach.New.pf_global id gl)) lid in - let ivs = compute_ivs f cl gl in - let concl = Proofview.Goal.concl gl in - let quoted_terms = quote_terms env sigma ivs [concl] in - let (p, vm) = match quoted_terms with + Proofview.Goal.enter { enter = begin fun gl -> + let fg = Tacmach.New.pf_global f gl in + let clg = List.map (fun id -> Tacmach.New.pf_global id gl) lid in + Tacticals.New.pf_constr_of_global fg >>= fun f -> + pf_constrs_of_globals clg >>= fun cl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Tacmach.New.project gl in + let ivs = compute_ivs f (List.map (EConstr.to_constr sigma) cl) gl in + let concl = Proofview.Goal.concl gl in + let quoted_terms = quote_terms env sigma ivs [concl] in + let (p, vm) = match quoted_terms with | [p], vm -> (p,vm) | _ -> assert false - in - match ivs.variable_lhs with - | None -> Tactics.convert_concl (mkApp (f, [| p |])) DEFAULTcast - | Some _ -> Tactics.convert_concl (mkApp (f, [| vm; p |])) DEFAULTcast + in + match ivs.variable_lhs with + | None -> Tactics.convert_concl (mkApp (f, [| p |])) DEFAULTcast + | Some _ -> Tactics.convert_concl (mkApp (f, [| vm; p |])) DEFAULTcast + end } end } let gen_quote cont c f lid = - Proofview.Goal.nf_enter { enter = begin fun gl -> - let env = Proofview.Goal.env gl in - let sigma = Tacmach.New.project gl in - let f = Tacmach.New.pf_global f gl in - let cl = List.map (fun id -> EConstr.to_constr sigma (Tacmach.New.pf_global id gl)) lid in - let ivs = compute_ivs f cl gl in - let quoted_terms = quote_terms env sigma ivs [c] in - let (p, vm) = match quoted_terms with - | [p], vm -> (p,vm) - | _ -> assert false - in - match ivs.variable_lhs with - | None -> cont (mkApp (f, [| p |])) - | Some _ -> cont (mkApp (f, [| vm; p |])) + Proofview.Goal.enter { enter = begin fun gl -> + let fg = Tacmach.New.pf_global f gl in + let clg = List.map (fun id -> Tacmach.New.pf_global id gl) lid in + Tacticals.New.pf_constr_of_global fg >>= fun f -> + pf_constrs_of_globals clg >>= fun cl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Tacmach.New.project gl in + let cl = List.map (EConstr.to_constr sigma) cl in + let ivs = compute_ivs f cl gl in + let quoted_terms = quote_terms env sigma ivs [c] in + let (p, vm) = match quoted_terms with + | [p], vm -> (p,vm) + | _ -> assert false + in + match ivs.variable_lhs with + | None -> cont (mkApp (f, [| p |])) + | Some _ -> cont (mkApp (f, [| vm; p |])) + end } end } (*i diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 426157372..80680e408 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -731,7 +731,7 @@ let get_names env sigma sign eqns = (fun (LocalAssum (na,t) | LocalDef (na,_,t)) -> Name (next_name_away (named_hd env sigma t na) avoid)) d na in - (na::l,(out_name na)::avoid)) + (na::l,(Name.get_id na)::avoid)) ([],allvars) (List.rev sign) names2 in names3,aliasname @@ -2223,14 +2223,14 @@ let build_ineqs evdref prevpatterns pats liftsign = (Some ([], 0, 0, [])) eqnpats pats in match acc with None -> c - | Some (sign, len, _, c') -> - let conj = it_mkProd_or_LetIn (mk_coq_not (mk_coq_and c')) - (lift_rel_context liftsign sign) - in - conj :: c) + | Some (sign, len, _, c') -> + let sigma, conj = mk_coq_and !evdref c' in + let sigma, neg = mk_coq_not sigma conj in + let conj = it_mkProd_or_LetIn neg (lift_rel_context liftsign sign) in + evdref := sigma; conj :: c) [] prevpatterns in match diffs with [] -> None - | _ -> Some (mk_coq_and diffs) + | _ -> Some (let sigma, conj = mk_coq_and !evdref diffs in evdref := sigma; conj) let constrs_of_pats typing_fun env evdref eqns tomatchs sign neqs arity = let i = ref 0 in diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 752819aa3..6f099c8df 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -907,8 +907,7 @@ let simple_cases_matrix_of_branches ind brs = let nal,c = it_destRLambda_or_LetIn_names n b in let mkPatVar na = CAst.make @@ PatVar na in let p = CAst.make @@ PatCstr ((ind,i+1),List.map mkPatVar nal,Anonymous) in - let map name = try Some (Nameops.out_name name) with Failure _ -> None in - let ids = List.map_filter map nal in + let ids = List.map_filter Nameops.Name.to_option nal in Loc.tag @@ (ids,[p],c)) brs diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index bf62cea6b..630f80ad2 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -638,7 +638,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty (fun i -> let b = nf_evar i b1 in let t = nf_evar i t1 in - let na = Nameops.name_max na1 na2 in + let na = Nameops.Name.pick na1 na2 in evar_conv_x ts (push_rel (RelDecl.LocalDef (na,b,t)) env) i pbty c'1 c'2); (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)] and f2 i = @@ -755,7 +755,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty [(fun i -> evar_conv_x ts env i CONV c1 c2); (fun i -> let c = nf_evar i c1 in - let na = Nameops.name_max na1 na2 in + let na = Nameops.Name.pick na1 na2 in evar_conv_x ts (push_rel (RelDecl.LocalAssum (na,c)) env) i CONV c'1 c'2)] | Flexible ev1, Rigid -> flex_rigid true ev1 appr1 appr2 @@ -816,7 +816,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty [(fun i -> evar_conv_x ts env i CONV c1 c2); (fun i -> let c = nf_evar i c1 in - let na = Nameops.name_max n1 n2 in + let na = Nameops.Name.pick n1 n2 in evar_conv_x ts (push_rel (RelDecl.LocalAssum (na,c)) env) i pbty c'1 c'2)] | Rel x1, Rel x2 -> diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 923d7d938..6fb1b6089 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -33,109 +33,104 @@ let map_glob_decl_left_to_right f (na,k,obd,ty) = (na,k,comp1,comp2) let binding_kind_eq bk1 bk2 = match bk1, bk2 with -| Decl_kinds.Explicit, Decl_kinds.Explicit -> true -| Decl_kinds.Implicit, Decl_kinds.Implicit -> true -| _ -> false + | Decl_kinds.Explicit, Decl_kinds.Explicit -> true + | Decl_kinds.Implicit, Decl_kinds.Implicit -> true + | (Decl_kinds.Explicit | Decl_kinds.Implicit), _ -> false let case_style_eq s1 s2 = match s1, s2 with -| LetStyle, LetStyle -> true -| IfStyle, IfStyle -> true -| LetPatternStyle, LetPatternStyle -> true -| MatchStyle, MatchStyle -> true -| RegularStyle, RegularStyle -> true -| _ -> false + | LetStyle, LetStyle -> true + | IfStyle, IfStyle -> true + | LetPatternStyle, LetPatternStyle -> true + | MatchStyle, MatchStyle -> true + | RegularStyle, RegularStyle -> true + | (LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle), _ -> false let rec cases_pattern_eq { CAst.v = p1} { CAst.v = p2 } = match p1, p2 with -| PatVar na1, PatVar na2 -> Name.equal na1 na2 -| PatCstr (c1, pl1, na1), PatCstr (c2, pl2, na2) -> - eq_constructor c1 c2 && List.equal cases_pattern_eq pl1 pl2 && - Name.equal na1 na2 -| _ -> false + | PatVar na1, PatVar na2 -> Name.equal na1 na2 + | PatCstr (c1, pl1, na1), PatCstr (c2, pl2, na2) -> + eq_constructor c1 c2 && List.equal cases_pattern_eq pl1 pl2 && + Name.equal na1 na2 + | (PatVar _ | PatCstr _), _ -> false let cast_type_eq eq t1 t2 = match t1, t2 with -| CastConv t1, CastConv t2 -> eq t1 t2 -| CastVM t1, CastVM t2 -> eq t1 t2 -| CastCoerce, CastCoerce -> true -| CastNative t1, CastNative t2 -> eq t1 t2 -| _ -> false - -let rec glob_constr_eq { CAst.v = c1 } { CAst.v = c2 } = match c1, c2 with -| GRef (gr1, _), GRef (gr2, _) -> eq_gr gr1 gr2 -| GVar id1, GVar id2 -> Id.equal id1 id2 -| GEvar (id1, arg1), GEvar (id2, arg2) -> - Id.equal id1 id2 && - List.equal instance_eq arg1 arg2 -| GPatVar (b1, pat1), GPatVar (b2, pat2) -> - (b1 : bool) == b2 && Id.equal pat1 pat2 -| GApp (f1, arg1), GApp (f2, arg2) -> - glob_constr_eq f1 f2 && List.equal glob_constr_eq arg1 arg2 -| GLambda (na1, bk1, t1, c1), GLambda (na2, bk2, t2, c2) -> - Name.equal na1 na2 && binding_kind_eq bk1 bk2 && - glob_constr_eq t1 t2 && glob_constr_eq c1 c2 -| GProd (na1, bk1, t1, c1), GProd (na2, bk2, t2, c2) -> - Name.equal na1 na2 && binding_kind_eq bk1 bk2 && - glob_constr_eq t1 t2 && glob_constr_eq c1 c2 -| GLetIn (na1, b1, t1, c1), GLetIn (na2, b2, t2, c2) -> - Name.equal na1 na2 && glob_constr_eq b1 b2 && Option.equal glob_constr_eq t1 t2 && glob_constr_eq c1 c2 -| GCases (st1, c1, tp1, cl1), GCases (st2, c2, tp2, cl2) -> - case_style_eq st1 st2 && Option.equal glob_constr_eq c1 c2 && - List.equal tomatch_tuple_eq tp1 tp2 && - List.equal cases_clause_eq cl1 cl2 -| GLetTuple (na1, (n1, p1), c1, t1), GLetTuple (na2, (n2, p2), c2, t2) -> - List.equal Name.equal na1 na2 && Name.equal n1 n2 && - Option.equal glob_constr_eq p1 p2 && glob_constr_eq c1 c2 && - glob_constr_eq t1 t2 -| GIf (m1, (pat1, p1), c1, t1), GIf (m2, (pat2, p2), c2, t2) -> - glob_constr_eq m1 m2 && Name.equal pat1 pat2 && - Option.equal glob_constr_eq p1 p2 && glob_constr_eq c1 c2 && - glob_constr_eq t1 t2 -| GRec (kn1, id1, decl1, c1, t1), GRec (kn2, id2, decl2, c2, t2) -> - fix_kind_eq kn1 kn2 && Array.equal Id.equal id1 id2 && - Array.equal (fun l1 l2 -> List.equal glob_decl_eq l1 l2) decl1 decl2 && - Array.equal glob_constr_eq c1 c2 && - Array.equal glob_constr_eq t1 t2 -| GSort s1, GSort s2 -> Miscops.glob_sort_eq s1 s2 -| GHole (kn1, nam1, gn1), GHole (kn2, nam2, gn2) -> - Option.equal (==) gn1 gn2 (** Only thing sensible *) && - Miscops.intro_pattern_naming_eq nam1 nam2 -| GCast (c1, t1), GCast (c2, t2) -> - glob_constr_eq c1 c2 && cast_type_eq glob_constr_eq t1 t2 -| _ -> false - -and tomatch_tuple_eq (c1, p1) (c2, p2) = + | CastConv t1, CastConv t2 -> eq t1 t2 + | CastVM t1, CastVM t2 -> eq t1 t2 + | CastCoerce, CastCoerce -> true + | CastNative t1, CastNative t2 -> eq t1 t2 + | (CastConv _ | CastVM _ | CastCoerce | CastNative _), _ -> false + +let tomatch_tuple_eq f (c1, p1) (c2, p2) = let eqp (_, (i1, na1)) (_, (i2, na2)) = eq_ind i1 i2 && List.equal Name.equal na1 na2 in let eq_pred (n1, o1) (n2, o2) = Name.equal n1 n2 && Option.equal eqp o1 o2 in - glob_constr_eq c1 c2 && eq_pred p1 p2 + f c1 c2 && eq_pred p1 p2 -and cases_clause_eq (_, (id1, p1, c1)) (_, (id2, p2, c2)) = - List.equal Id.equal id1 id2 && List.equal cases_pattern_eq p1 p2 && - glob_constr_eq c1 c2 +and cases_clause_eq f (_, (id1, p1, c1)) (_, (id2, p2, c2)) = + List.equal Id.equal id1 id2 && List.equal cases_pattern_eq p1 p2 && f c1 c2 -and glob_decl_eq (na1, bk1, c1, t1) (na2, bk2, c2, t2) = +let glob_decl_eq f (na1, bk1, c1, t1) (na2, bk2, c2, t2) = Name.equal na1 na2 && binding_kind_eq bk1 bk2 && - Option.equal glob_constr_eq c1 c2 && - glob_constr_eq t1 t2 - -and fix_kind_eq k1 k2 = match k1, k2 with -| GFix (a1, i1), GFix (a2, i2) -> - let eq (i1, o1) (i2, o2) = - Option.equal Int.equal i1 i2 && fix_recursion_order_eq o1 o2 - in - Int.equal i1 i2 && Array.equal eq a1 a1 -| GCoFix i1, GCoFix i2 -> Int.equal i1 i2 -| _ -> false - -and fix_recursion_order_eq o1 o2 = match o1, o2 with -| GStructRec, GStructRec -> true -| GWfRec c1, GWfRec c2 -> glob_constr_eq c1 c2 -| GMeasureRec (c1, o1), GMeasureRec (c2, o2) -> - glob_constr_eq c1 c2 && Option.equal glob_constr_eq o1 o2 -| _ -> false - -and instance_eq (x1,c1) (x2,c2) = - Id.equal x1 x2 && glob_constr_eq c1 c2 + Option.equal f c1 c2 && f t1 t2 + +let fix_recursion_order_eq f o1 o2 = match o1, o2 with + | GStructRec, GStructRec -> true + | GWfRec c1, GWfRec c2 -> f c1 c2 + | GMeasureRec (c1, o1), GMeasureRec (c2, o2) -> + f c1 c2 && Option.equal f o1 o2 + | (GStructRec | GWfRec _ | GMeasureRec _), _ -> false + +let fix_kind_eq f k1 k2 = match k1, k2 with + | GFix (a1, i1), GFix (a2, i2) -> + let eq (i1, o1) (i2, o2) = + Option.equal Int.equal i1 i2 && fix_recursion_order_eq f o1 o2 + in + Int.equal i1 i2 && Array.equal eq a1 a1 + | GCoFix i1, GCoFix i2 -> Int.equal i1 i2 + | (GFix _ | GCoFix _), _ -> false + +let instance_eq f (x1,c1) (x2,c2) = + Id.equal x1 x2 && f c1 c2 + +let mk_glob_constr_eq f { CAst.v = c1 } { CAst.v = c2 } = match c1, c2 with + | GRef (gr1, _), GRef (gr2, _) -> eq_gr gr1 gr2 + | GVar id1, GVar id2 -> Id.equal id1 id2 + | GEvar (id1, arg1), GEvar (id2, arg2) -> + Id.equal id1 id2 && List.equal (instance_eq f) arg1 arg2 + | GPatVar (b1, pat1), GPatVar (b2, pat2) -> + (b1 : bool) == b2 && Id.equal pat1 pat2 + | GApp (f1, arg1), GApp (f2, arg2) -> + f f1 f2 && List.equal f arg1 arg2 + | GLambda (na1, bk1, t1, c1), GLambda (na2, bk2, t2, c2) -> + Name.equal na1 na2 && binding_kind_eq bk1 bk2 && f t1 t2 && f c1 c2 + | GProd (na1, bk1, t1, c1), GProd (na2, bk2, t2, c2) -> + Name.equal na1 na2 && binding_kind_eq bk1 bk2 && f t1 t2 && f c1 c2 + | GLetIn (na1, b1, t1, c1), GLetIn (na2, b2, t2, c2) -> + Name.equal na1 na2 && f b1 b2 && Option.equal f t1 t2 && f c1 c2 + | GCases (st1, c1, tp1, cl1), GCases (st2, c2, tp2, cl2) -> + case_style_eq st1 st2 && Option.equal f c1 c2 && + List.equal (tomatch_tuple_eq f) tp1 tp2 && + List.equal (cases_clause_eq f) cl1 cl2 + | GLetTuple (na1, (n1, p1), c1, t1), GLetTuple (na2, (n2, p2), c2, t2) -> + List.equal Name.equal na1 na2 && Name.equal n1 n2 && + Option.equal f p1 p2 && f c1 c2 && f t1 t2 + | GIf (m1, (pat1, p1), c1, t1), GIf (m2, (pat2, p2), c2, t2) -> + f m1 m2 && Name.equal pat1 pat2 && + Option.equal f p1 p2 && f c1 c2 && f t1 t2 + | GRec (kn1, id1, decl1, c1, t1), GRec (kn2, id2, decl2, c2, t2) -> + fix_kind_eq f kn1 kn2 && Array.equal Id.equal id1 id2 && + Array.equal (fun l1 l2 -> List.equal (glob_decl_eq f) l1 l2) decl1 decl2 && + Array.equal f c1 c2 && Array.equal f t1 t2 + | GSort s1, GSort s2 -> Miscops.glob_sort_eq s1 s2 + | GHole (kn1, nam1, gn1), GHole (kn2, nam2, gn2) -> + Option.equal (==) gn1 gn2 (** Only thing sensible *) && + Miscops.intro_pattern_naming_eq nam1 nam2 + | GCast (c1, t1), GCast (c2, t2) -> + f c1 c2 && cast_type_eq f t1 t2 + | (GRef _ | GVar _ | GEvar _ | GPatVar _ | GApp _ | GLambda _ | GProd _ | GLetIn _ | + GCases _ | GLetTuple _ | GIf _ | GRec _ | GSort _ | GHole _ | GCast _), _ -> false + +let rec glob_constr_eq c = mk_glob_constr_eq glob_constr_eq c let map_glob_constr_left_to_right f = CAst.map (function | GApp (g,args) -> @@ -215,20 +210,20 @@ let fold_glob_constr f acc = CAst.with_val (function ) let fold_return_type_with_binders f g v acc (na,tyopt) = - Option.fold_left (f (name_fold g na v)) acc tyopt + Option.fold_left (f (Name.fold_right g na v)) acc tyopt let fold_glob_constr_with_binders g f v acc = CAst.(with_val (function | GVar _ -> acc | GApp (c,args) -> List.fold_left (f v) (f v acc c) args | GLambda (na,_,b,c) | GProd (na,_,b,c) -> - f (name_fold g na v) (f v acc b) c + f (Name.fold_right g na v) (f v acc b) c | GLetIn (na,b,t,c) -> - f (name_fold g na v) (Option.fold_left (f v) (f v acc b) t) c + f (Name.fold_right g na v) (Option.fold_left (f v) (f v acc b) t) c | GCases (_,rtntypopt,tml,pl) -> let fold_pattern acc (_,(idl,p,c)) = f (List.fold_right g idl v) acc c in let fold_tomatch (v',acc) (tm,(na,onal)) = - (Option.fold_left (fun v'' (_,(_,nal)) -> List.fold_right (name_fold g) nal v'') - (name_fold g na v') onal, + (Option.fold_left (fun v'' (_,(_,nal)) -> List.fold_right (Name.fold_right g) nal v'') + (Name.fold_right g na v') onal, f v acc tm) in let (v',acc) = List.fold_left fold_tomatch (v,acc) tml in let acc = Option.fold_left (f v') acc rtntypopt in @@ -242,7 +237,7 @@ let fold_glob_constr_with_binders g f v acc = CAst.(with_val (function let v,acc = List.fold_left (fun (v,acc) (na,k,bbd,bty) -> - (name_fold g na v, f v (Option.fold_left (f v) acc bbd) bty)) + (Name.fold_right g na v, f v (Option.fold_left (f v) acc bbd) bty)) (v,acc) bll.(i) in f (Array.fold_right g idl v) (f v acc tyl.(i)) (bv.(i)) in @@ -371,12 +366,12 @@ let loc_of_glob_constr c = c.CAst.loc let collide_id l id = List.exists (fun (id',id'') -> Id.equal id id' || Id.equal id id'') l let test_id l id = if collide_id l id then raise Not_found -let test_na l na = name_iter (test_id l) na +let test_na l na = Name.iter (test_id l) na let update_subst na l = let in_range id l = List.exists (fun (_,id') -> Id.equal id id') l in - let l' = name_fold Id.List.remove_assoc na l in - name_fold + let l' = Name.fold_right Id.List.remove_assoc na l in + Name.fold_right (fun id _ -> if in_range id l' then let id' = Namegen.next_ident_away_from id (fun id' -> in_range id' l') in diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index aa48516af..f7cc08ca2 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -36,6 +36,9 @@ val map_glob_constr_left_to_right : val warn_variable_collision : ?loc:Loc.t -> Id.t -> unit +val mk_glob_constr_eq : (glob_constr -> glob_constr -> bool) -> + glob_constr -> glob_constr -> bool + val fold_glob_constr : ('a -> glob_constr -> 'a) -> 'a -> glob_constr -> 'a val fold_glob_constr_with_binders : (Id.t -> 'a -> 'a) -> ('a -> 'b -> glob_constr -> 'b) -> 'a -> 'b -> glob_constr -> 'b val iter_glob_constr : (glob_constr -> unit) -> glob_constr -> unit diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 1c8ad0cdd..0818a5525 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -340,15 +340,15 @@ let rec pat_of_raw metas vars = CAst.with_loc_val (fun ?loc -> function PApp (pat_of_raw metas vars c, Array.of_list (List.map (pat_of_raw metas vars) cl)) | GLambda (na,bk,c1,c2) -> - name_iter (fun n -> metas := n::!metas) na; + Name.iter (fun n -> metas := n::!metas) na; PLambda (na, pat_of_raw metas vars c1, pat_of_raw metas (na::vars) c2) | GProd (na,bk,c1,c2) -> - name_iter (fun n -> metas := n::!metas) na; + Name.iter (fun n -> metas := n::!metas) na; PProd (na, pat_of_raw metas vars c1, pat_of_raw metas (na::vars) c2) | GLetIn (na,c1,t,c2) -> - name_iter (fun n -> metas := n::!metas) na; + Name.iter (fun n -> metas := n::!metas) na; PLetIn (na, pat_of_raw metas vars c1, Option.map (pat_of_raw metas vars) t, pat_of_raw metas (na::vars) c2) @@ -411,7 +411,7 @@ let rec pat_of_raw metas vars = CAst.with_loc_val (fun ?loc -> function and pats_of_glob_branches loc metas vars ind brs = let get_arg = function | { CAst.v = PatVar na } -> - name_iter (fun n -> metas := n::!metas) na; + Name.iter (fun n -> metas := n::!metas) na; na | { CAst.v = PatCstr(_,_,_) ; loc } -> err ?loc (Pp.str "Non supported pattern.") in diff --git a/pretyping/program.ml b/pretyping/program.ml index 8769c5659..2fa3facb3 100644 --- a/pretyping/program.ml +++ b/pretyping/program.ml @@ -9,7 +9,6 @@ open CErrors open Util -let init_constant dir s () = Universes.constr_of_global @@ Coqlib.coq_reference "Program" dir s let init_reference dir s () = Coqlib.coq_reference "Program" dir s let papp evdref r args = @@ -39,20 +38,25 @@ let coq_eq_rect = init_reference ["Init"; "Logic"] "eq_rect" let coq_JMeq_ind = init_reference ["Logic";"JMeq"] "JMeq" let coq_JMeq_refl = init_reference ["Logic";"JMeq"] "JMeq_refl" -let coq_not = init_constant ["Init";"Logic"] "not" -let coq_and = init_constant ["Init";"Logic"] "and" +let coq_not = init_reference ["Init";"Logic"] "not" +let coq_and = init_reference ["Init";"Logic"] "and" -let delayed_force c = EConstr.of_constr (c ()) +let new_global sigma gr = + let open Sigma in + let Sigma (c, sigma, _) = Evarutil.new_global (Sigma.Unsafe.of_evar_map sigma) gr + in Sigma.to_evar_map sigma, c -let mk_coq_not x = EConstr.mkApp (delayed_force coq_not, [| x |]) +let mk_coq_not sigma x = + let sigma, notc = new_global sigma (coq_not ()) in + sigma, EConstr.mkApp (notc, [| x |]) let unsafe_fold_right f = function hd :: tl -> List.fold_right f tl hd | [] -> invalid_arg "unsafe_fold_right" -let mk_coq_and l = - let and_typ = delayed_force coq_and in - unsafe_fold_right +let mk_coq_and sigma l = + let sigma, and_typ = new_global sigma (coq_and ()) in + sigma, unsafe_fold_right (fun c conj -> EConstr.mkApp (and_typ, [| c ; conj |])) l diff --git a/pretyping/program.mli b/pretyping/program.mli index 94a7bdcb6..8439b9528 100644 --- a/pretyping/program.mli +++ b/pretyping/program.mli @@ -32,8 +32,8 @@ val coq_eq_rect : unit -> global_reference val coq_JMeq_ind : unit -> global_reference val coq_JMeq_refl : unit -> global_reference -val mk_coq_and : constr list -> constr -val mk_coq_not : constr -> constr +val mk_coq_and : Evd.evar_map -> constr list -> Evd.evar_map * constr +val mk_coq_not : Evd.evar_map -> constr -> Evd.evar_map * constr (** Polymorphic application of delayed references *) val papp : Evd.evar_map ref -> (unit -> global_reference) -> constr array -> constr diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index e7c963582..5a2328aaa 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1317,19 +1317,23 @@ let sigma_univ_state = let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y = (** FIXME *) + let open Universes in let x = EConstr.Unsafe.to_constr x in let y = EConstr.Unsafe.to_constr y in try - let fold cstr sigma = - try Some (Evd.add_universe_constraints sigma cstr) - with Univ.UniverseInconsistency _ | Evd.UniversesDiffer -> None - in + let fold cstr accu = Some (Constraints.fold Constraints.add cstr accu) in let b, sigma = let ans = if pb == Reduction.CUMUL then - Universes.leq_constr_univs_infer (Evd.universes sigma) fold x y sigma + Universes.leq_constr_univs_infer (Evd.universes sigma) fold x y Constraints.empty else - Universes.eq_constr_univs_infer (Evd.universes sigma) fold x y sigma + Universes.eq_constr_univs_infer (Evd.universes sigma) fold x y Constraints.empty + in + let ans = match ans with + | None -> None + | Some cstr -> + try Some (Evd.add_universe_constraints sigma cstr) + with Univ.UniverseInconsistency _ | Evd.UniversesDiffer -> None in match ans with | None -> false, sigma diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index f76555b04..60511d913 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -151,8 +151,8 @@ let tag_var = tag Tag.variable let pr_univ l = match l with - | [_,x] -> pr_name x - | l -> str"max(" ++ prlist_with_sep (fun () -> str",") (fun x -> pr_name (snd x)) l ++ str")" + | [_,x] -> Name.print x + | l -> str"max(" ++ prlist_with_sep (fun () -> str",") (fun x -> Name.print (snd x)) l ++ str")" let pr_univ_annot pr x = str "@{" ++ pr x ++ str "}" @@ -166,7 +166,7 @@ let tag_var = tag Tag.variable | GProp -> tag_type (str "Prop") | GSet -> tag_type (str "Set") | GType None -> tag_type (str "Type") - | GType (Some (_, u)) -> tag_type (pr_name u) + | GType (Some (_, u)) -> tag_type (Name.print u) let pr_qualid sp = let (sl, id) = repr_qualid sp in @@ -191,7 +191,7 @@ let tag_var = tag Tag.variable tag_type (str "Set") | GType u -> (match u with - | Some (_,u) -> pr_name u + | Some (_,u) -> Name.print u | None -> tag_type (str "Type")) let pr_universe_instance l = @@ -224,7 +224,7 @@ let tag_var = tag Tag.variable let pr_lname = function | (loc,Name id) -> pr_lident (loc,id) - | lna -> pr_located pr_name lna + | lna -> pr_located Name.print lna let pr_or_var pr = function | ArgArg x -> pr x diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index c328b6032..6aa136b60 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -56,7 +56,7 @@ open Decl_kinds let pr_lname = function | (loc,Name id) -> pr_lident (loc,id) - | lna -> pr_located pr_name lna + | lna -> pr_located Name.print lna let pr_smart_global = Pputils.pr_or_by_notation pr_reference @@ -1022,13 +1022,13 @@ open Decl_kinds | n, { name = id; recarg_like = k; notation_scope = s; implicit_status = imp } :: tl -> - spc() ++ pr_br imp (pr_if k (str"!") ++ pr_name id ++ pr_s s) ++ + spc() ++ pr_br imp (pr_if k (str"!") ++ Name.print id ++ pr_s s) ++ print_arguments (Option.map pred n) tl in let rec print_implicits = function | [] -> mt () | (name, impl) :: rest -> - spc() ++ pr_br impl (pr_name name) ++ print_implicits rest + spc() ++ pr_br impl (Name.print name) ++ print_implicits rest in print_arguments nargs args ++ if not (List.is_empty more_implicits) then diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 0f7da3613..2b21b3f9e 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -132,7 +132,7 @@ let print_impargs_list prefix l = let print_renames_list prefix l = if List.is_empty l then [] else [add_colon prefix ++ str "Arguments are renamed to " ++ - hv 2 (prlist_with_sep pr_comma (fun x -> x) (List.map pr_name l))] + hv 2 (prlist_with_sep pr_comma (fun x -> x) (List.map Name.print l))] let need_expansion impl ref = let typ = Global.type_of_global_unsafe ref in diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 33a86402e..87b31849e 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -433,7 +433,7 @@ let explain_no_such_bound_variable evd id = | Cltyp (na, _) -> na | Clval (na, _, _) -> na in - if na != Anonymous then out_name na :: l else l + if na != Anonymous then Name.get_id na :: l else l in let mvl = List.fold_left fold [] (Evd.meta_list evd) in user_err ~hdr:"Evd.meta_with_name" diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 97c5cda77..66d91c634 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -75,7 +75,7 @@ let pf_get_new_ids ids gls = (fun id acc -> (next_ident_away id (acc@avoid))::acc) ids [] -let pf_global gls id = EConstr.of_constr (Constrintern.construct_reference (pf_hyps gls) id) +let pf_global gls id = EConstr.of_constr (Universes.constr_of_global (Constrintern.construct_reference (pf_hyps gls) id)) let pf_reduction_of_red_expr gls re c = let (redfun, _) = reduction_of_red_expr (pf_env gls) re in @@ -171,7 +171,7 @@ module New = struct (** We only check for the existence of an [id] in [hyps] *) let gl = Proofview.Goal.assume gl in let hyps = Proofview.Goal.hyps gl in - EConstr.of_constr (Constrintern.construct_reference hyps id) + Constrintern.construct_reference hyps id let pf_env = Proofview.Goal.env let pf_concl = Proofview.Goal.concl diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index e6e60e27f..1172e55ac 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -100,7 +100,7 @@ val pr_glls : goal list sigma -> Pp.std_ppcmds (* Variants of [Tacmach] functions built with the new proof engine *) module New : sig val pf_apply : (env -> evar_map -> 'a) -> ('b, 'r) Proofview.Goal.t -> 'a - val pf_global : identifier -> ('a, 'r) Proofview.Goal.t -> constr + val pf_global : identifier -> ('a, 'r) Proofview.Goal.t -> Globnames.global_reference (** FIXME: encapsulate the level in an existential type. *) val of_old : (Proof_type.goal Evd.sigma -> 'a) -> ([ `NF ], 'r) Proofview.Goal.t -> 'a diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index fe44559ed..5e7090ded 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -19,10 +19,9 @@ module NamedDecl = Context.Named.Declaration (* Absurd *) -let mk_absurd_proof t = - let build_coq_not () = EConstr.of_constr (Universes.constr_of_global @@ build_coq_not ()) in +let mk_absurd_proof coq_not t = let id = Namegen.default_dependent_ident in - mkLambda (Names.Name id,mkApp(build_coq_not (),[|t|]), + mkLambda (Names.Name id,mkApp(coq_not,[|t|]), mkLambda (Names.Name id,t,mkApp (mkRel 2,[|mkRel 1|]))) let absurd c = @@ -34,9 +33,11 @@ let absurd c = let sigma, j = Coercion.inh_coerce_to_sort env sigma j in let t = j.Environ.utj_val in let tac = + Tacticals.New.pf_constr_of_global (build_coq_not ()) >>= fun coqnot -> + Tacticals.New.pf_constr_of_global (build_coq_False ()) >>= fun coqfalse -> Tacticals.New.tclTHENLIST [ - elim_type (EConstr.of_constr (Universes.constr_of_global @@ build_coq_False ())); - Simple.apply (mk_absurd_proof t) + elim_type coqfalse; + Simple.apply (mk_absurd_proof coqnot t) ] in Sigma.Unsafe.of_pair (tac, sigma) end } diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml index bda25d7f0..48ce52f09 100644 --- a/tactics/eqdecide.ml +++ b/tactics/eqdecide.ml @@ -104,14 +104,9 @@ let solveNoteqBranch side = (* Constructs the type {c1=c2}+{~c1=c2} *) -let make_eq () = -(*FIXME*) EConstr.of_constr (Universes.constr_of_global (Coqlib.build_coq_eq ())) -let build_coq_not () = EConstr.of_constr (Universes.constr_of_global @@ build_coq_not ()) -let build_coq_sumbool () = EConstr.of_constr (Universes.constr_of_global @@ build_coq_sumbool ()) - -let mkDecideEqGoal eqonleft op rectype c1 c2 = - let equality = mkApp(make_eq(), [|rectype; c1; c2|]) in - let disequality = mkApp(build_coq_not (), [|equality|]) in +let mkDecideEqGoal eqonleft (op,eq,neg) rectype c1 c2 = + let equality = mkApp(eq, [|rectype; c1; c2|]) in + let disequality = mkApp(neg, [|equality|]) in if eqonleft then mkApp(op, [|equality; disequality |]) else mkApp(op, [|disequality; equality |]) @@ -121,13 +116,13 @@ let mkDecideEqGoal eqonleft op rectype c1 c2 = let idx = Id.of_string "x" let idy = Id.of_string "y" -let mkGenDecideEqGoal rectype g = +let mkGenDecideEqGoal rectype ops g = let hypnames = pf_ids_of_hyps g in let xname = next_ident_away idx hypnames and yname = next_ident_away idy hypnames in (mkNamedProd xname rectype (mkNamedProd yname rectype - (mkDecideEqGoal true (build_coq_sumbool ()) + (mkDecideEqGoal true ops rectype (mkVar xname) (mkVar yname)))) let rec rewrite_and_clear hyps = match hyps with @@ -256,9 +251,9 @@ let decideGralEquality = let decideEqualityGoal = tclTHEN intros decideGralEquality -let decideEquality rectype = +let decideEquality rectype ops = Proofview.Goal.enter { enter = begin fun gl -> - let decide = mkGenDecideEqGoal rectype gl in + let decide = mkGenDecideEqGoal rectype ops gl in (tclTHENS (cut decide) [default_auto;decideEqualityGoal]) end } @@ -266,11 +261,15 @@ let decideEquality rectype = (* The tactic Compare *) let compare c1 c2 = + pf_constr_of_global (build_coq_sumbool ()) >>= fun opc -> + pf_constr_of_global (Coqlib.build_coq_eq ()) >>= fun eqc -> + pf_constr_of_global (build_coq_not ()) >>= fun notc -> Proofview.Goal.enter { enter = begin fun gl -> let rectype = pf_unsafe_type_of gl c1 in - let decide = mkDecideEqGoal true (build_coq_sumbool ()) rectype c1 c2 in + let ops = (opc,eqc,notc) in + let decide = mkDecideEqGoal true ops rectype c1 c2 in (tclTHENS (cut decide) [(tclTHEN intro (tclTHEN (onLastHyp simplest_case) clear_last)); - decideEquality rectype]) + decideEquality rectype ops]) end } diff --git a/tactics/equality.ml b/tactics/equality.ml index e6278943d..268daf6b6 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -874,7 +874,7 @@ let descend_then env sigma head dirn = let dirn_env = Environ.push_rel_context cstr.(dirn-1).cs_args env in (dirn_nlams, dirn_env, - (fun dirnval (dfltval,resty) -> + (fun sigma dirnval (dfltval,resty) -> let deparsign = make_arity_signature env sigma true indf in let p = it_mkLambda_or_LetIn (lift (mip.mind_nrealargs+1) resty) deparsign in @@ -887,7 +887,7 @@ let descend_then env sigma head dirn = List.map build_branch (List.interval 1 (Array.length mip.mind_consnames)) in let ci = make_case_info env ind RegularStyle in - Inductiveops.make_case_or_project env sigma indf ci p head (Array.of_list brl))) + sigma, Inductiveops.make_case_or_project env sigma indf ci p head (Array.of_list brl))) (* Now we need to construct the discriminator, given a discriminable position. This boils down to: @@ -932,23 +932,28 @@ let build_selector env sigma dirn c ind special default = let brl = List.map build_branch(List.interval 1 (Array.length mip.mind_consnames)) in let ci = make_case_info env ind RegularStyle in - mkCase (ci, p, c, Array.of_list brl) + sigma, mkCase (ci, p, c, Array.of_list brl) -let build_coq_False () = EConstr.of_constr (Universes.constr_of_global @@ build_coq_False ()) -let build_coq_True () = EConstr.of_constr (Universes.constr_of_global @@ build_coq_True ()) -let build_coq_I () = EConstr.of_constr (Universes.constr_of_global @@ build_coq_I ()) +let new_global sigma gr = + let Sigma (c, sigma, _) = Evarutil.new_global (Sigma.Unsafe.of_evar_map sigma) gr + in Sigma.to_evar_map sigma, c + +let build_coq_False sigma = new_global sigma (build_coq_False ()) +let build_coq_True sigma = new_global sigma (build_coq_True ()) +let build_coq_I sigma = new_global sigma (build_coq_I ()) let rec build_discriminator env sigma dirn c = function | [] -> let ind = get_type_of env sigma c in - let true_0,false_0 = - build_coq_True(),build_coq_False() in + let sigma, true_0 = build_coq_True sigma in + let sigma, false_0 = build_coq_False sigma in build_selector env sigma dirn c ind true_0 false_0 | ((sp,cnum),argnum)::l -> + let sigma, false_0 = build_coq_False sigma in let (cnum_nlams,cnum_env,kont) = descend_then env sigma c cnum in let newc = mkRel(cnum_nlams-argnum) in - let subval = build_discriminator cnum_env sigma dirn newc l in - kont subval (build_coq_False (),mkSort (Prop Null)) + let sigma, subval = build_discriminator cnum_env sigma dirn newc l in + kont sigma subval (false_0,mkSort (Prop Null)) (* Note: discrimination could be more clever: if some elimination is not allowed because of a large impredicative constructor in the @@ -991,9 +996,9 @@ let ind_scheme_of_eq lbeq = let discrimination_pf env sigma e (t,t1,t2) discriminator lbeq = - let i = build_coq_I () in - let absurd_term = build_coq_False () in - let eq_elim, eff = ind_scheme_of_eq lbeq in + let sigma, i = build_coq_I sigma in + let sigma, absurd_term = build_coq_False sigma in + let eq_elim, eff = ind_scheme_of_eq lbeq in let sigma, eq_elim = Evd.fresh_global (Global.env ()) sigma eq_elim in let eq_elim = EConstr.of_constr eq_elim in sigma, (applist (eq_elim, [t;t1;mkNamedLambda e t discriminator;i;t2]), absurd_term), @@ -1013,7 +1018,7 @@ let apply_on_clause (f,t) clause = let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn = let e = next_ident_away eq_baseid (ids_of_context env) in let e_env = push_named (Context.Named.Declaration.LocalAssum (e,t)) env in - let discriminator = + let sigma, discriminator = build_discriminator e_env sigma dirn (mkVar e) cpath in let sigma,(pf, absurd_term), eff = discrimination_pf env sigma e (t,t1,t2) discriminator lbeq in @@ -1309,7 +1314,8 @@ let rec build_injrec env sigma dflt c = function let (cnum_nlams,cnum_env,kont) = descend_then env sigma c cnum in let newc = mkRel(cnum_nlams-argnum) in let sigma, (subval,tuplety,dfltval) = build_injrec cnum_env sigma dflt newc l in - sigma, (kont subval (dfltval,tuplety), tuplety,dfltval) + let sigma, res = kont sigma subval (dfltval,tuplety) in + sigma, (res, tuplety,dfltval) with UserError _ -> failwith "caught" @@ -1326,8 +1332,6 @@ let inject_if_homogenous_dependent_pair ty = let sigma = Tacmach.New.project gl in let eq,u,(t,t1,t2) = find_this_eq_data_decompose gl ty in (* fetch the informations of the pair *) - let ceq = Universes.constr_of_global Coqlib.glob_eq in - let ceq = EConstr.of_constr ceq in let sigTconstr () = (Coqlib.build_sigma_type()).Coqlib.typ in let existTconstr () = (Coqlib.build_sigma_type()).Coqlib.intro in (* check whether the equality deals with dep pairs or not *) @@ -1346,16 +1350,18 @@ let inject_if_homogenous_dependent_pair ty = pf_apply is_conv gl ar1.(2) ar2.(2)) then raise Exit; Coqlib.check_required_library ["Coq";"Logic";"Eqdep_dec"]; let new_eq_args = [|pf_unsafe_type_of gl ar1.(3);ar1.(3);ar2.(3)|] in - let inj2 = EConstr.of_constr @@ Universes.constr_of_global @@ - Coqlib.coq_reference "inj_pair2_eq_dec is missing" ["Logic";"Eqdep_dec"] "inj_pair2_eq_dec" in + let inj2 = Coqlib.coq_reference "inj_pair2_eq_dec is missing" ["Logic";"Eqdep_dec"] + "inj_pair2_eq_dec" in let c, eff = find_scheme (!eq_dec_scheme_kind_name()) ind in (* cut with the good equality and prove the requested goal *) tclTHENLIST [Proofview.tclEFFECTS eff; intro; onLastHyp (fun hyp -> + Tacticals.New.pf_constr_of_global Coqlib.glob_eq >>= fun ceq -> tclTHENS (cut (mkApp (ceq,new_eq_args))) [clear [destVar sigma hyp]; + Tacticals.New.pf_constr_of_global inj2 >>= fun inj2 -> Proofview.V82.tactic (Tacmach.refine (mkApp(inj2,[|ar1.(0);mkConst c;ar1.(1);ar1.(2);ar1.(3);ar2.(3);hyp|]))) ])] diff --git a/tactics/equality.mli b/tactics/equality.mli index b47be3bbc..27be5affb 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -126,4 +126,4 @@ val set_eq_dec_scheme_kind : mutual scheme_kind -> unit (* [build_selector env sigma i c t u v] matches on [c] of type [t] and returns [u] in branch [i] and [v] on other branches *) val build_selector : env -> evar_map -> int -> constr -> types -> - constr -> constr -> constr + constr -> constr -> evar_map * constr diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index 35fbec5a6..2ba18ceb4 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -544,7 +544,7 @@ let match_eqdec sigma t = false,op_or,matches sigma (Lazy.force coq_eqdec_rev_pattern) t in match Id.Map.bindings subst with | [(_,typ);(_,c1);(_,c2)] -> - eqonleft, EConstr.of_constr (Universes.constr_of_global (Lazy.force op)), c1, c2, typ + eqonleft, Lazy.force op, c1, c2, typ | _ -> anomaly (Pp.str "Unexpected pattern") (* Patterns "~ ?" and "? -> False" *) diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli index 82a3d47b5..9110830aa 100644 --- a/tactics/hipattern.mli +++ b/tactics/hipattern.mli @@ -142,7 +142,7 @@ val is_matching_sigma : evar_map -> constr -> bool (** Match a decidable equality judgement (e.g [{t=u:>T}+{~t=u}]), returns [t,u,T] and a boolean telling if equality is on the left side *) -val match_eqdec : evar_map -> constr -> bool * constr * constr * constr * constr +val match_eqdec : evar_map -> constr -> bool * Globnames.global_reference * constr * constr * constr (** Match an equality up to conversion; returns [(eq,t1,t2)] in normal form *) val dest_nf_eq : ('a, 'r) Proofview.Goal.t -> constr -> (constr * constr * constr) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index f4408d403..2a9928a3a 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2954,6 +2954,19 @@ let quantify lconstr = (* Modifying/Adding an hypothesis *) +(* Instantiating some arguments (whatever their position) of an hypothesis + or any term, leaving other arguments quantified. If operating on an + hypothesis of the goal, the new hypothesis replaces it. + + (c,lbind) are supposed to be of the form + ((t t1 t2 ... tm) , someBindings) + + in which case we pose a proof with body + + (fun y1...yp => H t1 t2 ... tm u1 ... uq) where yi are the + remaining arguments of H that lbind could not resolve, ui are a mix + of inferred args and yi. The overall effect is to remove from H as + much quantification as possible given lbind. *) let specialize (c,lbind) ipat = Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in @@ -2962,22 +2975,49 @@ let specialize (c,lbind) ipat = if lbind == NoBindings then sigma, c else - let clause = make_clenv_binding env sigma (c,Retyping.get_type_of env sigma c) lbind in + let typ_of_c = Retyping.get_type_of env sigma c in + (* If the term is lambda then we put a letin to put avoid + interaction between the term and the bindings. *) + let c = match EConstr.kind sigma c with + | Lambda(_,_,_) -> + mkLetIn(Name.Anonymous, c, typ_of_c, (mkRel 1)) + | _ -> c in + let clause = make_clenv_binding env sigma (c,typ_of_c) lbind in let flags = { (default_unify_flags ()) with resolve_evars = true } in let clause = clenv_unify_meta_types ~flags clause in - let (thd,tstack) = whd_nored_stack clause.evd (clenv_value clause) in - let rec chk = function - | [] -> [] - | t::l -> if occur_meta clause.evd t then [] else t :: chk l - in - let tstack = chk tstack in - let term = applist(thd,List.map (nf_evar clause.evd) tstack) in - if occur_meta clause.evd term then - user_err (str "Cannot infer an instance for " ++ - - pr_name (meta_name clause.evd (List.hd (collect_metas clause.evd term))) ++ - str "."); - clause.evd, term in + let sigma = clause.evd in + let (thd,tstack) = whd_nored_stack sigma (clenv_value clause) in + let c_hd , c_args = decompose_app sigma c in + let liftrel x = + match kind sigma x with + | Rel n -> mkRel (n+1) + | _ -> x in + (* We grab names used in product to remember them at re-abstracting phase *) + let typ_of_c_hd = pf_get_type_of gl c_hd in + let lprod, concl = decompose_prod_assum sigma typ_of_c_hd in + (* accumulator args: arguments to apply to c_hd: all infered + args + re-abstracted rels *) + let rec rebuild_lambdas sigma lprd args hd l = + match lprd , l with + | _, [] -> sigma,applist (hd, (List.map (nf_evar sigma) args)) + | Context.Rel.Declaration.LocalAssum(nme,_)::lp' , t::l' when occur_meta sigma t -> + (* nme has not been resolved, let us re-abstract it. Same + name but type updated by instanciation of other args. *) + let sigma,new_typ_of_t = Typing.type_of clause.env sigma t in + let liftedargs = List.map liftrel args in + (* lifting rels in the accumulator args *) + let sigma,hd' = rebuild_lambdas sigma lp' (liftedargs@[mkRel 1 ]) hd l' in + (* replace meta variable by the abstracted variable *) + let hd'' = subst_term sigma t hd' in + (* lambda expansion *) + sigma,mkLambda (nme,new_typ_of_t,hd'') + | Context.Rel.Declaration.LocalAssum(_,_)::lp' , t::l' -> + let sigma,hd' = rebuild_lambdas sigma lp' (args@[t]) hd l' in + sigma,hd' + | _ ,_ -> assert false in + let sigma,hd = rebuild_lambdas sigma (List.rev lprod) [] c_hd tstack in + sigma, hd + in let typ = Retyping.get_type_of env sigma term in let tac = match EConstr.kind sigma (fst(EConstr.decompose_app sigma (snd(EConstr.decompose_lam_assum sigma c)))) with @@ -2994,7 +3034,9 @@ let specialize (c,lbind) ipat = | None -> (* Like generalize with extra support for "with" bindings *) (* even though the "with" bindings forces full application *) - Tacticals.New.tclTHENLAST (cut typ) (exact_no_check term) + (* TODO: add intro to be more homogeneous. It will break + scripts but will be easy to fix *) + (Tacticals.New.tclTHENLAST (cut typ) (exact_no_check term)) | Some (loc,ipat) -> (* Like pose proof with extra support for "with" bindings *) (* even though the "with" bindings forces full application *) @@ -3519,27 +3561,32 @@ let error_ind_scheme s = let s = if not (String.is_empty s) then s^" " else s in user_err ~hdr:"Tactics" (str "Cannot recognize " ++ str s ++ str "an induction scheme.") -let glob c = EConstr.of_constr (Universes.constr_of_global c) +let glob sigma gr = + let Sigma (c, sigma, _) = Evarutil.new_global (Sigma.Unsafe.of_evar_map sigma) gr + in Sigma.to_evar_map sigma, c -let coq_eq = lazy (glob (Coqlib.build_coq_eq ())) -let coq_eq_refl = lazy (glob (Coqlib.build_coq_eq_refl ())) +let coq_eq sigma = glob sigma (Coqlib.build_coq_eq ()) +let coq_eq_refl sigma = glob sigma (Coqlib.build_coq_eq_refl ()) -let coq_heq = lazy (EConstr.of_constr @@ Universes.constr_of_global (Coqlib.coq_reference"mkHEq" ["Logic";"JMeq"] "JMeq")) -let coq_heq_refl = lazy (EConstr.of_constr @@ Universes.constr_of_global (Coqlib.coq_reference "mkHEq" ["Logic";"JMeq"] "JMeq_refl")) +let coq_heq_ref = lazy (Coqlib.coq_reference"mkHEq" ["Logic";"JMeq"] "JMeq") +let coq_heq sigma = glob sigma (Lazy.force coq_heq_ref) +let coq_heq_refl sigma = glob sigma (Coqlib.coq_reference "mkHEq" ["Logic";"JMeq"] "JMeq_refl") -let mkEq t x y = - mkApp (Lazy.force coq_eq, [| t; x; y |]) +let mkEq sigma t x y = + let sigma, eq = coq_eq sigma in + sigma, mkApp (eq, [| t; x; y |]) -let mkRefl t x = - mkApp (Lazy.force coq_eq_refl, [| t; x |]) +let mkRefl sigma t x = + let sigma, refl = coq_eq_refl sigma in + sigma, mkApp (refl, [| t; x |]) -let mkHEq t x u y = - mkApp (Lazy.force coq_heq, - [| t; x; u; y |]) +let mkHEq sigma t x u y = + let sigma, c = coq_heq sigma in + sigma, mkApp (c,[| t; x; u; y |]) -let mkHRefl t x = - mkApp (Lazy.force coq_heq_refl, - [| t; x |]) +let mkHRefl sigma t x = + let sigma, c = coq_heq_refl sigma in + sigma, mkApp (c, [| t; x |]) let lift_togethern n l = let l', _ = @@ -3577,23 +3624,30 @@ let decompose_indapp sigma f args = mkApp (f, pars), args | _ -> f, args -let mk_term_eq env sigma ty t ty' t' = +let mk_term_eq homogeneous env sigma ty t ty' t' = let sigma = Sigma.to_evar_map sigma in - if Reductionops.is_conv env sigma ty ty' then - mkEq ty t t', mkRefl ty' t' + if homogeneous then + let sigma, eq = mkEq sigma ty t t' in + let sigma, refl = mkRefl sigma ty' t' in + Sigma.Unsafe.of_evar_map sigma, (eq, refl) else - mkHEq ty t ty' t', mkHRefl ty' t' + let sigma, heq = mkHEq sigma ty t ty' t' in + let sigma, hrefl = mkHRefl sigma ty' t' in + Sigma.Unsafe.of_evar_map sigma, (heq, hrefl) let make_abstract_generalize env id typ concl dep ctx body c eqs args refls = let open Context.Rel.Declaration in Refine.refine { run = begin fun sigma -> let eqslen = List.length eqs in (* Abstract by the "generalized" hypothesis equality proof if necessary. *) - let abshypeq, abshypt = + let sigma, abshypeq, abshypt = if dep then - let eq, refl = mk_term_eq (push_rel_context ctx env) sigma (lift 1 c) (mkRel 1) typ (mkVar id) in - mkProd (Anonymous, eq, lift 1 concl), [| refl |] - else concl, [||] + let ty = lift 1 c in + let homogeneous = Reductionops.is_conv env (Sigma.to_evar_map sigma) ty typ in + let sigma, (eq, refl) = + mk_term_eq homogeneous (push_rel_context ctx env) sigma ty (mkRel 1) typ (mkVar id) in + sigma, mkProd (Anonymous, eq, lift 1 concl), [| refl |] + else sigma, concl, [||] in (* Abstract by equalities *) let eqs = lift_togethern 1 eqs in (* lift together and past genarg *) @@ -3699,9 +3753,13 @@ let abstract_args gl generalize_vars dep id defined f args = let liftarg = lift (List.length ctx) arg in let eq, refl = if leq then - mkEq (lift 1 ty) (mkRel 1) liftarg, mkRefl (lift (-lenctx) ty) arg + let sigma', eq = mkEq !sigma (lift 1 ty) (mkRel 1) liftarg in + let sigma', refl = mkRefl sigma' (lift (-lenctx) ty) arg in + sigma := sigma'; eq, refl else - mkHEq (lift 1 ty) (mkRel 1) liftargty liftarg, mkHRefl argty arg + let sigma', eq = mkHEq !sigma (lift 1 ty) (mkRel 1) liftargty liftarg in + let sigma', refl = mkHRefl sigma' argty arg in + sigma := sigma'; eq, refl in let eqs = eq :: lift_list eqs in let refls = refl :: refls in @@ -3801,17 +3859,19 @@ let specialize_eqs id gl = match EConstr.kind !evars ty with | Prod (na, t, b) -> (match EConstr.kind !evars t with - | App (eq, [| eqty; x; y |]) when EConstr.eq_constr !evars (Lazy.force coq_eq) eq -> + | App (eq, [| eqty; x; y |]) when EConstr.is_global !evars (Lazy.force coq_eq_ref) eq -> let c = if noccur_between !evars 1 (List.length ctx) x then y else x in - let pt = mkApp (Lazy.force coq_eq, [| eqty; c; c |]) in - let p = mkApp (Lazy.force coq_eq_refl, [| eqty; c |]) in + let pt = mkApp (eq, [| eqty; c; c |]) in + let ind = destInd !evars eq in + let p = mkApp (mkConstructUi (ind,0), [| eqty; c |]) in if unif (push_rel_context ctx env) evars pt t then aux true ctx (mkApp (acc, [| p |])) (subst1 p b) else acc, in_eqs, ctx, ty - | App (heq, [| eqty; x; eqty'; y |]) when EConstr.eq_constr !evars heq (Lazy.force coq_heq) -> + | App (heq, [| eqty; x; eqty'; y |]) when EConstr.is_global !evars (Lazy.force coq_heq_ref) heq -> let eqt, c = if noccur_between !evars 1 (List.length ctx) x then eqty', y else eqty, x in - let pt = mkApp (Lazy.force coq_heq, [| eqt; c; eqt; c |]) in - let p = mkApp (Lazy.force coq_heq_refl, [| eqt; c |]) in + let pt = mkApp (heq, [| eqt; c; eqt; c |]) in + let ind = destInd !evars heq in + let p = mkApp (mkConstructUi (ind,0), [| eqt; c |]) in if unif (push_rel_context ctx env) evars pt t then aux true ctx (mkApp (acc, [| p |])) (subst1 p b) else acc, in_eqs, ctx, ty diff --git a/test-suite/Makefile b/test-suite/Makefile index a26f66285..e15094ccf 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -68,6 +68,7 @@ ifeq (,$(bogomips)) $(warning cannot run complexity tests (no bogomips found)) endif +# keep these synced with test-suite/save-logs.sh log_success = "==========> SUCCESS <==========" log_segfault = "==========> FAILURE <==========" log_anomaly = "==========> FAILURE <==========" @@ -164,7 +165,13 @@ summary.log: $(SHOW) BUILDING SUMMARY FILE $(HIDE)$(MAKE) --quiet summary > "$@" +# if not on travis we can get the log files (they're just there for a +# local build, and downloadable on GitLab) report: summary.log + $(HIDE)./save-logs.sh + $(HIDE)if [ -n "${TRAVIS}" ]; then echo 'travis_fold:start:coq.logs'; fi + $(HIDE)if [ -n "${TRAVIS}" ]; then find logs/ -name '*.log' -not -name 'summary.log' -exec cat '{}' ';'; fi + $(HIDE)if [ -n "${TRAVIS}" ]; then echo 'travis_fold:end:coq.logs'; fi $(HIDE)if grep -q -F 'Error!' summary.log ; then echo FAILURES; grep -F 'Error!' summary.log; false; else echo NO FAILURES; fi ####################################################################### diff --git a/test-suite/bugs/closed/5523.v b/test-suite/bugs/closed/5523.v new file mode 100644 index 000000000..d7582a379 --- /dev/null +++ b/test-suite/bugs/closed/5523.v @@ -0,0 +1,6 @@ +(* Support for complex constructions in recursive notations, especially "match". *) + +Definition Let_In {A P} (x : A) (f : forall a : A, P a) : P x := let y := x in f y. +Notation "'dlet' x , y := v 'in' ( a , b , .. , c )" + := (Let_In v (fun '(x, y) => pair .. (pair a b) .. c)) + (at level 0). diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index 4d59a92cb..f4ecfd736 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -98,5 +98,10 @@ fun n : nat => foo4 n (fun _ y : nat => ETA z : nat, (fun _ : nat => y = 0)) : nat -> Prop tele (t : Type) '(y, z) (x : t0) := tt : forall t : Type, nat * nat -> t -> fpack +[fun x : nat => x + 0;; fun x : nat => x + 1;; fun x : nat => x + 2] + : (nat -> nat) * + ((nat -> nat) * + ((nat -> nat) * + ((nat -> nat) * ((nat -> nat) * ((nat -> nat) * (nat -> nat)))))) foo5 x nat x : nat -> nat diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index 96d831944..71536c68f 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -140,6 +140,12 @@ Notation "'tele' x .. z := b" := Check tele (t:Type) '((y,z):nat*nat) (x:t) := tt. +(* Checking that "fun" in a notation does not mixed up with the + detection of a recursive binder *) + +Notation "[ x ;; .. ;; y ]" := ((x,((fun u => S u), .. (y,(fun u => S u,fun v:nat => v)) ..))). +Check [ fun x => x+0 ;; fun x => x+1 ;; fun x => x+2 ]. + (* Cyprien's part of bug #4765 *) Notation foo5 x T y := (fun x : T => y). diff --git a/test-suite/save-logs.sh b/test-suite/save-logs.sh new file mode 100755 index 000000000..fb8a1c1b0 --- /dev/null +++ b/test-suite/save-logs.sh @@ -0,0 +1,19 @@ +#!/usr/bin/env bash + +SAVEDIR="logs" + +# reset for local builds +rm -rf "$SAVEDIR" +mkdir "$SAVEDIR" + +# keep this synced with test-suite/Makefile +FAILMARK="==========> FAILURE <==========" + +FAILED=$(mktemp) +find . '(' -path ./bugs/opened -prune ')' -o '(' -name '*.log' -exec grep "$FAILMARK" -q '{}' ';' -print0 ')' > "$FAILED" + +rsync -a --from0 --files-from="$FAILED" . "$SAVEDIR" +cp summary.log "$SAVEDIR"/ + +# cleanup +rm "$FAILED" diff --git a/test-suite/success/specialize.v b/test-suite/success/specialize.v index 4b41a509e..f12db8b08 100644 --- a/test-suite/success/specialize.v +++ b/test-suite/success/specialize.v @@ -17,6 +17,29 @@ specialize (eq_trans (x:=a)(y:=b)). intros _. specialize (eq_trans H H0). intros _. specialize (eq_trans H0 (z:=b)). intros _. +(* incomplete bindings: y is left quantified and z is instantiated. *) +specialize eq_trans with (x:=a)(z:=c). +intro h. +(* y can be instantiated now *) +specialize h with (y:=b). +(* z was instantiated above so this must fail. *) +Fail specialize h with (z:=c). +clear h. + +(* incomplete bindings: 1st dep hyp is instantiated thus A, x and y + instantiated too. *) +specialize eq_trans with (1:=H). +intro h. +(* 2nd dep hyp can be instantiated now, which instatiates z too. *) +specialize h with (1:=H0). +(* checking that there is no more products in h. *) +match type of h with +| _ = _ => idtac +| _ => fail "specialize test failed: hypothesis h should be an equality at this point" +end. +clear h. + + (* local "in place" specialization *) assert (Eq:=eq_trans). @@ -31,6 +54,27 @@ specialize (Eq _ a b c). Undo. specialize (Eq _ _ _ _ H H0). Undo. specialize (Eq _ _ _ b H0). Undo. +(* incomplete binding *) +specialize Eq with (y:=b). +(* A and y have been instantiated so this works *) +specialize (Eq _ _ H H0). +Undo 2. + +(* incomplete binding (dependent) *) +specialize Eq with (1:=H). +(* A, x and y have been instantiated so this works *) +specialize (Eq _ H0). +Undo 2. + +(* incomplete binding (dependent) *) +specialize Eq with (1:=H) (2:=H0). +(* A, x and y have been instantiated so this works *) +match type of Eq with +| _ = _ => idtac +| _ => fail "specialize test failed: hypothesis Eq should be an equality at this point" +end. +Undo 2. + (* (** strange behavior to inspect more precisely *) @@ -40,7 +84,7 @@ specialize (Eq _ _ _ b H0). Undo. (* 2) echoue moins lorsque zero premise de mangé *) specialize eq_trans with (1:=Eq). (* mal typé !! *) -(* 3) *) +(* 3) Seems fixed.*) specialize eq_trans with _ a b c. intros _. (* Anomaly: Evar ?88 was not declared. Please report. *) *) diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index cf534f13a..b99ccbf4a 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -533,7 +533,7 @@ open Namegen let compute_bl_goal ind lnamesparrec nparrec = let eqI, eff = eqI ind lnamesparrec in let list_id = list_id lnamesparrec in - let avoid = List.fold_right (Nameops.name_fold (fun id l -> id::l)) (List.map RelDecl.get_name lnamesparrec) [] in + let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> id::l)) (List.map RelDecl.get_name lnamesparrec) [] in let create_input c = let x = next_ident_away (Id.of_string "x") avoid and y = next_ident_away (Id.of_string "y") avoid in @@ -676,7 +676,7 @@ let _ = bl_scheme_kind_aux := fun () -> bl_scheme_kind let compute_lb_goal ind lnamesparrec nparrec = let list_id = list_id lnamesparrec in let eq = Lazy.force eq and tt = Lazy.force tt and bb = Lazy.force bb in - let avoid = List.fold_right (Nameops.name_fold (fun id l -> id::l)) (List.map RelDecl.get_name lnamesparrec) [] in + let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> id::l)) (List.map RelDecl.get_name lnamesparrec) [] in let eqI, eff = eqI ind lnamesparrec in let create_input c = let x = next_ident_away (Id.of_string "x") avoid and @@ -806,7 +806,7 @@ let compute_dec_goal ind lnamesparrec nparrec = check_not_is_defined (); let eq = Lazy.force eq and tt = Lazy.force tt and bb = Lazy.force bb in let list_id = list_id lnamesparrec in - let avoid = List.fold_right (Nameops.name_fold (fun id l -> id::l)) (List.map RelDecl.get_name lnamesparrec) [] in + let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> id::l)) (List.map RelDecl.get_name lnamesparrec) [] in let create_input c = let x = next_ident_away (Id.of_string "x") avoid and y = next_ident_away (Id.of_string "y") avoid in diff --git a/vernac/command.ml b/vernac/command.ml index 25dd724af..87e7e50ec 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -211,7 +211,7 @@ let do_definition ident k pl bl red_option c ctypopt hook = assert(Univ.ContextSet.is_empty ctx); let typ = match ce.const_entry_type with | Some t -> t - | None -> EConstr.Unsafe.to_constr (Retyping.get_type_of env evd (EConstr.of_constr c)) + | None -> EConstr.to_constr evd (Retyping.get_type_of env evd (EConstr.of_constr c)) in Obligations.check_evars env evd; let obls, _, c, cty = @@ -411,8 +411,8 @@ let mk_mltype_data evdref env assums arity indname = (is_ml_type,indname,assums) let prepare_param = function - | LocalAssum (na,t) -> out_name na, LocalAssumEntry t - | LocalDef (na,b,_) -> out_name na, LocalDefEntry b + | LocalAssum (na,t) -> Name.get_id na, LocalAssumEntry t + | LocalDef (na,b,_) -> Name.get_id na, LocalDefEntry b (** Make the arity conclusion flexible to avoid generating an upper bound universe now, only if the universe does not appear anywhere else. @@ -590,7 +590,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite = (* Names of parameters as arguments of the inductive type (defs removed) *) let assums = List.filter is_local_assum ctx_params in - let params = List.map (RelDecl.get_name %> out_name) assums in + let params = List.map (RelDecl.get_name %> Name.get_id) assums in (* Interpret the arities *) let arities = List.map (interp_ind_arity env_params evdref) indl in @@ -907,23 +907,26 @@ let fixsub_module = subtac_dir @ ["Wf"] let tactics_module = subtac_dir @ ["Tactics"] let init_reference dir s () = Coqlib.coq_reference "Command" dir s -let init_constant dir s () = EConstr.of_constr @@ Universes.constr_of_global (Coqlib.coq_reference "Command" dir s) +let init_constant dir s evdref = + let Sigma (c, sigma, _) = Evarutil.new_global (Sigma.Unsafe.of_evar_map !evdref) + (Coqlib.coq_reference "Command" dir s) + in evdref := Sigma.to_evar_map sigma; c let make_ref l s = init_reference l s let fix_proto = init_constant tactics_module "fix_proto" let fix_sub_ref = make_ref fixsub_module "Fix_sub" let measure_on_R_ref = make_ref fixsub_module "MR" let well_founded = init_constant ["Init"; "Wf"] "well_founded" -let mkSubset name typ prop = +let mkSubset evdref name typ prop = let open EConstr in - mkApp (EConstr.of_constr (Universes.constr_of_global (delayed_force build_sigma).typ), + mkApp (Evarutil.e_new_global evdref (delayed_force build_sigma).typ, [| typ; mkLambda (name, typ, prop) |]) let sigT = Lazy.from_fun build_sigma_type let make_qref s = Qualid (Loc.tag @@ qualid_of_string s) let lt_ref = make_qref "Init.Peano.lt" -let rec telescope l = +let rec telescope evdref l = let open EConstr in let open Vars in match l with @@ -935,10 +938,8 @@ let rec telescope l = (fun (ty, tys, (k, constr)) decl -> let t = RelDecl.get_type decl in let pred = mkLambda (RelDecl.get_name decl, t, ty) in - let ty = Universes.constr_of_global (Lazy.force sigT).typ in - let ty = EConstr.of_constr ty in - let intro = Universes.constr_of_global (Lazy.force sigT).intro in - let intro = EConstr.of_constr intro in + let ty = Evarutil.e_new_global evdref (Lazy.force sigT).typ in + let intro = Evarutil.e_new_global evdref (Lazy.force sigT).intro in let sigty = mkApp (ty, [|t; pred|]) in let intro = mkApp (intro, [|lift k t; lift k pred; mkRel k; constr|]) in (sigty, pred :: tys, (succ k, intro))) @@ -947,17 +948,15 @@ let rec telescope l = let (last, subst) = List.fold_right2 (fun pred decl (prev, subst) -> let t = RelDecl.get_type decl in - let p1 = Universes.constr_of_global (Lazy.force sigT).proj1 in - let p1 = EConstr.of_constr p1 in - let p2 = Universes.constr_of_global (Lazy.force sigT).proj2 in - let p2 = EConstr.of_constr p2 in + let p1 = Evarutil.e_new_global evdref (Lazy.force sigT).proj1 in + let p2 = Evarutil.e_new_global evdref (Lazy.force sigT).proj2 in let proj1 = applist (p1, [t; pred; prev]) in let proj2 = applist (p2, [t; pred; prev]) in (lift 1 proj2, LocalDef (get_name decl, proj1, t) :: subst)) (List.rev tys) tl (mkRel 1, []) in ty, (LocalDef (n, last, t) :: subst), constr - | LocalDef (n, b, t) :: tl -> let ty, subst, term = telescope tl in + | LocalDef (n, b, t) :: tl -> let ty, subst, term = telescope evdref tl in ty, (LocalDef (n, b, t) :: subst), lift 1 term let nf_evar_context sigma ctx = @@ -976,7 +975,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = let top_env = push_rel_context binders_rel env in let top_arity = interp_type_evars top_env evdref arityc in let full_arity = it_mkProd_or_LetIn top_arity binders_rel in - let argtyp, letbinders, make = telescope binders_rel in + let argtyp, letbinders, make = telescope evdref binders_rel in let argname = Id.of_string "recarg" in let arg = LocalAssum (Name argname, argtyp) in let binders = letbinders @ [arg] in @@ -1004,7 +1003,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = it_mkLambda_or_LetIn measure letbinders, it_mkLambda_or_LetIn measure binders in - let comb = EConstr.of_constr (Universes.constr_of_global (delayed_force measure_on_R_ref)) in + let comb = Evarutil.e_new_global evdref (delayed_force measure_on_R_ref) in let relargty = EConstr.of_constr relargty in let wf_rel = mkApp (comb, [| argtyp; relargty; rel; measure |]) in let wf_rel_fun x y = @@ -1012,15 +1011,15 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = subst1 y measure_body |]) in wf_rel, wf_rel_fun, measure in - let wf_proof = mkApp (delayed_force well_founded, [| argtyp ; wf_rel |]) in + let wf_proof = mkApp (well_founded evdref, [| argtyp ; wf_rel |]) in let argid' = Id.of_string (Id.to_string argname ^ "'") in let wfarg len = LocalAssum (Name argid', - mkSubset (Name argid') argtyp + mkSubset evdref (Name argid') argtyp (wf_rel_fun (mkRel 1) (mkRel (len + 1)))) in let intern_bl = wfarg 1 :: [arg] in let _intern_env = push_rel_context intern_bl env in - let proj = (*FIXME*)EConstr.of_constr (Universes.constr_of_global (delayed_force build_sigma).Coqlib.proj1) in + let proj = Evarutil.e_new_global evdref (delayed_force build_sigma).Coqlib.proj1 in let wfargpred = mkLambda (Name argid', argtyp, wf_rel_fun (mkRel 1) (mkRel 3)) in let projection = (* in wfarg :: arg :: before *) mkApp (proj, [| argtyp ; wfargpred ; mkRel 1 |]) @@ -1033,7 +1032,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = let intern_fun_binder = LocalAssum (Name (add_suffix recname "'"), intern_fun_arity_prod) in let curry_fun = let wfpred = mkLambda (Name argid', argtyp, wf_rel_fun (mkRel 1) (mkRel (2 * len + 4))) in - let intro = (*FIXME*)EConstr.of_constr (Universes.constr_of_global (delayed_force build_sigma).Coqlib.intro) in + let intro = Evarutil.e_new_global evdref (delayed_force build_sigma).Coqlib.intro in let arg = mkApp (intro, [| argtyp; wfpred; lift 1 make; mkRel 1 |]) in let app = mkApp (mkRel (2 * len + 2 (* recproof + orig binders + current binders *)), [| arg |]) in let rcurry = mkApp (rel, [| measure; lift len measure |]) in @@ -1059,7 +1058,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = let intern_body_lam = it_mkLambda_or_LetIn intern_body (curry_fun :: lift_lets @ fun_bl) in let prop = mkLambda (Name argname, argtyp, top_arity_let) in let def = - mkApp (EConstr.of_constr (Universes.constr_of_global (delayed_force fix_sub_ref)), + mkApp (Evarutil.e_new_global evdref (delayed_force fix_sub_ref), [| argtyp ; wf_rel ; Evarutil.e_new_evar env evdref ~src:(Loc.tag @@ Evar_kinds.QuestionMark (Evar_kinds.Define false,Anonymous)) wf_proof; @@ -1075,12 +1074,12 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = if List.length binders_rel > 1 then let name = add_suffix recname "_func" in let hook l gr _ = - let body = it_mkLambda_or_LetIn (mkApp (EConstr.of_constr (Universes.constr_of_global gr), [|make|])) binders_rel in + let body = it_mkLambda_or_LetIn (mkApp (Evarutil.e_new_global evdref gr, [|make|])) binders_rel in let ty = it_mkProd_or_LetIn top_arity binders_rel in let ty = EConstr.Unsafe.to_constr ty in let pl, univs = Evd.universe_context ?names:pl !evdref in (*FIXME poly? *) - let ce = definition_entry ~poly ~types:ty ~univs (EConstr.Unsafe.to_constr (Evarutil.nf_evar !evdref body)) in + let ce = definition_entry ~poly ~types:ty ~univs (EConstr.to_constr !evdref body) in (** FIXME: include locality *) let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in let gr = ConstRef c in @@ -1097,10 +1096,8 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = in hook, recname, typ in let hook = Lemmas.mk_hook hook in - let fullcoqc = Evarutil.nf_evar !evdref def in - let fullctyp = Evarutil.nf_evar !evdref typ in - let fullcoqc = EConstr.Unsafe.to_constr fullcoqc in - let fullctyp = EConstr.Unsafe.to_constr fullctyp in + let fullcoqc = EConstr.to_constr !evdref def in + let fullctyp = EConstr.to_constr !evdref typ in Obligations.check_evars env !evdref; let evars, _, evars_def, evars_typ = Obligations.eterm_obligations env recname !evdref 0 fullcoqc fullctyp @@ -1143,7 +1140,7 @@ let interp_recursive isfix fixl notations = let sort = Evarutil.evd_comb1 (Typing.type_of ~refresh:true env) evdref t in let fixprot = try - let app = mkApp (delayed_force fix_proto, [|sort; t|]) in + let app = mkApp (fix_proto evdref, [|sort; t|]) in Typing.e_solve_evars env evdref app with e when CErrors.noncritical e -> t in @@ -1303,9 +1300,9 @@ let do_program_recursive local p fixkind fixl ntns = let collect_evars id def typ imps = (* Generalize by the recursive prototypes *) let def = - EConstr.Unsafe.to_constr (nf_evar evd (Termops.it_mkNamedLambda_or_LetIn (EConstr.of_constr def) rec_sign)) + EConstr.to_constr evd (Termops.it_mkNamedLambda_or_LetIn (EConstr.of_constr def) rec_sign) and typ = - EConstr.Unsafe.to_constr (nf_evar evd (Termops.it_mkNamedProd_or_LetIn (EConstr.of_constr typ) rec_sign)) + EConstr.to_constr evd (Termops.it_mkNamedProd_or_LetIn (EConstr.of_constr typ) rec_sign) in let evm = collect_evars_of_term evd def typ in let evars, _, def, typ = diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 17bb87f2a..6d8dd82ac 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -682,12 +682,12 @@ let explain_wrong_abstraction_type env sigma na abs expected result = let explain_abstraction_over_meta _ m n = strbrk "Too complex unification problem: cannot find a solution for both " ++ - pr_name m ++ spc () ++ str "and " ++ pr_name n ++ str "." + Name.print m ++ spc () ++ str "and " ++ Name.print n ++ str "." let explain_non_linear_unification env sigma m t = let t = EConstr.to_constr sigma t in strbrk "Cannot unambiguously instantiate " ++ - pr_name m ++ str ":" ++ + Name.print m ++ str ":" ++ strbrk " which would require to abstract twice on " ++ pr_lconstr_env env sigma t ++ str "." @@ -1055,7 +1055,7 @@ let explain_refiner_bad_type arg ty conclty = let explain_refiner_unresolved_bindings l = str "Unable to find an instance for the " ++ str (String.plural (List.length l) "variable") ++ spc () ++ - prlist_with_sep pr_comma pr_name l ++ str"." + prlist_with_sep pr_comma Name.print l ++ str"." let explain_refiner_cannot_apply t harg = str "In refiner, a term of type" ++ brk(1,1) ++ diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index f57b1bba0..a678d20bb 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -453,11 +453,19 @@ let fold_left' f = function [] -> invalid_arg "fold_left'" | hd :: tl -> List.fold_left f hd tl +let new_global sigma gr = + let open Sigma in + let Sigma (c, sigma, _) = Evarutil.new_global (Sigma.Unsafe.of_evar_map sigma) gr + in Sigma.to_evar_map sigma, c + +let mk_coq_and sigma = new_global sigma (Coqlib.build_coq_and ()) +let mk_coq_conj sigma = new_global sigma (Coqlib.build_coq_conj ()) + let build_combined_scheme env schemes = - let defs = List.map (fun cst -> (* FIXME *) - let evd, c = Evd.fresh_constant_instance env (Evd.from_env env) cst in - (c, Typeops.type_of_constant_in env c)) schemes in -(* let nschemes = List.length schemes in *) + let evdref = ref (Evd.from_env env) in + let defs = List.map (fun cst -> + let evd, c = Evd.fresh_constant_instance env !evdref cst in + evdref := evd; (c, Typeops.type_of_constant_in env c)) schemes in let find_inductive ty = let (ctx, arity) = decompose_prod ty in let (_, last) = List.hd ctx in @@ -471,26 +479,27 @@ let build_combined_scheme env schemes = let (c, t) = List.hd defs in let ctx, ind, nargs = find_inductive t in (* Number of clauses, including the predicates quantification *) - let prods = nb_prod Evd.empty (EConstr.of_constr t) - (nargs + 1) (** FIXME *) in - let coqand = Universes.constr_of_global @@ Coqlib.build_coq_and () in - let coqconj = Universes.constr_of_global @@ Coqlib.build_coq_conj () in + let prods = nb_prod !evdref (EConstr.of_constr t) - (nargs + 1) in + let sigma, coqand = mk_coq_and !evdref in + let sigma, coqconj = mk_coq_conj sigma in + let () = evdref := sigma in let relargs = rel_vect 0 prods in let concls = List.rev_map - (fun (cst, t) -> (* FIXME *) + (fun (cst, t) -> mkApp(mkConstU cst, relargs), snd (decompose_prod_n prods t)) defs in let concl_bod, concl_typ = fold_left' (fun (accb, acct) (cst, x) -> - mkApp (coqconj, [| x; acct; cst; accb |]), - mkApp (coqand, [| x; acct |])) concls + mkApp (EConstr.to_constr !evdref coqconj, [| x; acct; cst; accb |]), + mkApp (EConstr.to_constr !evdref coqand, [| x; acct |])) concls in let ctx, _ = list_split_rev_at prods (List.rev_map (fun (x, y) -> LocalAssum (x, y)) ctx) in let typ = List.fold_left (fun d c -> Term.mkProd_wo_LetIn c d) concl_typ ctx in let body = it_mkLambda_or_LetIn concl_bod ctx in - (body, typ) + (!evdref, body, typ) let do_combined_scheme name schemes = let csts = @@ -501,9 +510,9 @@ let do_combined_scheme name schemes = with Not_found -> user_err Pp.(pr_qualid (snd qualid) ++ str " is not declared.")) schemes in - let body,typ = build_combined_scheme (Global.env ()) csts in + let sigma,body,typ = build_combined_scheme (Global.env ()) csts in let proof_output = Future.from_val ((body,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in - ignore (define (snd name) UserIndividualRequest Evd.empty proof_output (Some typ)); + ignore (define (snd name) UserIndividualRequest sigma proof_output (Some typ)); fixpoint_message None [snd name] (**********************************************************************) diff --git a/vernac/indschemes.mli b/vernac/indschemes.mli index e5d79fd51..0f559d2bd 100644 --- a/vernac/indschemes.mli +++ b/vernac/indschemes.mli @@ -40,7 +40,7 @@ val do_scheme : (Id.t located option * scheme) list -> unit (** Combine a list of schemes into a conjunction of them *) -val build_combined_scheme : env -> constant list -> constr * types +val build_combined_scheme : env -> constant list -> Evd.evar_map * constr * types val do_combined_scheme : Id.t located -> Id.t located list -> unit diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 6c1d64cfe..77be7f454 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1003,12 +1003,12 @@ let vernac_arguments locality reference args more_implicits nargs_for_red flags let err_extra_args names = user_err ~hdr:"vernac_declare_arguments" (strbrk "Extra arguments: " ++ - prlist_with_sep pr_comma pr_name names ++ str ".") + prlist_with_sep pr_comma Name.print names ++ str ".") in let err_missing_args names = user_err ~hdr:"vernac_declare_arguments" (strbrk "The following arguments are not declared: " ++ - prlist_with_sep pr_comma pr_name names ++ str ".") + prlist_with_sep pr_comma Name.print names ++ str ".") in let rec check_extra_args extra_args = @@ -1093,14 +1093,14 @@ let vernac_arguments locality reference args more_implicits nargs_for_red flags match !example_renaming with | None -> mt () | Some (o,n) -> - str "Argument " ++ pr_name o ++ - str " renamed to " ++ pr_name n ++ str "."); + str "Argument " ++ Name.print o ++ + str " renamed to " ++ Name.print n ++ str "."); let duplicate_names = List.duplicates Name.equal (List.filter ((!=) Anonymous) names) in if not (List.is_empty duplicate_names) then begin - let duplicates = prlist_with_sep pr_comma pr_name duplicate_names in + let duplicates = prlist_with_sep pr_comma Name.print duplicate_names in user_err (strbrk "Some argument names are duplicated: " ++ duplicates) end; @@ -1129,7 +1129,7 @@ let vernac_arguments locality reference args more_implicits nargs_for_red flags anonymous argument implicit *) | Anonymous :: _, (name, _) :: _ -> user_err ~hdr:"vernac_declare_arguments" - (strbrk"Argument "++ pr_name name ++ + (strbrk"Argument "++ Name.print name ++ strbrk " cannot be declared implicit.") | Name id :: inf_names, (name, impl) :: implicits -> @@ -1765,12 +1765,11 @@ let vernac_locate = let open Feedback in function let vernac_register id r = if Pfedit.refining () then user_err Pp.(str "Cannot register a primitive while in proof editing mode."); - let t = (Constrintern.global_reference (snd id)) in - if not (isConst t) then + let kn = Constrintern.global_reference (snd id) in + if not (isConstRef kn) then user_err Pp.(str "Register inline: a constant is expected"); - let kn = destConst t in match r with - | RegisterInline -> Global.register_inline (Univ.out_punivs kn) + | RegisterInline -> Global.register_inline (destConstRef kn) (********************) (* Proof management *) |