From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sun, 11 Jun 2006 08:13:05 +0000 (+0000)
Subject: - slight fix in lapply syntax
X-Git-Tag: 0.4.95@7852~1342
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e6cc7d4297352151b0fefe44cbe57cbe63a1c579;p=helm.git

- slight fix in lapply syntax
- Ferruccio Guidi is NOT a former member :)
---

diff --git a/components/cic/.depend b/components/cic/.depend
index a35156331..bc476d918 100644
--- 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 82a9d39d6..60d32461b 100644
--- 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 43e2117cd..9038b3b60 100644
--- 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 0d9f450f9..5bf73503b 100644
--- 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 e94cfa5ab..743811ceb 100644
--- 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 fc3681074..cc0043724 100644
--- 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>