From: Ferruccio Guidi Date: Sun, 11 Jun 2006 08:13:05 +0000 (+0000) Subject: - slight fix in lapply syntax X-Git-Tag: make_still_working~7217 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=cc16727f34114cee287e6a81b80f68657c656725;p=helm.git - slight fix in lapply syntax - Ferruccio Guidi is NOT a former member :) --- diff --git a/helm/software/components/cic/.depend b/helm/software/components/cic/.depend index a35156331..bc476d918 100644 --- a/helm/software/components/cic/.depend +++ b/helm/software/components/cic/.depend @@ -19,8 +19,8 @@ cicUtil.cmo: cicUniv.cmi cic.cmo cicUtil.cmi cicUtil.cmx: cicUniv.cmx cic.cmx cicUtil.cmi helmLibraryObjects.cmo: cic.cmo helmLibraryObjects.cmi helmLibraryObjects.cmx: cic.cmx helmLibraryObjects.cmi -libraryObjects.cmo: helmLibraryObjects.cmi libraryObjects.cmi -libraryObjects.cmx: helmLibraryObjects.cmx libraryObjects.cmi +libraryObjects.cmo: libraryObjects.cmi +libraryObjects.cmx: libraryObjects.cmi discrimination_tree.cmo: cic.cmo discrimination_tree.cmi discrimination_tree.cmx: cic.cmx discrimination_tree.cmi path_indexing.cmo: cic.cmo path_indexing.cmi diff --git a/helm/software/components/extlib/.depend b/helm/software/components/extlib/.depend index 82a9d39d6..60d32461b 100644 --- a/helm/software/components/extlib/.depend +++ b/helm/software/components/extlib/.depend @@ -1,7 +1,7 @@ componentsConf.cmo: componentsConf.cmi componentsConf.cmx: componentsConf.cmi -hExtlib.cmo: componentsConf.cmi hExtlib.cmi -hExtlib.cmx: componentsConf.cmx hExtlib.cmi +hExtlib.cmo: hExtlib.cmi +hExtlib.cmx: hExtlib.cmi hMarshal.cmo: hExtlib.cmi hMarshal.cmi hMarshal.cmx: hExtlib.cmx hMarshal.cmi patternMatcher.cmo: patternMatcher.cmi diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml index 43e2117cd..9038b3b60 100644 --- a/helm/software/components/grafite/grafiteAstPp.ml +++ b/helm/software/components/grafite/grafiteAstPp.ml @@ -129,7 +129,7 @@ let rec pp_tactic ~term_pp ~lazy_term_pp = (match level_opt with None -> "" | Some i -> " depth = " ^ string_of_int i ^ " ") (term_pp term) (match terms with [] -> "" | _ -> " to " ^ terms_pp ~term_pp terms) - (match ident_opt with None -> "" | Some ident -> " using " ^ ident) + (match ident_opt with None -> "" | Some ident -> " as " ^ ident) | Left _ -> "left" | LetIn (_, term, ident) -> sprintf "let %s in %s" (term_pp term) ident | Reduce (_, kind, pat) -> diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index 0d9f450f9..5bf73503b 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -197,7 +197,7 @@ EXTEND depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ]; what = tactic_term; to_what = OPT [ "to" ; t = tactic_term_list1 -> t ]; - ident = OPT [ IDENT "using" ; ident = IDENT -> ident ] -> + ident = OPT [ IDENT "as" ; ident = IDENT -> ident ] -> let to_what = match to_what with None -> [] | Some to_what -> to_what in GrafiteAst.LApply (loc, depth, to_what, what, ident) | IDENT "left" -> GrafiteAst.Left loc diff --git a/helm/software/components/tactics/.depend b/helm/software/components/tactics/.depend index e94cfa5ab..743811ceb 100644 --- a/helm/software/components/tactics/.depend +++ b/helm/software/components/tactics/.depend @@ -87,15 +87,15 @@ paramodulation/indexing.cmx: paramodulation/utils.cmx \ paramodulation/equality_indexing.cmx paramodulation/equality.cmx \ paramodulation/indexing.cmi paramodulation/saturation.cmo: paramodulation/utils.cmi \ - paramodulation/subst.cmi reductionTactics.cmi proofEngineTypes.cmi \ - proofEngineReduction.cmi primitiveTactics.cmi \ - paramodulation/inference.cmi paramodulation/indexing.cmi \ - paramodulation/equality.cmi paramodulation/saturation.cmi + paramodulation/subst.cmi proofEngineTypes.cmi proofEngineReduction.cmi \ + proofEngineHelpers.cmi primitiveTactics.cmi paramodulation/inference.cmi \ + paramodulation/indexing.cmi paramodulation/equality.cmi \ + paramodulation/saturation.cmi paramodulation/saturation.cmx: paramodulation/utils.cmx \ - paramodulation/subst.cmx reductionTactics.cmx proofEngineTypes.cmx \ - proofEngineReduction.cmx primitiveTactics.cmx \ - paramodulation/inference.cmx paramodulation/indexing.cmx \ - paramodulation/equality.cmx paramodulation/saturation.cmi + paramodulation/subst.cmx proofEngineTypes.cmx proofEngineReduction.cmx \ + proofEngineHelpers.cmx primitiveTactics.cmx paramodulation/inference.cmx \ + paramodulation/indexing.cmx paramodulation/equality.cmx \ + paramodulation/saturation.cmi variousTactics.cmo: tacticals.cmi proofEngineTypes.cmi \ proofEngineReduction.cmi proofEngineHelpers.cmi primitiveTactics.cmi \ variousTactics.cmi diff --git a/helm/software/matita/help/C/sec_tactics.xml b/helm/software/matita/help/C/sec_tactics.xml index fc3681074..cc0043724 100644 --- a/helm/software/matita/help/C/sec_tactics.xml +++ b/helm/software/matita/help/C/sec_tactics.xml @@ -847,11 +847,11 @@ its constructor takes no arguments. - <emphasis role="bold">lapply</emphasis> [<emphasis role="bold">depth=</emphasis>&nat;] &sterm; [<emphasis role="bold">to</emphasis> &sterm; [&sterm;]…] [<emphasis role="bold">using</emphasis> &id;] + <emphasis role="bold">lapply</emphasis> [<emphasis role="bold">depth=</emphasis>&nat;] &sterm; [<emphasis role="bold">to</emphasis> &sterm; [&sterm;]…] [<emphasis role="bold">as</emphasis> &id;] lapply lapply depth=d t - to t1, ..., tn using H + to t1, ..., tn as H diff --git a/helm/www/matita/development.shtml b/helm/www/matita/development.shtml index ebf279462..4454357a2 100644 --- a/helm/www/matita/development.shtml +++ b/helm/www/matita/development.shtml @@ -24,11 +24,11 @@
  • Claudio Sacerdoti Coen - Lecturer
  • Enrico Tassi - PhD Student
  • Stefano Zacchiroli - PhD Student
    • +
  • Ferruccio Guidi - PhD

    • Former members