diff options
| -rw-r--r-- | doc/refman/RefMan-gal.tex | 2 | ||||
| -rw-r--r-- | lib/system.ml | 3 | ||||
| -rw-r--r-- | tactics/equality.ml | 4 | ||||
| -rw-r--r-- | tactics/hipattern.ml4 | 17 | ||||
| -rw-r--r-- | tactics/hipattern.mli | 3 | ||||
| -rw-r--r-- | tactics/tactics.ml | 2 | ||||
| -rw-r--r-- | theories/Init/Datatypes.v | 4 | ||||
| -rw-r--r-- | toplevel/mltop.ml4 | 2 |
8 files changed, 29 insertions, 8 deletions
diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex index 28cb402f3..3e3d42263 100644 --- a/doc/refman/RefMan-gal.tex +++ b/doc/refman/RefMan-gal.tex @@ -1427,7 +1427,7 @@ generally any mutually recursive definitions. \begin{Variants} \item {\tt Fixpoint {\ident$_1$} {\params$_1$} :{\type$_1$} := {\term$_1$}\\ with {\ldots} \\ - with {\ident$_m$} {\params$_m$} :{\type$_m$} := {\type$_m$}}\\ + with {\ident$_m$} {\params$_m$} :{\type$_m$} := {\term$_m$}}\\ Allows to define simultaneously {\ident$_1$}, {\ldots}, {\ident$_m$}. \end{Variants} diff --git a/lib/system.ml b/lib/system.ml index 4f21c8746..7ca62dcc8 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -116,7 +116,8 @@ let where_in_path warn path filename = msg_warning (str filename ++ str " has been found in" ++ spc () ++ hov 0 (str "[ " ++ - hv 0 (prlist_with_sep pr_semicolon (fun (lpe,_) -> str lpe) l) + hv 0 (prlist_with_sep (fun () -> spc() ++ pr_semicolon()) + (fun (lpe,_) -> str lpe) l) ++ str " ];") ++ fnl () ++ str "loading " ++ str f); (lpe, f) in diff --git a/tactics/equality.ml b/tactics/equality.ml index cbcf5993c..641e274af 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -116,13 +116,13 @@ let general_rewrite_ebindings_clause cls lft2rgt occs ((c,l) : open_constr with_ let sigma = Evd.merge sigma (project gl) in let ctype = get_type_of env sigma c' in let rels, t = decompose_prod (whd_betaiotazeta ctype) in - match match_with_equation t with + match match_with_equality_type t with | Some (hdcncl,_) -> (* Fast path: direct leibniz rewrite *) leibniz_rewrite_ebindings_clause cls lft2rgt sigma c' l with_evars gl hdcncl | None -> let env' = List.fold_left (fun env (n,t) -> push_rel (n, None, t) env) env rels in let _,t' = splay_prod env' sigma t in (* Search for underlying eq *) - match match_with_equation t' with + match match_with_equality_type t' with | Some (hdcncl,_) -> (* Maybe a setoid relation with eq inside *) if l = NoBindings && !is_applied_setoid_relation t then !general_setoid_rewrite_clause cls lft2rgt occs c ~new_goals:[] gl diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4 index 4145a8dcc..9e0281855 100644 --- a/tactics/hipattern.ml4 +++ b/tactics/hipattern.ml4 @@ -121,8 +121,8 @@ let match_with_unit_type t = let constr_types = mip.mind_nf_lc in let nconstr = Array.length mip.mind_consnames in let zero_args c = - nb_prod c = mib.mind_nparams in - if nconstr = 1 && array_for_all zero_args constr_types then + nb_prod c = mib.mind_nparams in + if nconstr = 1 && zero_args constr_types.(0) then Some hdapp else None @@ -157,6 +157,19 @@ let match_with_equation t = let is_equation t = op2bool (match_with_equation t) +let match_with_equality_type t = + let (hdapp,args) = decompose_app t in + match (kind_of_term hdapp) with + | Ind ind when args <> [] -> + let (mib,mip) = Global.lookup_inductive ind in + let nconstr = Array.length mip.mind_consnames in + if nconstr = 1 && constructor_nrealargs (Global.env()) (ind,1) = 0 + then + Some (hdapp,args) + else + None + | _ -> None + let coq_arrow_pattern = PATTERN [ ?X1 -> ?X2 ] let match_arrow_pattern t = diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli index 6dde098cf..ce1c70e5a 100644 --- a/tactics/hipattern.mli +++ b/tactics/hipattern.mli @@ -69,6 +69,9 @@ val is_unit_type : testing_function val match_with_equation : (constr * constr list) matching_function val is_equation : testing_function +(* type with only one constructor, no arguments and at least one dependency *) +val match_with_equality_type : (constr * constr list) matching_function + val match_with_nottype : (constr * constr) matching_function val is_nottype : testing_function diff --git a/tactics/tactics.ml b/tactics/tactics.ml index e0f5a3a42..da4d95eaa 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2900,7 +2900,7 @@ let reflexivity_red allowred gl = let concl = if not allowred then pf_concl gl else whd_betadeltaiota (pf_env gl) (project gl) (pf_concl gl) in - match match_with_equation concl with + match match_with_equality_type concl with | None -> None | Some _ -> Some (one_constructor 1 NoBindings) diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index 1e8a5b062..45228073a 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -72,6 +72,10 @@ Hint Resolve andb_true_intro: bool v62. Inductive eq_true : bool -> Prop := is_eq_true : eq_true true. +(** Technical lemma: identify -> rewriting on eq_true with <- rewriting *) + +Definition eq_true_ind_r := eq_true_ind. + (** [nat] is the datatype of natural numbers built from [O] and successor [S]; note that the constructor name is the letter O. Numbers in [nat] can be denoted using a decimal notation; diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4 index 275f9a5f7..694e60dbc 100644 --- a/toplevel/mltop.ml4 +++ b/toplevel/mltop.ml4 @@ -106,7 +106,7 @@ let dir_ml_load s = * if this code section starts to use a module not used elsewhere * in this file, the Makefile dependency logic needs to be updated. *) - let _,gname = where_in_path true !coq_mlpath_copy s in + let _,gname = where_in_path true (list_uniquize !coq_mlpath_copy) s in try Dynlink.loadfile gname; with | Dynlink.Error a -> |