- slight fix in lapply syntax

- Ferruccio Guidi is NOT a former member :)

diff --git a/components/cic/.depend b/components/cic/.depend
index a3515633139ee1740c27ba15db60c806b6a60ba9..bc476d918aa8ab13fc8f6a96ee2cb56bc960d52e 100644 (file)
--- a/components/cic/.depend
+++ b/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/components/extlib/.depend b/components/extlib/.depend
index 82a9d39d62fd592fa7f016d1af2966a92b8e39a6..60d32461b8ff18f78a2e0b32cf334af9b00860e8 100644 (file)
--- a/components/extlib/.depend
+++ b/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/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml
index 43e2117cdb13470cb435776cd22c1420f6c68819..9038b3b6043a198c12add0c97da8d4c9106ef38b 100644 (file)
--- a/components/grafite/grafiteAstPp.ml
+++ b/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/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml
index 0d9f450f9d8f9d1724c494bc7777d05f549c316c..5bf73503b7503677b49341dae3956c7e58d84399 100644 (file)
--- a/components/grafite_parser/grafiteParser.ml
+++ b/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/components/tactics/.depend b/components/tactics/.depend
index e94cfa5ab2f333e2ef303ae40cf80d6f288807b3..743811ceb5d9d315e622ff08c7adffff53b62d5d 100644 (file)
--- a/components/tactics/.depend
+++ b/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/matita/help/C/sec_tactics.xml b/matita/help/C/sec_tactics.xml
index fc3681074429c8f29b7d90b975937df1628332ec..cc0043724f57c33fa32f0e7bec60dfff326c8098 100644 (file)
--- a/matita/help/C/sec_tactics.xml
+++ b/matita/help/C/sec_tactics.xml
@@ -847,11 +847,11 @@ its constructor takes no arguments.</para>
     </para>
   </sect1>
   <sect1 id="tac_lapply">
-    <title><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;]</title>
+    <title><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;]</title>
     <titleabbrev>lapply</titleabbrev>
     <para><userinput>
      lapply depth=d t 
-     to t<subscript>1</subscript>, ..., t<subscript>n</subscript> using H
+     to t<subscript>1</subscript>, ..., t<subscript>n</subscript> as H
     </userinput></para>
     <para>
       <variablelist>