]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/gTopLevel/proofEngineStructuralRules.ml
Param ~ask_dtd_to_the_getter added to Cic2Xml.print_object.
[helm.git] / helm / gTopLevel / proofEngineStructuralRules.ml
index e01f95e9f02f121287fcc1416401878e1ac53263..d89420f58cde8526c4d578341db8633db23c7f10 100644 (file)
@@ -36,7 +36,7 @@ let clearbody ~hyp ~status:(proof, goal) =
         let string_of_name =
          function
             C.Name n -> n
-          | C.Anonimous -> "_"
+          | C.Anonymous -> "_"
         in
         let metasenv' =
          List.map
@@ -101,7 +101,7 @@ let clear ~hyp:hyp_to_clear ~status:(proof, goal) =
         let string_of_name =
          function
             C.Name n -> n
-          | C.Anonimous -> "_"
+          | C.Anonymous -> "_"
         in
         let metasenv' =
          List.map